C

• CSub (SORT)

Field

• accDefinition (TACLET)

• alphaObj (SORT)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assignableDefinition (TACLET)

• castTrueImpliesOriginalTrue (TACLET)

• dismissNonSelectedField (TACLET)

• dismissNonSelectedFieldEQ (TACLET)

• dropEffectlessStores (TACLET)

• equalityToSelect (TACLET)

• narrowSelectType (TACLET)

• narrowTypeFinal (TACLET)

• onlyCreatedObjectsAreInLocSets (TACLET)

• onlyCreatedObjectsAreInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreInLocSetsEQFinal (TACLET)

• onlyCreatedObjectsAreInLocSetsFinal (TACLET)

• onlyCreatedObjectsAreObserved (TACLET)

• onlyCreatedObjectsAreObservedInLocSets (TACLET)

• onlyCreatedObjectsAreObservedInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreReferenced (TACLET)

• onlyCreatedObjectsAreReferencedFinal (TACLET)

• pullOutSelect (TACLET)

• reachDependenciesAnon (TACLET)

• reachDependenciesAnonCoarse (TACLET)

• reachDependenciesStore (TACLET)

• reachDependenciesStoreEQ (TACLET)

• reachDependenciesStoreSimple (TACLET)

• reachDependenciesStoreSimpleEQ (TACLET)

• reachEndOfUniquePath (TACLET)

• reachEndOfUniquePath2 (TACLET)

• reachUniquePathSameSteps (TACLET)

• selectOfAnon (TACLET)

• selectOfAnonEQ (TACLET)

• selectOfCreate (TACLET)

• selectOfCreateEQ (TACLET)

• selectOfMemset (TACLET)

• selectOfMemsetEQ (TACLET)

• selectOfStore (TACLET)

• selectOfStoreEQ (TACLET)

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• wellFormedStoreLocSet (TACLET)

• wellFormedStoreLocSetEQ (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

• wellFormedStorePrimitive (TACLET)

• wellFormedStorePrimitiveEQ (TACLET)

Free

• Free (SORT)

G

• GSub (SORT)

• J (SORT)

• exact_instance_for_interfaces_or_abstract_classes (TACLET)

• instanceof_not_compatible (TACLET)

• instanceof_not_compatible_2 (TACLET)

• instanceof_not_compatible_3 (TACLET)

• instanceof_not_compatible_4 (TACLET)

• instanceof_static_type (TACLET)

• instanceof_static_type_2 (TACLET)

• sameTypeTrue (TACLET)

Heap

• acc (PREDICATE)

• accDefinition (TACLET)

• alphaObj (SORT)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assignable (PREDICATE)

• assignableDefinition (TACLET)

• castTrueImpliesOriginalTrue (TACLET)

• definitionOfNewObjectsIsomorphic (TACLET)

• definitionOfNewOnHeap (TACLET)

• dismissNonSelectedField (TACLET)

• dismissNonSelectedFieldEQ (TACLET)

• dropEffectlessStores (TACLET)

• equalityToSelect (TACLET)

• loopScopeInvBox (TACLET)

• loopScopeInvDia (TACLET)

• memsetEmpty (TACLET)

• narrowSelectArrayType (TACLET)

• narrowSelectType (TACLET)

• newObjectsIsomorphic (PREDICATE)

• newOnHeap (PREDICATE)

• nonNull (PREDICATE)

• nullCreated (TACLET)

• onlyCreatedObjectsAreInLocSets (TACLET)

• onlyCreatedObjectsAreInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreInLocSetsEQFinal (TACLET)

• onlyCreatedObjectsAreInLocSetsFinal (TACLET)

• onlyCreatedObjectsAreObserved (TACLET)

• onlyCreatedObjectsAreObservedInLocSets (TACLET)

• onlyCreatedObjectsAreObservedInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreReferenced (TACLET)

• onlyCreatedObjectsAreReferencedFinal (TACLET)

• only_created_objects_are_reachable (TACLET)

• pullOutSelect (TACLET)

• reach (PREDICATE)

• reachAddOne (TACLET)

• reachAddOne2 (TACLET)

• reachDefinition (TACLET)

• reachDependenciesAnon (TACLET)

• reachDependenciesAnonCoarse (TACLET)

• reachDependenciesStore (TACLET)

• reachDependenciesStoreEQ (TACLET)

• reachDependenciesStoreSimple (TACLET)

• reachDependenciesStoreSimpleEQ (TACLET)

• reachDoesNotDependOnCreatedness (TACLET)

• reachEndOfUniquePath (TACLET)

• reachEndOfUniquePath2 (TACLET)

• reachNull (TACLET)

• reachNull2 (TACLET)

• reachOne (TACLET)

• reachUniquePathSameSteps (TACLET)

• reachZero (TACLET)

• reach_does_not_depend_on_fresh_locs (TACLET)

• reach_does_not_depend_on_fresh_locs_EQ (TACLET)

• selectCreatedOfAnon (TACLET)

• selectCreatedOfAnonAsFormula (TACLET)

• selectCreatedOfAnonAsFormulaEQ (TACLET)

• selectCreatedOfAnonEQ (TACLET)

• selectOfAnon (TACLET)

• selectOfAnonEQ (TACLET)

• selectOfCreate (TACLET)

• selectOfCreateEQ (TACLET)

• selectOfMemset (TACLET)

• selectOfMemsetEQ (TACLET)

• selectOfStore (TACLET)

• selectOfStoreEQ (TACLET)

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• threeBranchLoopScopeInvRuleBox (TACLET)

• threeBranchLoopScopeInvRuleDia (TACLET)

• wellFormed (PREDICATE)

• wellFormedAnon (TACLET)

• wellFormedAnonEQ (TACLET)

• wellFormedCreate (TACLET)

• wellFormedMemsetArrayObject (TACLET)

• wellFormedMemsetArrayPrimitive (TACLET)

• wellFormedStoreArray (TACLET)

• wellFormedStoreLocSet (TACLET)

• wellFormedStoreLocSetEQ (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

• wellFormedStorePrimitive (TACLET)

• wellFormedStorePrimitiveArray (TACLET)

• wellFormedStorePrimitiveEQ (TACLET)

J

• instance_for_final_types (TACLET)

Map

• Map (SORT)

• isFinite (PREDICATE)

• mapSize (FILE)

Pair

• Pair (SORT)

SORT

• alphSub (SORT)

• ssubsort (PREDICATE)

alph

• alphSub (SORT)

• ssubsortDirect (TACLET)

alphSub

• ssubsortDirect (TACLET)

alpha

• alphaObj (SORT)

• betaObj (SORT)

• dismissNonSelectedField (TACLET)

• dismissNonSelectedFieldEQ (TACLET)

• maxAxiom (TACLET)

• minAxiom (TACLET)

• narrowFinalArrayType (TACLET)

• narrowSelectArrayType (TACLET)

• narrowSelectType (TACLET)

• narrowTypeFinal (TACLET)

• reachEndOfUniquePath (TACLET)

• reachEndOfUniquePath2 (TACLET)

• selectOfStore (TACLET)

• selectOfStoreEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• wd_Heap_Reference (TACLET)

• wd_Heap_Reference_Array (TACLET)

• wd_Heap_Reference_Created (TACLET)

• wd_Heap_Reference_Static (TACLET)

• wd_Seq_Get (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

alphaObj

• allocateInstance (TACLET)

• allocateInstanceWithLength (TACLET)

any

• Map (SORT)

• Pair (SORT)

• alphaObj (SORT)

• applyOnElementary (TACLET)

• applyOnPV (TACLET)

• applyOnRigidTerm (TACLET)

• applySkip1 (TACLET)

• arrayStoreValid (PREDICATE)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assignableDefinition (TACLET)

• betaObj (SORT)

• castTrueImpliesOriginalTrue (TACLET)

• defIsFinite (TACLET)

• definitionOfNewOnHeap (TACLET)

• definitionOfObjectIsomorphic (TACLET)

• definitionOfObjectsIsomorphic (TACLET)

• definitionOfSameTypes (TACLET)

• dismissNonSelectedField (TACLET)

• dismissNonSelectedFieldEQ (TACLET)

• dropEffectlessStores (TACLET)

• equalityToSelect (TACLET)

• hideAuxiliaryEq (TACLET)

• hideAuxiliaryEqConcrete (TACLET)

• hideAuxiliaryEqConcrete2 (TACLET)

• instance_for_final_types (TACLET)

• instanceof_not_compatible (TACLET)

• instanceof_not_compatible_2 (TACLET)

• instanceof_not_compatible_3 (TACLET)

• instanceof_not_compatible_4 (TACLET)

• instanceof_static_type (TACLET)

• instanceof_static_type_2 (TACLET)

• loopScopeInvDia (TACLET)

• measuredBy (PREDICATE)

• measuredByCheck (PREDICATE)

• measuredByCheck (TACLET)

• measuredByCheckEmpty (TACLET)

• memsetEmpty (TACLET)

• prec (PREDICATE)

• precOfIntPair (TACLET)

• precOfPair (TACLET)

• precOfPairInt (TACLET)

• precOfSeq (TACLET)

• reachDependenciesStore (TACLET)

• reachDependenciesStoreEQ (TACLET)

• reachDependenciesStoreSimple (TACLET)

• reachDependenciesStoreSimpleEQ (TACLET)

• sameType (PREDICATE)

• sameTypeTrue (TACLET)

• selectOfMemset (TACLET)

• selectOfMemsetEQ (TACLET)

• sequentialToParallel1 (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifyUpdate1 (TACLET)

• threeBranchLoopScopeInvRuleDia (TACLET)

• wd (TRANSFORMER)

beta

• narrowFinalArrayType (TACLET)

• narrowSelectArrayType (TACLET)

• narrowSelectType (TACLET)

• narrowTypeFinal (TACLET)

• pullOutSelect (TACLET)

• selectOfAnon (TACLET)

• selectOfAnonEQ (TACLET)

• selectOfCreate (TACLET)

• selectOfCreateEQ (TACLET)

• selectOfMemset (TACLET)

• selectOfMemsetEQ (TACLET)

• selectOfStore (TACLET)

• selectOfStoreEQ (TACLET)

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• wellFormedMemsetArrayPrimitive (TACLET)

• wellFormedStorePrimitive (TACLET)

• wellFormedStorePrimitiveArray (TACLET)

• wellFormedStorePrimitiveEQ (TACLET)

boolean

• allocateInstance (TACLET)

• allocateInstanceWithLength (TACLET)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assignableDefinition (TACLET)

• betaObj (SORT)

• boolean (SORT)

• castTrueImpliesOriginalTrue (TACLET)

• definitionOfNewOnHeap (TACLET)

• exact_instance_definition_boolean (TACLET)

• insert_constant_string_value (TACLET)

• maxAxiom (TACLET)

• minAxiom (TACLET)

• nullCreated (TACLET)

• onlyCreatedObjectsAreInLocSets (TACLET)

• onlyCreatedObjectsAreInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreInLocSetsEQFinal (TACLET)

• onlyCreatedObjectsAreInLocSetsFinal (TACLET)

• onlyCreatedObjectsAreObserved (TACLET)

• onlyCreatedObjectsAreObservedInLocSets (TACLET)

• onlyCreatedObjectsAreObservedInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreReferenced (TACLET)

• onlyCreatedObjectsAreReferencedFinal (TACLET)

• only_created_objects_are_reachable (TACLET)

• reach_does_not_depend_on_fresh_locs (TACLET)

• reach_does_not_depend_on_fresh_locs_EQ (TACLET)

• selectCreatedOfAnon (TACLET)

• selectCreatedOfAnonAsFormula (TACLET)

• selectCreatedOfAnonAsFormulaEQ (TACLET)

• selectCreatedOfAnonEQ (TACLET)

• stringAssignment (TACLET)

• wd_Heap_Reference (TACLET)

• wd_Heap_Reference_Array (TACLET)

• wd_Heap_Store (TACLET)

• wd_LocSet_AllElemsArr (TACLET)

• wd_LocSet_AllElemsArrLocsets (TACLET)

• wellFormedMemsetArrayObject (TACLET)

• wellFormedStoreArray (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

deltaObject

• accDefinition (TACLET)

• onlyCreatedObjectsAreObserved (TACLET)

• onlyCreatedObjectsAreReferenced (TACLET)

• onlyCreatedObjectsAreReferencedFinal (TACLET)

• wellFormedMemsetArrayObject (TACLET)

• wellFormedStoreArray (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

java.lang.Object

• abortJavaCardTransactionBox (TACLET)

• abortJavaCardTransactionDiamond (TACLET)

• allocateInstance (TACLET)

• allocateInstanceWithLength (TACLET)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assignableDefinition (TACLET)

• definitionOfNewOnHeap (TACLET)

• definitionOfObjectIsomorphic (TACLET)

• definitionOfObjectsIsomorphic (TACLET)

• deltaObject (SORT)

• getJavaCardTransient (TACLET)

• insert_constant_string_value (TACLET)

• java.io.Serializable (SORT)

• java.lang.Cloneable (SORT)

• java.lang.String (SORT)

• nullCreated (TACLET)

• onlyCreatedObjectsAreInLocSets (TACLET)

• onlyCreatedObjectsAreInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreInLocSetsEQFinal (TACLET)

• onlyCreatedObjectsAreInLocSetsFinal (TACLET)

• onlyCreatedObjectsAreObserved (TACLET)

• onlyCreatedObjectsAreObservedInLocSets (TACLET)

• onlyCreatedObjectsAreObservedInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreReferenced (TACLET)

• onlyCreatedObjectsAreReferencedFinal (TACLET)

• only_created_objects_are_reachable (TACLET)

• reach_does_not_depend_on_fresh_locs (TACLET)

• reach_does_not_depend_on_fresh_locs_EQ (TACLET)

• selectCreatedOfAnon (TACLET)

• selectCreatedOfAnonAsFormula (TACLET)

• selectCreatedOfAnonAsFormulaEQ (TACLET)

• selectCreatedOfAnonEQ (TACLET)

• selectOfAnon (TACLET)

• selectOfAnonEQ (TACLET)

• selectOfCreate (TACLET)

• selectOfCreateEQ (TACLET)

• selectOfMemset (TACLET)

• selectOfMemsetEQ (TACLET)

• selectOfStore (TACLET)

• selectOfStoreEQ (TACLET)

• setJavaCardTransient (TACLET)

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• stringAssignment (TACLET)

• wd_Heap_Reference (TACLET)

• wd_Heap_Reference_Array (TACLET)

• wd_Heap_Reference_Created (TACLET)

• wd_Heap_Store (TACLET)

• wd_LocSet_AllElemsArr (TACLET)

• wd_LocSet_AllElemsArrLocsets (TACLET)

• wellFormedMemsetArrayObject (TACLET)

• wellFormedStoreArray (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

java.lang.String

• java.lang.String (SORT)

• stringConcat (TACLET)

• stringConcatBooleanLeft (TACLET)

• stringConcatBooleanRight (TACLET)

• stringConcatCharExpLeft (TACLET)

• stringConcatCharExpRight (TACLET)

• stringConcatIntExpLeft (TACLET)

• stringConcatIntExpRight (TACLET)

• stringConcatObjectLeft (TACLET)

• stringConcatObjectRight (TACLET)

acc

• acc (PREDICATE)

arrayStoreValid

• arrayStoreValid (PREDICATE)

assignable

• assignable (PREDICATE)

isFinite

• isFinite (PREDICATE)

measuredBy

• measuredBy (PREDICATE)

measuredByCheck

• measuredByCheck (PREDICATE)

measuredByEmpty

• measuredByEmpty (PREDICATE)

newObjectsIsomorphic

• newObjectsIsomorphic (PREDICATE)

newOnHeap

• newOnHeap (PREDICATE)

nonNull

• nonNull (PREDICATE)

objectIsomorphic

• objectIsomorphic (PREDICATE)

objectsIsomorphic

• objectsIsomorphic (PREDICATE)

prec

• prec (PREDICATE)

reach

• reach (PREDICATE)

sameType

• sameType (PREDICATE)

sameTypes

• sameTypes (PREDICATE)

ssubsort

• ssubsort (PREDICATE)

wellFormed

• wellFormed (PREDICATE)

wellOrderLeqInt

• wellOrderLeqInt (PREDICATE)

$classErroneous

• alphaObj (SORT)

$classInitializationInProgress

• alphaObj (SORT)

$classInitialized

• alphaObj (SORT)

$classPrepared

• alphaObj (SORT)

FALSE

• boolean (SORT)

TRUE

• boolean (SORT)

anon

• alphaObj (SORT)

anySORT

• alphSub (SORT)

arr

• alphaObj (SORT)

atom

• Free (SORT)

cast

• betaObj (SORT)

create

• alphaObj (SORT)

defaultValue

• alphaObj (SORT)

exactInstance

• betaObj (SORT)

final

• alphaObj (SORT)

first

• Pair (SORT)

instance

• betaObj (SORT)

length

• alphaObj (SORT)

mapForeach

• Map (SORT)

mapGet

• Map (SORT)

mapSize

• mapSize (FILE)

mapUndef

• Map (SORT)

memset

• alphaObj (SORT)

null

• alphaObj (SORT)

pair

• Pair (SORT)

second

• Pair (SORT)

select

• alphaObj (SORT)

ssort

• alphSub (SORT)

store

• alphaObj (SORT)

strContent

• java.lang.String (SORT)

strPool

• java.lang.String (SORT)

F

• F (TRANSFORMER)

T

• T (TRANSFORMER)

WD

• WD (TRANSFORMER)

wd

• wd (TRANSFORMER)

comprehensions

• definitionOfNewOnHeap (TACLET)

• definitionOfObjectIsomorphic (TACLET)

• definitionOfObjectsIsomorphic (TACLET)

• definitionOfSameTypes (TACLET)

concrete

• applySkip1 (TACLET)

• dropEffectlessStores (TACLET)

• firstOfPair (TACLET)

• hideAuxiliaryEq (TACLET)

• hideAuxiliaryEqConcrete (TACLET)

• hideAuxiliaryEqConcrete2 (TACLET)

• insert_constant_string_value (TACLET)

• instanceof_not_compatible (TACLET)

• instanceof_not_compatible_2 (TACLET)

• instanceof_not_compatible_3 (TACLET)

• instanceof_static_type (TACLET)

• instanceof_static_type_2 (TACLET)

• memsetEmpty (TACLET)

• nullString (TACLET)

• secondOfPair (TACLET)

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• wellFormedAnon (TACLET)

• wellFormedAnonEQ (TACLET)

• wellFormedCreate (TACLET)

• wellFormedStorePrimitive (TACLET)

• wellFormedStorePrimitiveArray (TACLET)

• wellFormedStorePrimitiveEQ (TACLET)

delayedExpansion

• assignableDefinition (TACLET)

evaluate_instanceof

• instanceof_not_compatible (TACLET)

• instanceof_not_compatible_2 (TACLET)

• instanceof_not_compatible_3 (TACLET)

• instanceof_static_type (TACLET)

• instanceof_static_type_2 (TACLET)

hide_auxiliary_eq

• hideAuxiliaryEq (TACLET)

hide_auxiliary_eq_const

• hideAuxiliaryEqConcrete (TACLET)

• hideAuxiliaryEqConcrete2 (TACLET)

inReachableStateImplication

• arrayLengthNotNegative (TACLET)

• onlyCreatedObjectsAreInLocSets (TACLET)

• onlyCreatedObjectsAreInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreInLocSetsEQFinal (TACLET)

• onlyCreatedObjectsAreInLocSetsFinal (TACLET)

• onlyCreatedObjectsAreObserved (TACLET)

• onlyCreatedObjectsAreObservedInLocSets (TACLET)

• onlyCreatedObjectsAreObservedInLocSetsEQ (TACLET)

• onlyCreatedObjectsAreReferenced (TACLET)

• onlyCreatedObjectsAreReferencedFinal (TACLET)

• only_created_objects_are_reachable (TACLET)

• reachEndOfUniquePath (TACLET)

• reachEndOfUniquePath2 (TACLET)

• reachUniquePathSameSteps (TACLET)

loopInvariant

• crossInst (TACLET)

• cutUpperBound (TACLET)

loop_expand

• forInitUnfold (TACLET)

• loopUnwind (TACLET)

loop_scope_expand

• unwindLoopScope (TACLET)

loop_scope_inv_taclet

• loopScopeInvBox (TACLET)

• loopScopeInvDia (TACLET)

• threeBranchLoopScopeInvRuleBox (TACLET)

• threeBranchLoopScopeInvRuleDia (TACLET)

method_expand

• allocateInstance (TACLET)

• allocateInstanceWithLength (TACLET)

• instanceCreation (TACLET)

• instanceCreationAssignment (TACLET)

• special_constructor_call (TACLET)

pull_out_select

• pullOutSelect (TACLET)

semantics_blasting

• equalityToSelect (TACLET)

• selectOfAnon (TACLET)

• selectOfCreate (TACLET)

• selectOfMemset (TACLET)

• selectOfStore (TACLET)

simplify

• accDefinition (TACLET)

• arrayInitialisation (TACLET)

• dismissNonSelectedField (TACLET)

• dismissNonSelectedFieldEQ (TACLET)

• exact_instance_definition_boolean (TACLET)

• exact_instance_definition_int (TACLET)

• exact_instance_definition_null (TACLET)

• exact_instance_for_interfaces_or_abstract_classes (TACLET)

• instance_for_final_types (TACLET)

• measuredByCheck (TACLET)

• narrowFinalArrayType (TACLET)

• narrowSelectArrayType (TACLET)

• narrowSelectType (TACLET)

• narrowTypeFinal (TACLET)

• poolIsInjective (TACLET)

• poolKeyIsContentOfValue (TACLET)

• precOfInt (TACLET)

• precOfIntPair (TACLET)

• precOfPair (TACLET)

• precOfPairInt (TACLET)

• reachAddOne (TACLET)

• reachAddOne2 (TACLET)

• reachDependenciesStoreSimple (TACLET)

• reachDependenciesStoreSimpleEQ (TACLET)

• reachDoesNotDependOnCreatedness (TACLET)

• reachNull (TACLET)

• reachNull2 (TACLET)

• reachOne (TACLET)

• reachZero (TACLET)

• reach_does_not_depend_on_fresh_locs (TACLET)

• reach_does_not_depend_on_fresh_locs_EQ (TACLET)

• wd_F_Logical_Op_And (TACLET)

• wd_F_Logical_Op_Cond_Form (TACLET)

• wd_F_Logical_Op_Eqv (TACLET)

• wd_F_Logical_Op_ExCond_Form (TACLET)

• wd_F_Logical_Op_Imp (TACLET)

• wd_F_Logical_Op_Neg (TACLET)

• wd_F_Logical_Op_Or (TACLET)

• wd_F_Logical_Quant_All (TACLET)

• wd_F_Logical_Quant_Exist (TACLET)

• wd_F_Resolve (TACLET)

• wd_Heap_Anon (TACLET)

• wd_Heap_ArrLength (TACLET)

• wd_Heap_Create (TACLET)

• wd_Heap_Memset (TACLET)

• wd_Heap_Pred_ArrStoreValid (TACLET)

• wd_Heap_Pred_NonNull (TACLET)

• wd_Heap_Pred_WellFormed (TACLET)

• wd_Heap_Reference (TACLET)

• wd_Heap_Reference_Array (TACLET)

• wd_Heap_Reference_Created (TACLET)

• wd_Heap_Reference_Static (TACLET)

• wd_Heap_Store (TACLET)

• wd_LocSet_AllElemsArr (TACLET)

• wd_LocSet_AllElemsArrLocsets (TACLET)

• wd_LocSet_AllFields (TACLET)

• wd_LocSet_AllFieldsArr (TACLET)

• wd_LocSet_AllObjects (TACLET)

• wd_LocSet_ArrRange (TACLET)

• wd_LocSet_Diff (TACLET)

• wd_LocSet_FreshLocs (TACLET)

• wd_LocSet_InfiniteUnion (TACLET)

• wd_LocSet_InfiniteUnion2 (TACLET)

• wd_LocSet_Intersect (TACLET)

• wd_LocSet_Pred_Disjoint (TACLET)

• wd_LocSet_Pred_ElementOf (TACLET)

• wd_LocSet_Pred_ElementOf_Static (TACLET)

• wd_LocSet_Pred_InHeap (TACLET)

• wd_LocSet_Pred_Subset (TACLET)

• wd_LocSet_Singleton (TACLET)

• wd_LocSet_Singleton_Arr (TACLET)

• wd_LocSet_Singleton_Quant (TACLET)

• wd_LocSet_Singleton_Static (TACLET)

• wd_LocSet_Union (TACLET)

• wd_Logical_Op_And (TACLET)

• wd_Logical_Op_AndSC (TACLET)

• wd_Logical_Op_Cond_Expr (TACLET)

• wd_Logical_Op_Cond_Form (TACLET)

• wd_Logical_Op_Eqv (TACLET)

• wd_Logical_Op_ExCond_Expr (TACLET)

• wd_Logical_Op_ExCond_Form (TACLET)

• wd_Logical_Op_Imp (TACLET)

• wd_Logical_Op_Neg (TACLET)

• wd_Logical_Op_Or (TACLET)

• wd_Logical_Op_OrSC (TACLET)

• wd_Logical_Quant_All (TACLET)

• wd_Logical_Quant_Exist (TACLET)

• wd_Reach_Pred_Acc (TACLET)

• wd_Reach_Pred_Reach (TACLET)

• wd_RegEx (TACLET)

• wd_RegEx_Alt (TACLET)

• wd_RegEx_Concat (TACLET)

• wd_RegEx_Opt (TACLET)

• wd_RegEx_Plus (TACLET)

• wd_RegEx_Pred_Match (TACLET)

• wd_RegEx_Repeat (TACLET)

• wd_RegEx_Star (TACLET)

• wd_Seq_Concat (TACLET)

• wd_Seq_Def (TACLET)

• wd_Seq_Get (TACLET)

• wd_Seq_IndexOf (TACLET)

• wd_Seq_Length (TACLET)

• wd_Seq_NPermInv (TACLET)

• wd_Seq_Pred_NPerm (TACLET)

• wd_Seq_Pred_Perm (TACLET)

• wd_Seq_Remove (TACLET)

• wd_Seq_Reverse (TACLET)

• wd_Seq_Singleton (TACLET)

• wd_Seq_Sub (TACLET)

• wd_Seq_Swap (TACLET)

• wd_String_Hash (TACLET)

• wd_String_IndexOfChar (TACLET)

• wd_String_IndexOfStr (TACLET)

• wd_String_LastIndexOfChar (TACLET)

• wd_String_LastIndexOfStr (TACLET)

• wd_String_Pred_Contains (TACLET)

• wd_String_Pred_EndsWith (TACLET)

• wd_String_Pred_StartsWith (TACLET)

• wd_String_Replace (TACLET)

• wd_String_RmvZeros (TACLET)

• wd_String_Translate (TACLET)

• wd_T_Logical_Op_And (TACLET)

• wd_T_Logical_Op_Cond_Form (TACLET)

• wd_T_Logical_Op_Eqv (TACLET)

• wd_T_Logical_Op_ExCond_Form (TACLET)

• wd_T_Logical_Op_Imp (TACLET)

• wd_T_Logical_Op_Neg (TACLET)

• wd_T_Logical_Op_Or (TACLET)

• wd_T_Logical_Quant_All (TACLET)

• wd_T_Logical_Quant_Exist (TACLET)

• wd_T_Resolve (TACLET)

• wd_Y_Split (TACLET)

simplify_ENLARGING

• selectCreatedOfAnonAsFormula (TACLET)

• selectCreatedOfAnonAsFormulaEQ (TACLET)

simplify_autoname

• instanceCreationAssignmentUnfoldArguments (TACLET)

• instanceCreationUnfoldArguments (TACLET)

simplify_enlarging

• definitionOfNewObjectsIsomorphic (TACLET)

• wellFormedMemsetArrayObject (TACLET)

• wellFormedMemsetArrayPrimitive (TACLET)

• wellFormedStoreArray (TACLET)

• wellFormedStoreLocSet (TACLET)

• wellFormedStoreLocSetEQ (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

simplify_expression

• activeUseAddition (TACLET)

• activeUseBitwiseAnd (TACLET)

• activeUseBitwiseNegation (TACLET)

• activeUseBitwiseOr (TACLET)

• activeUseBitwiseXOr (TACLET)

• activeUseByteCast (TACLET)

• activeUseCharCast (TACLET)

• activeUseDivision (TACLET)

• activeUseIntCast (TACLET)

• activeUseMinus (TACLET)

• activeUseModulo (TACLET)

• activeUseMultiplication (TACLET)

• activeUseShiftLeft (TACLET)

• activeUseShiftRight (TACLET)

• activeUseShortCast (TACLET)

• activeUseSubtraction (TACLET)

• activeUseUnaryMinus (TACLET)

• activeUseUnsignedShiftRight (TACLET)

simplify_heap_high_costs

• selectCreatedOfAnon (TACLET)

• selectCreatedOfAnonEQ (TACLET)

• selectOfAnonEQ (TACLET)

• selectOfCreateEQ (TACLET)

• selectOfMemsetEQ (TACLET)

• selectOfStoreEQ (TACLET)

simplify_prog

• abortJavaCardTransactionAPI (TACLET)

• abortJavaCardTransactionBox (TACLET)

• abortJavaCardTransactionDiamond (TACLET)

• activeUseStaticFieldReadAccess (TACLET)

• activeUseStaticFieldReadAccess2 (TACLET)

• activeUseStaticFieldWriteAccess (TACLET)

• activeUseStaticFieldWriteAccess2 (TACLET)

• activeUseStaticFieldWriteAccess3 (TACLET)

• activeUseStaticFieldWriteAccess4 (TACLET)

• activeUseStaticFieldWriteAccess5 (TACLET)

• activeUseStaticFieldWriteAccess6 (TACLET)

• allFieldsUnfold (TACLET)

• allObjectsAssignment (TACLET)

• arrayCreation (TACLET)

• arrayCreationWithInitializers (TACLET)

• assert (TACLET)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assertWithPrimitiveMessage (TACLET)

• assertWithReferenceMessage (TACLET)

• assertWithReferenceMessageNull (TACLET)

• beginJavaCardTransactionAPI (TACLET)

• beginJavaCardTransactionBox (TACLET)

• beginJavaCardTransactionDiamond (TACLET)

• blockBreak (TACLET)

• blockBreakLabeled (TACLET)

• blockContinue (TACLET)

• blockContinueLabeled (TACLET)

• commitJavaCardTransactionAPI (TACLET)

• commitJavaCardTransactionBox (TACLET)

• commitJavaCardTransactionDiamond (TACLET)

• doWhileUnwind (TACLET)

• emptyModality (TACLET)

• enhancedfor_iterable (TACLET)

• evaluateAssertCondition_1 (TACLET)

• evaluateAssertCondition_2 (TACLET)

• evaluateAssertMessage (TACLET)

• execBreak (TACLET)

• execBreakEliminateBreakLabel (TACLET)

• execBreakEliminateBreakLabelWildcard (TACLET)

• execBreakEliminateContinue (TACLET)

• execBreakEliminateContinueLabel (TACLET)

• execBreakEliminateContinueLabelWildcard (TACLET)

• execBreakEliminateExcCcatch (TACLET)

• execBreakEliminateReturn (TACLET)

• execBreakEliminateReturnVal (TACLET)

• execBreakLabelEliminateBreak (TACLET)

• execBreakLabelEliminateBreakLabelNoMatch (TACLET)

• execBreakLabelEliminateContinue (TACLET)

• execBreakLabelEliminateContinueLabel (TACLET)

• execBreakLabelEliminateContinueLabelWildcard (TACLET)

• execBreakLabelEliminateExcCcatch (TACLET)

• execBreakLabelEliminateReturn (TACLET)

• execBreakLabelEliminateReturnVal (TACLET)

• execBreakLabelMatch (TACLET)

• execBreakLabelWildcard (TACLET)

• execCatchThrow (TACLET)

• execContinue (TACLET)

• execContinueEliminateBreak (TACLET)

• execContinueEliminateBreakLabel (TACLET)

• execContinueEliminateBreakLabelWildcard (TACLET)

• execContinueEliminateExcCcatch (TACLET)

• execContinueEliminateReturn (TACLET)

• execContinueEliminateReturnVal (TACLET)

• execContinueLabelEliminateBreak (TACLET)

• execContinueLabelEliminateBreakLabel (TACLET)

• execContinueLabelEliminateBreakLabelWildcard (TACLET)

• execContinueLabelEliminateContinue (TACLET)

• execContinueLabelEliminateContinueLabelNoMatch (TACLET)

• execContinueLabelEliminateExcCcatch (TACLET)

• execContinueLabelEliminateReturn (TACLET)

• execContinueLabelEliminateReturnVal (TACLET)

• execContinueLabelMatch (TACLET)

• execContinueLabelWildcard (TACLET)

• execEmpty (TACLET)

• execMultipleCatchThrow (TACLET)

• execNoCcatch (TACLET)

• execReturn (TACLET)

• execReturnEliminateBreak (TACLET)

• execReturnEliminateBreakLabel (TACLET)

• execReturnEliminateBreakLabelWildcard (TACLET)

• execReturnEliminateContinue (TACLET)

• execReturnEliminateContinueLabel (TACLET)

• execReturnEliminateContinueLabelWildcard (TACLET)

• execReturnEliminateExcCcatch (TACLET)

• execReturnEliminateReturnVal (TACLET)

• execReturnVal (TACLET)

• execReturnValEliminateBreak (TACLET)

• execReturnValEliminateBreakLabel (TACLET)

• execReturnValEliminateBreakLabelWildcard (TACLET)

• execReturnValEliminateContinue (TACLET)

• execReturnValEliminateContinueLabel (TACLET)

• execReturnValEliminateContinueLabelWildcard (TACLET)

• execReturnValEliminateExcCcatch (TACLET)

• execReturnValEliminateReturn (TACLET)

• execReturnValNonMatchingType (TACLET)

• execThrowEliminateBreak (TACLET)

• execThrowEliminateBreakLabel (TACLET)

• execThrowEliminateBreakLabelWildcard (TACLET)

• execThrowEliminateContinue (TACLET)

• execThrowEliminateContinueLabel (TACLET)

• execThrowEliminateContinueLabelWildcard (TACLET)

• execThrowEliminateReturn (TACLET)

• execThrowEliminateReturnVal (TACLET)

• finishJavaCardTransactionBox (TACLET)

• finishJavaCardTransactionDiamond (TACLET)

• for_to_while (TACLET)

• getJavaCardTransient (TACLET)

• lsBreak (TACLET)

• lsContinue (TACLET)

• lsLblBreak (TACLET)

• lsLblContinueMatch (TACLET)

• lsLblContinueNoMatch1 (TACLET)

• lsLblContinueNoMatch2 (TACLET)

• lsReturnNonVoid (TACLET)

• lsReturnVoid (TACLET)

• lsThrow (TACLET)

• seqConcatUnfoldLeft (TACLET)

• seqConcatUnfoldRight (TACLET)

• seqGetUnfoldLeft (TACLET)

• seqGetUnfoldRight (TACLET)

• seqIndexOfUnfoldLeft (TACLET)

• seqIndexOfUnfoldRight (TACLET)

• seqLengthUnfold (TACLET)

• seqReverseUnfold (TACLET)

• seqSingletonUnfold (TACLET)

• seqSubUnfoldLeft (TACLET)

• seqSubUnfoldMiddle (TACLET)

• seqSubUnfoldRight (TACLET)

• setIntersectUnfoldLeft (TACLET)

• setIntersectUnfoldRight (TACLET)

• setJavaCardTransient (TACLET)

• setMinusUnfoldLeft (TACLET)

• setMinusUnfoldRight (TACLET)

• setUnionUnfoldLeft (TACLET)

• setUnionUnfoldRight (TACLET)

• singletonAssignment (TACLET)

• singletonUnfold (TACLET)

• skipAssert (TACLET)

• skipAssert_2 (TACLET)

• stringAssignment (TACLET)

• stringConcat (TACLET)

• stringConcatBooleanLeft (TACLET)

• stringConcatBooleanRight (TACLET)

• stringConcatCharExpLeft (TACLET)

• stringConcatCharExpRight (TACLET)

• stringConcatIntExpLeft (TACLET)

• stringConcatIntExpRight (TACLET)

• stringConcatObjectLeft (TACLET)

• stringConcatObjectRight (TACLET)

simplify_prog_subset

• activeUseStaticFieldReadAccess (TACLET)

• activeUseStaticFieldReadAccess2 (TACLET)

• activeUseStaticFieldWriteAccess (TACLET)

• activeUseStaticFieldWriteAccess2 (TACLET)

• activeUseStaticFieldWriteAccess3 (TACLET)

• activeUseStaticFieldWriteAccess4 (TACLET)

• activeUseStaticFieldWriteAccess5 (TACLET)

• activeUseStaticFieldWriteAccess6 (TACLET)

• stringAssignment (TACLET)

• stringConcat (TACLET)

• stringConcatBooleanLeft (TACLET)

• stringConcatBooleanRight (TACLET)

• stringConcatCharExpLeft (TACLET)

• stringConcatCharExpRight (TACLET)

• stringConcatIntExpLeft (TACLET)

• stringConcatIntExpRight (TACLET)

• stringConcatObjectLeft (TACLET)

• stringConcatObjectRight (TACLET)

simplify_select

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

update_apply

• applyOnRigidFormula (TACLET)

• applyOnRigidTerm (TACLET)

update_apply_on_update

• applyOnElementary (TACLET)

• applyOnParallel (TACLET)

update_elim

• applyOnPV (TACLET)

• applyOnSkip (TACLET)

• applySkip2 (TACLET)

• applySkip3 (TACLET)

• parallelWithSkip1 (TACLET)

• parallelWithSkip2 (TACLET)

• simplifyUpdate1 (TACLET)

• simplifyUpdate2 (TACLET)

• simplifyUpdate3 (TACLET)

update_join

• sequentialToParallel1 (TACLET)

• sequentialToParallel2 (TACLET)

• sequentialToParallel3 (TACLET)