C

• CSub (SORT)

• castAdd (TACLET)

• castAdd2 (TACLET)

• castDel (TACLET)

• castDel2 (TACLET)

• castType (TACLET)

• castType2 (TACLET)

• ineffectiveCast2 (TACLET)

CSub

• castAdd (TACLET)

• castDel2 (TACLET)

• castType (TACLET)

• castType2 (TACLET)

• ineffectiveCast2 (TACLET)

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)

• array_self_reference (TACLET)

• array_self_reference_eq (TACLET)

• assignment_array2 (TACLET)

• assignment_read_attribute (TACLET)

• assignment_read_attribute_final (TACLET)

• assignment_read_attribute_this (TACLET)

• assignment_read_attribute_this_final (TACLET)

• assignment_read_static_attribute (TACLET)

• assignment_read_static_attribute_final (TACLET)

• assignment_read_static_attribute_with_variable_prefix (TACLET)

• castAdd2 (TACLET)

• castDel2 (TACLET)

• closeType (TACLET)

• closeTypeSwitched (TACLET)

• delete_unnecessary_cast (TACLET)

• dynamic_type_for_null (TACLET)

• exact_instance_for_interfaces_or_abstract_classes (TACLET)

• exact_instance_known_dynamic_type (TACLET)

• ineffectiveCast2 (TACLET)

• instanceof_known_dynamic_type (TACLET)

• instanceof_known_dynamic_type_2 (TACLET)

• instanceof_not_compatible (TACLET)

• instanceof_not_compatible_2 (TACLET)

• instanceof_not_compatible_3 (TACLET)

• instanceof_not_compatible_4 (TACLET)

• instanceof_not_compatible_5 (TACLET)

• instanceof_static_type (TACLET)

• instanceof_static_type_2 (TACLET)

• reference_type_cast (TACLET)

• sameTypeFalse (TACLET)

• sameTypeTrue (TACLET)

• sortsDisjoint1 (TACLET)

• sortsDisjoint2 (TACLET)

• sortsDisjointModuloNull (TACLET)

• typeEq (TACLET)

• typeEqDerived2 (TACLET)

• typeStatic (TACLET)

GSub

• closeType (TACLET)

• closeTypeSwitched (TACLET)

H

• castType (TACLET)

• castType2 (TACLET)

• exact_instance_known_dynamic_type (TACLET)

• ineffectiveCast (TACLET)

• ineffectiveCast3 (TACLET)

• instanceof_known_dynamic_type (TACLET)

• instanceof_known_dynamic_type_2 (TACLET)

• instanceof_not_compatible_5 (TACLET)

• sameTypeFalse (TACLET)

• sortsDisjoint1 (TACLET)

• sortsDisjoint2 (TACLET)

• sortsDisjointModuloNull (TACLET)

• typeEq (TACLET)

• typeEqDerived (TACLET)

Heap

• acc (PREDICATE)

• accDefinition (TACLET)

• alphaObj (SORT)

• array_self_reference (TACLET)

• array_self_reference_eq (TACLET)

• 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 (TACLET)

• nonNull (PREDICATE)

• nonNullZero (TACLET)

• nullCreated (TACLET)

• nullIsNotNonNull (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

• array_store_known_dynamic_array_type (TACLET)

• instance_for_final_types (TACLET)

Map

• Map (SORT)

• inDomain (PREDICATE)

• inDomainImpliesCreated (PREDICATE)

• isFinite (PREDICATE)

• mapSize (FILE)

Pair

• Pair (SORT)

SORT

• alphSub (SORT)

• ssubsort (PREDICATE)

• ssubsortTop (TACLET)

• subsortTrans (TACLET)

alph

• alphSub (SORT)

• ssubsortDirect (TACLET)

• ssubsortSup (TACLET)

alphSub

• ssubsortDirect (TACLET)

• ssubsortSup (TACLET)

alpha

• alphaObj (SORT)

• betaObj (SORT)

• dismissNonSelectedField (TACLET)

• dismissNonSelectedFieldEQ (TACLET)

• getOfMapForeach (TACLET)

• inDomainOfMapForeach (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)

• wd_Type_Cast (TACLET)

• wd_Type_ExactInstance (TACLET)

• wd_Type_Instance (TACLET)

• wellFormedStoreObject (TACLET)

• wellFormedStoreObjectEQ (TACLET)

alphaObj

• allocateInstance (TACLET)

• allocateInstanceWithLength (TACLET)

• class_being_initialized_is_prepared (TACLET)

• class_erroneous_excludes_class_in_init (TACLET)

• class_initialized_excludes_class_init_in_progress (TACLET)

• erroneous_class_has_no_initialized_sub_class (TACLET)

• initialized_class_is_not_erroneous (TACLET)

• initialized_class_is_prepared (TACLET)

• superclasses_of_initialized_classes_are_initialized (TACLET)

• superclasses_of_initialized_classes_are_prepared (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)

• defMapSingleton (TACLET)

• defSeq2Map (TACLET)

• definitionOfNewOnHeap (TACLET)

• definitionOfObjectIsomorphic (TACLET)

• definitionOfObjectsIsomorphic (TACLET)

• definitionOfSameTypes (TACLET)

• dismissNonSelectedField (TACLET)

• dismissNonSelectedFieldEQ (TACLET)

• dropEffectlessStores (TACLET)

• equalityToSelect (TACLET)

• exact_instance_known_dynamic_type (TACLET)

• getOfSeq2Map (TACLET)

• hideAuxiliaryEq (TACLET)

• hideAuxiliaryEqConcrete (TACLET)

• hideAuxiliaryEqConcrete2 (TACLET)

• inDomain (PREDICATE)

• instance_for_final_types (TACLET)

• instanceof_known_dynamic_type (TACLET)

• instanceof_known_dynamic_type_2 (TACLET)

• instanceof_not_compatible (TACLET)

• instanceof_not_compatible_2 (TACLET)

• instanceof_not_compatible_3 (TACLET)

• instanceof_not_compatible_4 (TACLET)

• instanceof_not_compatible_5 (TACLET)

• instanceof_static_type (TACLET)

• instanceof_static_type_2 (TACLET)

• loopScopeInvDia (TACLET)

• measuredBy (PREDICATE)

• measuredByCheck (PREDICATE)

• measuredByCheck (TACLET)

• measuredByCheckEmpty (TACLET)

• memsetEmpty (TACLET)

• observerDependency (TACLET)

• observerDependencyEQ (TACLET)

• prec (PREDICATE)

• precOfIntPair (TACLET)

• precOfPair (TACLET)

• precOfPairInt (TACLET)

• precOfSeq (TACLET)

• reachDependenciesStore (TACLET)

• reachDependenciesStoreEQ (TACLET)

• reachDependenciesStoreSimple (TACLET)

• reachDependenciesStoreSimpleEQ (TACLET)

• sameType (PREDICATE)

• sameTypeFalse (TACLET)

• 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)

betaObj

• erroneous_class_has_no_initialized_sub_class (TACLET)

• superclasses_of_initialized_classes_are_initialized (TACLET)

• superclasses_of_initialized_classes_are_prepared (TACLET)

boolean

• Map (SORT)

• all_bool (TACLET)

• allocateInstance (TACLET)

• allocateInstanceWithLength (TACLET)

• apply_eq_boolean_rigid (TACLET)

• apply_eq_boolean_rigid_2 (TACLET)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assignableDefinition (TACLET)

• assignment_to_primitive_array_component_transaction (TACLET)

• assignment_to_reference_array_component_transaction (TACLET)

• betaObj (SORT)

• boolean (SORT)

• castTrueImpliesOriginalTrue (TACLET)

• class_being_initialized_is_prepared (TACLET)

• class_erroneous_excludes_class_in_init (TACLET)

• class_initialized_excludes_class_init_in_progress (TACLET)

• defInDomainImpliesCreated (TACLET)

• definitionOfNewOnHeap (TACLET)

• erroneous_class_has_no_initialized_sub_class (TACLET)

• ex_bool (TACLET)

• exact_instance_definition_boolean (TACLET)

• ifthenelse_equals_1 (TACLET)

• ifthenelse_equals_2 (TACLET)

• initialized_class_is_not_erroneous (TACLET)

• initialized_class_is_prepared (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)

• superclasses_of_initialized_classes_are_initialized (TACLET)

• superclasses_of_initialized_classes_are_prepared (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)

• alphaObj (SORT)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assignableDefinition (TACLET)

• assignment_to_primitive_array_component_transaction (TACLET)

• assignment_to_reference_array_component_transaction (TACLET)

• defInDomainImpliesCreated (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)

inDomain

• inDomain (PREDICATE)

inDomainImpliesCreated

• inDomainImpliesCreated (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)

mapEmpty

• Map (SORT)

mapForeach

• Map (SORT)

mapGet

• Map (SORT)

mapOverride

• Map (SORT)

mapRemove

• Map (SORT)

mapSingleton

• Map (SORT)

mapSize

• mapSize (FILE)

mapUndef

• Map (SORT)

mapUpdate

• Map (SORT)

memset

• alphaObj (SORT)

null

• alphaObj (SORT)

pair

• Pair (SORT)

second

• Pair (SORT)

select

• alphaObj (SORT)

seq2map

• Map (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)

apply_equations

• apply_eq_boolean (TACLET)

• apply_eq_boolean_2 (TACLET)

• apply_eq_boolean_rigid (TACLET)

• apply_eq_boolean_rigid_2 (TACLET)

boolean_cases

• all_bool (TACLET)

• ex_bool (TACLET)

boxDiamondConv

• boxToDiamond (TACLET)

• boxToDiamondTransaction (TACLET)

• diamondToBox (TACLET)

• diamondToBoxTransaction (TACLET)

cast_deletion

• castDel (TACLET)

closure

• closeType (TACLET)

• closeTypeSwitched (TACLET)

comprehensions

• definitionOfNewOnHeap (TACLET)

• definitionOfObjectIsomorphic (TACLET)

• definitionOfObjectsIsomorphic (TACLET)

• definitionOfSameTypes (TACLET)

concrete

• applySkip1 (TACLET)

• boolean_equal (TACLET)

• boolean_equal_2 (TACLET)

• boolean_not_equal_1 (TACLET)

• boolean_not_equal_2 (TACLET)

• castTrueImpliesOriginalTrue (TACLET)

• dropEffectlessStores (TACLET)

• dynamic_type_for_null (TACLET)

• false_to_not_true (TACLET)

• firstOfPair (TACLET)

• hideAuxiliaryEq (TACLET)

• hideAuxiliaryEqConcrete (TACLET)

• hideAuxiliaryEqConcrete2 (TACLET)

• ifExthenelse1_eq (TACLET)

• ifExthenelse1_eq2 (TACLET)

• ifExthenelse1_eq2_for (TACLET)

• ifExthenelse1_eq2_for_phi (TACLET)

• ifExthenelse1_eq2_phi (TACLET)

• ifExthenelse1_eq_for (TACLET)

• ifExthenelse1_eq_for_phi (TACLET)

• ifExthenelse1_eq_phi (TACLET)

• ifExthenelse1_false (TACLET)

• ifExthenelse1_false_for (TACLET)

• ifExthenelse1_min (TACLET)

• ifExthenelse1_min_for (TACLET)

• ifthenelse_concrete (TACLET)

• ifthenelse_concrete2 (TACLET)

• ifthenelse_concrete3 (TACLET)

• ifthenelse_concrete4 (TACLET)

• ifthenelse_equals (TACLET)

• ifthenelse_false (TACLET)

• ifthenelse_false_for (TACLET)

• ifthenelse_same_branches (TACLET)

• ifthenelse_same_branches_for (TACLET)

• ifthenelse_true (TACLET)

• ifthenelse_true_for (TACLET)

• inDomainOfMapEmpty (TACLET)

• insert_constant_string_value (TACLET)

• instanceof_not_compatible (TACLET)

• instanceof_not_compatible_2 (TACLET)

• instanceof_not_compatible_3 (TACLET)

• instanceof_not_compatible_4 (TACLET)

• instanceof_not_compatible_5 (TACLET)

• instanceof_static_type (TACLET)

• instanceof_static_type_2 (TACLET)

• memsetEmpty (TACLET)

• nonNullZero (TACLET)

• nullIsNotNonNull (TACLET)

• nullString (TACLET)

• sameTypeFalse (TACLET)

• sameTypeTrue (TACLET)

• secondOfPair (TACLET)

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

• sortsDisjoint1 (TACLET)

• sortsDisjoint2 (TACLET)

• typeEqDerived (TACLET)

• typeEqDerived2 (TACLET)

• wellFormedAnon (TACLET)

• wellFormedAnonEQ (TACLET)

• wellFormedCreate (TACLET)

• wellFormedStorePrimitive (TACLET)

• wellFormedStorePrimitiveArray (TACLET)

• wellFormedStorePrimitiveEQ (TACLET)

concrete_java

• insert_constant_value (TACLET)

confluence_restricted

• class_being_initialized_is_prepared (TACLET)

• class_erroneous_excludes_class_in_init (TACLET)

• class_initialized_excludes_class_init_in_progress (TACLET)

• erroneous_class_has_no_initialized_sub_class (TACLET)

• initialized_class_is_not_erroneous (TACLET)

• initialized_class_is_prepared (TACLET)

delayedExpansion

• assignableDefinition (TACLET)

evaluate_instanceof

• exact_instance_known_dynamic_type (TACLET)

• instanceof_known_dynamic_type (TACLET)

• instanceof_known_dynamic_type_2 (TACLET)

• instanceof_not_compatible (TACLET)

• instanceof_not_compatible_2 (TACLET)

• instanceof_not_compatible_3 (TACLET)

• instanceof_not_compatible_4 (TACLET)

• instanceof_not_compatible_5 (TACLET)

• instanceof_static_type (TACLET)

• instanceof_static_type_2 (TACLET)

hide_auxiliary_eq

• hideAuxiliaryEq (TACLET)

hide_auxiliary_eq_const

• hideAuxiliaryEqConcrete (TACLET)

• hideAuxiliaryEqConcrete2 (TACLET)

inReachableStateImplication

• arrayLengthIsAShort (TACLET)

• arrayLengthIsAnInt (TACLET)

• arrayLengthNotNegative (TACLET)

• inDomainConcrete (TACLET)

• ineffectiveCast (TACLET)

• ineffectiveCast2 (TACLET)

• ineffectiveCast3 (TACLET)

• mapSizeNotNegativeForFiniteMaps (TACLET)

• notInDomain (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)

• sizeOfMapRemove (TACLET)

• sizeOfMapUpdate (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)

merge_point

• deleteMergePoint (TACLET)

method_expand

• allocateInstance (TACLET)

• allocateInstanceWithLength (TACLET)

• instanceCreation (TACLET)

• instanceCreationAssignment (TACLET)

• methodCall (TACLET)

• methodCallSuper (TACLET)

• methodCallWithAssignment (TACLET)

• methodCallWithAssignmentSuper (TACLET)

• methodCallWithAssignmentWithinClass (TACLET)

• methodCallWithinClass (TACLET)

• passiveMethodCallStatic (TACLET)

• passiveMethodCallStaticWithAssignment (TACLET)

• passiveMethodCallWithAssignmentWithinClass (TACLET)

• passiveMethodCallWithinClass (TACLET)

• special_constructor_call (TACLET)

• staticMethodCall (TACLET)

• staticMethodCallStaticViaTypereference (TACLET)

• staticMethodCallStaticWithAssignmentViaTypereference (TACLET)

• staticMethodCallWithAssignment (TACLET)

modal_tautology

• box_true (TACLET)

• diamond_false (TACLET)

obsolete

• equality_comparison_new (TACLET)

• greater_equal_than_comparison_new (TACLET)

• greater_than_comparison_new (TACLET)

• inequality_comparison_new (TACLET)

• less_equal_than_comparison_new (TACLET)

• less_than_comparison_new (TACLET)

pull_out_select

• pullOutSelect (TACLET)

semantics_blasting

• equalityToSelect (TACLET)

• selectOfAnon (TACLET)

• selectOfCreate (TACLET)

• selectOfMemset (TACLET)

• selectOfStore (TACLET)

simplify

• accDefinition (TACLET)

• arrayInitialisation (TACLET)

• castDel (TACLET)

• castType (TACLET)

• castType2 (TACLET)

• def_wellOrderLeqInt (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)

• exact_instance_known_dynamic_type (TACLET)

• getOfMapEmpty (TACLET)

• getOfMapSingleton (TACLET)

• ifExthenelse1_unused_var (TACLET)

• ifExthenelse1_unused_var_for (TACLET)

• ifthenelse_negated (TACLET)

• ifthenelse_negated_for (TACLET)

• inDomainOfMapForeach (TACLET)

• inDomainOfMapOverride (TACLET)

• inDomainOfMapSingleton (TACLET)

• inDomainOfSeq2Map (TACLET)

• instance_for_final_types (TACLET)

• instanceof_known_dynamic_type (TACLET)

• instanceof_known_dynamic_type_2 (TACLET)

• isFiniteOfMapEmpty (TACLET)

• isFiniteOfMapRemove (TACLET)

• isFiniteOfMapSingleton (TACLET)

• isFiniteOfMapUpdate (TACLET)

• isFiniteOfSeq2Map (TACLET)

• measuredByCheck (TACLET)

• measuredByCheckEmpty (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)

• sizeOfMapEmpty (TACLET)

• sizeOfMapSingleton (TACLET)

• sizeOfSeq2Map (TACLET)

• sortsDisjointModuloNull (TACLET)

• ssubsortDirect (TACLET)

• ssubsortSup (TACLET)

• ssubsortTop (TACLET)

• typeEqDerived (TACLET)

• typeEqDerived2 (TACLET)

• wd_Constant_Formula (TACLET)

• wd_Constant_Term (TACLET)

• wd_Equality_Pred (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_F_Subst_Formula (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_Numerical_Cast_Byte (TACLET)

• wd_Numerical_Cast_ByteOverFlow (TACLET)

• wd_Numerical_Cast_Char (TACLET)

• wd_Numerical_Cast_CharOverFlow (TACLET)

• wd_Numerical_Cast_Int (TACLET)

• wd_Numerical_Cast_IntOverFlow (TACLET)

• wd_Numerical_Cast_Long (TACLET)

• wd_Numerical_Cast_LongOverFlow (TACLET)

• wd_Numerical_Cast_Short (TACLET)

• wd_Numerical_Cast_ShortOverFlow (TACLET)

• wd_Numerical_Const (TACLET)

• wd_Numerical_Const_C (TACLET)

• wd_Numerical_Const_Z (TACLET)

• wd_Numerical_Mod_Byte (TACLET)

• wd_Numerical_Mod_Char (TACLET)

• wd_Numerical_Mod_Int (TACLET)

• wd_Numerical_Mod_Long (TACLET)

• wd_Numerical_Mod_Short (TACLET)

• wd_Numerical_Op_Add (TACLET)

• wd_Numerical_Op_AddInt (TACLET)

• wd_Numerical_Op_AddIntOverFlow (TACLET)

• wd_Numerical_Op_AddJInt (TACLET)

• wd_Numerical_Op_AddJLong (TACLET)

• wd_Numerical_Op_AddLong (TACLET)

• wd_Numerical_Op_AddLongOverFlow (TACLET)

• wd_Numerical_Op_AndJInt (TACLET)

• wd_Numerical_Op_AndJLong (TACLET)

• wd_Numerical_Op_BitAndInt (TACLET)

• wd_Numerical_Op_BitAndLong (TACLET)

• wd_Numerical_Op_BitNegInt (TACLET)

• wd_Numerical_Op_BitNegLong (TACLET)

• wd_Numerical_Op_BitOrInt (TACLET)

• wd_Numerical_Op_BitOrLong (TACLET)

• wd_Numerical_Op_BitXOrInt (TACLET)

• wd_Numerical_Op_BitXOrLong (TACLET)

• wd_Numerical_Op_CheckedAddInt (TACLET)

• wd_Numerical_Op_CheckedAddLong (TACLET)

• wd_Numerical_Op_CheckedBitNegInt (TACLET)

• wd_Numerical_Op_CheckedBitNegLong (TACLET)

• wd_Numerical_Op_CheckedBitwiseAndInt (TACLET)

• wd_Numerical_Op_CheckedBitwiseOrInt (TACLET)

• wd_Numerical_Op_CheckedBitwiseOrLong (TACLET)

• wd_Numerical_Op_CheckedBitwiseXOrInt (TACLET)

• wd_Numerical_Op_CheckedBitwiseXOrLong (TACLET)

• wd_Numerical_Op_CheckedDivInt (TACLET)

• wd_Numerical_Op_CheckedDivLong (TACLET)

• wd_Numerical_Op_CheckedMinusInt (TACLET)

• wd_Numerical_Op_CheckedMinusLong (TACLET)

• wd_Numerical_Op_CheckedMulInt (TACLET)

• wd_Numerical_Op_CheckedMulLong (TACLET)

• wd_Numerical_Op_CheckedShiftLeftInt (TACLET)

• wd_Numerical_Op_CheckedShiftLeftLong (TACLET)

• wd_Numerical_Op_CheckedShiftRightInt (TACLET)

• wd_Numerical_Op_CheckedShiftRightLong (TACLET)

• wd_Numerical_Op_CheckedSubInt (TACLET)

• wd_Numerical_Op_CheckedSubLong (TACLET)

• wd_Numerical_Op_CheckedUShiftRightInt (TACLET)

• wd_Numerical_Op_CheckedUShiftRightLong (TACLET)

• wd_Numerical_Op_Div (TACLET)

• wd_Numerical_Op_DivInt (TACLET)

• wd_Numerical_Op_DivIntOverFlow (TACLET)

• wd_Numerical_Op_DivJInt (TACLET)

• wd_Numerical_Op_DivJLong (TACLET)

• wd_Numerical_Op_DivLong (TACLET)

• wd_Numerical_Op_DivLongOverFlow (TACLET)

• wd_Numerical_Op_JDiv (TACLET)

• wd_Numerical_Op_JMod (TACLET)

• wd_Numerical_Op_JavaMod (TACLET)

• wd_Numerical_Op_JavaModOverFlow (TACLET)

• wd_Numerical_Op_JavaShiftLeftInt (TACLET)

• wd_Numerical_Op_JavaShiftLeftLong (TACLET)

• wd_Numerical_Op_JavaShiftRightInt (TACLET)

• wd_Numerical_Op_JavaShiftRightLong (TACLET)

• wd_Numerical_Op_JavaUnsignedShiftRightInt (TACLET)

• wd_Numerical_Op_JavaUnsignedShiftRightLong (TACLET)

• wd_Numerical_Op_MinusInt (TACLET)

• wd_Numerical_Op_MinusIntOverFlow (TACLET)

• wd_Numerical_Op_MinusJInt (TACLET)

• wd_Numerical_Op_MinusJLong (TACLET)

• wd_Numerical_Op_MinusLong (TACLET)

• wd_Numerical_Op_MinusLongOverFlow (TACLET)

• wd_Numerical_Op_Mod (TACLET)

• wd_Numerical_Op_ModJInt (TACLET)

• wd_Numerical_Op_ModJLong (TACLET)

• wd_Numerical_Op_Mul (TACLET)

• wd_Numerical_Op_MulInt (TACLET)

• wd_Numerical_Op_MulIntOverFlow (TACLET)

• wd_Numerical_Op_MulJInt (TACLET)

• wd_Numerical_Op_MulJLong (TACLET)

• wd_Numerical_Op_MulLong (TACLET)

• wd_Numerical_Op_MulLongOverFlow (TACLET)

• wd_Numerical_Op_Neg (TACLET)

• wd_Numerical_Op_OrJInt (TACLET)

• wd_Numerical_Op_OrJLong (TACLET)

• wd_Numerical_Op_ShiftLeftInt (TACLET)

• wd_Numerical_Op_ShiftLeftLong (TACLET)

• wd_Numerical_Op_ShiftRightInt (TACLET)

• wd_Numerical_Op_ShiftRightLong (TACLET)

• wd_Numerical_Op_Sub (TACLET)

• wd_Numerical_Op_SubInt (TACLET)

• wd_Numerical_Op_SubIntOverFlow (TACLET)

• wd_Numerical_Op_SubJInt (TACLET)

• wd_Numerical_Op_SubJLong (TACLET)

• wd_Numerical_Op_SubLong (TACLET)

• wd_Numerical_Op_SubLongOverFlow (TACLET)

• wd_Numerical_Op_UShiftRightInt (TACLET)

• wd_Numerical_Op_UShiftRightLong (TACLET)

• wd_Numerical_Op_XorJInt (TACLET)

• wd_Numerical_Op_XorJLong (TACLET)

• wd_Numerical_Op_checkedBitwiseAndLong (TACLET)

• wd_Numerical_Pred_Geq (TACLET)

• wd_Numerical_Pred_Gt (TACLET)

• wd_Numerical_Pred_InByte (TACLET)

• wd_Numerical_Pred_InChar (TACLET)

• wd_Numerical_Pred_InInt (TACLET)

• wd_Numerical_Pred_InLong (TACLET)

• wd_Numerical_Pred_InShort (TACLET)

• wd_Numerical_Pred_Leq (TACLET)

• wd_Numerical_Pred_Lt (TACLET)

• wd_Numerical_Pred_WellOrdered (TACLET)

• wd_Numerical_Pred_inRangeByte (TACLET)

• wd_Numerical_Pred_inRangeChar (TACLET)

• wd_Numerical_Pred_inRangeInt (TACLET)

• wd_Numerical_Pred_inRangeLong (TACLET)

• wd_Numerical_Pred_inRangeShort (TACLET)

• wd_Numerical_Quant_Bprod (TACLET)

• wd_Numerical_Quant_Bsum (TACLET)

• wd_Numerical_Quant_Max (TACLET)

• wd_Numerical_Quant_Min (TACLET)

• wd_Numerical_Quant_Prod (TACLET)

• wd_Numerical_Quant_Sum (TACLET)

• wd_Pair (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_Subst_Formula (TACLET)

• wd_Subst_Term (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_T_Subst_Formula (TACLET)

• wd_Type_Cast (TACLET)

• wd_Type_ExactInstance (TACLET)

• wd_Type_Instance (TACLET)

• wd_Undef_Formula (TACLET)

• wd_Undef_Term (TACLET)

• wd_Y_Split (TACLET)

simplify_ENLARGING

• selectCreatedOfAnonAsFormula (TACLET)

• selectCreatedOfAnonAsFormulaEQ (TACLET)

simplify_autoname

• ifElseUnfold (TACLET)

• ifUnfold (TACLET)

• instanceCreationAssignmentUnfoldArguments (TACLET)

• instanceCreationUnfoldArguments (TACLET)

• instanceof_eval (TACLET)

• methodCallSuper (TACLET)

• methodCallUnfoldArguments (TACLET)

• methodCallUnfoldTarget (TACLET)

• methodCallWithAssignmentSuper (TACLET)

• methodCallWithAssignmentUnfoldArguments (TACLET)

• methodCallWithAssignmentUnfoldTarget (TACLET)

simplify_boolean

• boolean_equal (TACLET)

• boolean_equal_2 (TACLET)

• boolean_false_commute (TACLET)

• boolean_not_equal_1 (TACLET)

• boolean_not_equal_2 (TACLET)

• boolean_true_commute (TACLET)

• false_to_not_true (TACLET)

simplify_enlarging

• defInDomainImpliesCreated (TACLET)

• definitionOfNewObjectsIsomorphic (TACLET)

• getOfMapForeach (TACLET)

• getOfMapOverride (TACLET)

• getOfMapRemove (TACLET)

• getOfMapUpdate (TACLET)

• getOfSeq2Map (TACLET)

• inDomainOfMapRemove (TACLET)

• inDomainOfMapUpdate (TACLET)

• mapEqualityRight (TACLET)

• mapRemoveUnchanged (TACLET)

• mapRemoveUnchanged2 (TACLET)

• mapUpdateUnchanged (TACLET)

• mapUpdateUnchanged2 (TACLET)

• nonNull (TACLET)

• subsortTrans (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)

• compound_assignment_1_new (TACLET)

• compound_assignment_2 (TACLET)

• compound_assignment_3_mixed (TACLET)

• compound_assignment_3_nonsimple (TACLET)

• compound_assignment_3_simple (TACLET)

• compound_assignment_4_nonsimple (TACLET)

• compound_assignment_4_simple (TACLET)

• compound_assignment_5_mixed (TACLET)

• compound_assignment_5_nonsimple (TACLET)

• compound_assignment_5_simple (TACLET)

• compound_assignment_6_nonsimple (TACLET)

• compound_assignment_6_simple (TACLET)

• compound_assignment_xor_nonsimple (TACLET)

• compound_assignment_xor_simple (TACLET)

• postdecrement (TACLET)

• postdecrement_array (TACLET)

• postdecrement_assignment (TACLET)

• postdecrement_assignment_array (TACLET)

• postdecrement_assignment_attribute (TACLET)

• postdecrement_attribute (TACLET)

• postincrement (TACLET)

• postincrement_array (TACLET)

• postincrement_assignment (TACLET)

• postincrement_assignment_array (TACLET)

• postincrement_assignment_attribute (TACLET)

• postincrement_attribute (TACLET)

• predecrement (TACLET)

• predecrement_array (TACLET)

• predecrement_assignment (TACLET)

• predecrement_assignment_array (TACLET)

• predecrement_assignment_attribute (TACLET)

• predecrement_attribute (TACLET)

• preincrement (TACLET)

• preincrement_array (TACLET)

• preincrement_assignment (TACLET)

• preincrement_assignment_array (TACLET)

• preincrement_assignment_attribute (TACLET)

• preincrement_attribute (TACLET)

simplify_heap_high_costs

• selectCreatedOfAnon (TACLET)

• selectCreatedOfAnonEQ (TACLET)

• selectOfAnonEQ (TACLET)

• selectOfCreateEQ (TACLET)

• selectOfMemsetEQ (TACLET)

• selectOfStoreEQ (TACLET)

simplify_java

• array_self_reference (TACLET)

• array_self_reference_eq (TACLET)

• array_store_known_dynamic_array_type (TACLET)

• class_being_initialized_is_prepared (TACLET)

• class_erroneous_excludes_class_in_init (TACLET)

• class_initialized_excludes_class_init_in_progress (TACLET)

• erroneous_class_has_no_initialized_sub_class (TACLET)

• ifElseSkipElse (TACLET)

• ifElseSkipElseConditionInBlock (TACLET)

• ifElseSkipThen (TACLET)

• ifElseSkipThenConditionInBlock (TACLET)

• ifEnterThen (TACLET)

• ifEnterThenConditionInBlock (TACLET)

• ifSkipThen (TACLET)

• ifSkipThenConditionInBlock (TACLET)

• initialized_class_is_not_erroneous (TACLET)

• initialized_class_is_prepared (TACLET)

• null_can_always_be_stored_in_a_reference_type_array (TACLET)

• superclasses_of_initialized_classes_are_initialized (TACLET)

• superclasses_of_initialized_classes_are_prepared (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)

• array_post_declaration (TACLET)

• assert (TACLET)

• assertSafe (TACLET)

• assertSafeWithMessage (TACLET)

• assertWithPrimitiveMessage (TACLET)

• assertWithReferenceMessage (TACLET)

• assertWithReferenceMessageNull (TACLET)

• assignment (TACLET)

• assignment_array2 (TACLET)

• assignment_read_attribute (TACLET)

• assignment_read_attribute_final (TACLET)

• assignment_read_attribute_this (TACLET)

• assignment_read_attribute_this_final (TACLET)

• assignment_read_length (TACLET)

• assignment_read_length_this (TACLET)

• assignment_read_static_attribute (TACLET)

• assignment_read_static_attribute_final (TACLET)

• assignment_read_static_attribute_with_variable_prefix (TACLET)

• assignment_to_primitive_array_component (TACLET)

• assignment_to_primitive_array_component_transaction (TACLET)

• assignment_to_reference_array_component (TACLET)

• assignment_to_reference_array_component_transaction (TACLET)

• assignment_write_array_this_access_normalassign (TACLET)

• assignment_write_attribute (TACLET)

• assignment_write_attribute_this (TACLET)

• assignment_write_static_attribute (TACLET)

• assignment_write_static_attribute_with_variable_prefix (TACLET)

• beginJavaCardTransactionAPI (TACLET)

• beginJavaCardTransactionBox (TACLET)

• beginJavaCardTransactionDiamond (TACLET)

• blockBreak (TACLET)

• blockBreakLabel (TACLET)

• blockBreakLabeled (TACLET)

• blockBreakNoLabel (TACLET)

• blockContinue (TACLET)

• blockContinueLabeled (TACLET)

• blockEmpty (TACLET)

• blockEmptyLabel (TACLET)

• blockReturn (TACLET)

• blockReturnLabel1 (TACLET)

• blockReturnLabel2 (TACLET)

• blockReturnNoValue (TACLET)

• blockThrow (TACLET)

• break (TACLET)

• castToBoolean (TACLET)

• commitJavaCardTransactionAPI (TACLET)

• commitJavaCardTransactionBox (TACLET)

• commitJavaCardTransactionDiamond (TACLET)

• compound_addition_1 (TACLET)

• compound_addition_2 (TACLET)

• compound_assignment_op_and (TACLET)

• compound_assignment_op_and_array (TACLET)

• compound_assignment_op_and_attr (TACLET)

• compound_assignment_op_div (TACLET)

• compound_assignment_op_div_array (TACLET)

• compound_assignment_op_div_attr (TACLET)

• compound_assignment_op_minus (TACLET)

• compound_assignment_op_minus_array (TACLET)

• compound_assignment_op_minus_attr (TACLET)

• compound_assignment_op_mod (TACLET)

• compound_assignment_op_mod_array (TACLET)

• compound_assignment_op_mod_attr (TACLET)

• compound_assignment_op_mul (TACLET)

• compound_assignment_op_mul_array (TACLET)

• compound_assignment_op_mul_attr (TACLET)

• compound_assignment_op_or (TACLET)

• compound_assignment_op_or_array (TACLET)

• compound_assignment_op_or_attr (TACLET)

• compound_assignment_op_plus (TACLET)

• compound_assignment_op_plus_array (TACLET)

• compound_assignment_op_plus_attr (TACLET)

• compound_assignment_op_shiftleft (TACLET)

• compound_assignment_op_shiftleft_array (TACLET)

• compound_assignment_op_shiftleft_attr (TACLET)

• compound_assignment_op_shiftright (TACLET)

• compound_assignment_op_shiftright_array (TACLET)

• compound_assignment_op_shiftright_attr (TACLET)

• compound_assignment_op_unsigned_shiftright (TACLET)

• compound_assignment_op_unsigned_shiftright_array (TACLET)

• compound_assignment_op_unsigned_shiftright_attr (TACLET)

• compound_assignment_op_xor (TACLET)

• compound_assignment_op_xor_array (TACLET)

• compound_assignment_op_xor_attr (TACLET)

• compound_binary_AND_1 (TACLET)

• compound_binary_AND_2 (TACLET)

• compound_binary_OR_1 (TACLET)

• compound_binary_OR_2 (TACLET)

• compound_binary_XOR_1 (TACLET)

• compound_binary_XOR_2 (TACLET)

• compound_byte_cast_expression (TACLET)

• compound_division_1 (TACLET)

• compound_division_2 (TACLET)

• compound_equality_comparison_1 (TACLET)

• compound_equality_comparison_2 (TACLET)

• compound_greater_equal_than_comparison_1 (TACLET)

• compound_greater_equal_than_comparison_2 (TACLET)

• compound_greater_than_comparison_1 (TACLET)

• compound_greater_than_comparison_2 (TACLET)

• compound_inequality_comparison_1 (TACLET)

• compound_inequality_comparison_2 (TACLET)

• compound_int_cast_expression (TACLET)

• compound_invert_bits (TACLET)

• compound_less_equal_than_comparison_1 (TACLET)

• compound_less_equal_than_comparison_2 (TACLET)

• compound_less_than_comparison_1 (TACLET)

• compound_less_than_comparison_2 (TACLET)

• compound_long_cast_expression (TACLET)

• compound_modulo_1 (TACLET)

• compound_modulo_2 (TACLET)

• compound_multiplication_1 (TACLET)

• compound_multiplication_2 (TACLET)

• compound_reference_cast_expression (TACLET)

• compound_reference_cast_expression_primitive (TACLET)

• compound_shiftleft_1 (TACLET)

• compound_shiftleft_2 (TACLET)

• compound_shiftright_1 (TACLET)

• compound_shiftright_2 (TACLET)

• compound_short_cast_expression (TACLET)

• compound_subtraction_1 (TACLET)

• compound_subtraction_2 (TACLET)

• compound_unsigned_shiftright_1 (TACLET)

• compound_unsigned_shiftright_2 (TACLET)

• condition (TACLET)

• condition_not_simple (TACLET)

• condition_simple (TACLET)

• deleteMergePoint (TACLET)

• delete_unnecessary_cast (TACLET)

• doWhileUnwind (TACLET)

• elim_double_block (TACLET)

• elim_double_block_2 (TACLET)

• elim_double_block_3 (TACLET)

• elim_double_block_4 (TACLET)

• elim_double_block_5 (TACLET)

• elim_double_block_6 (TACLET)

• elim_double_block_7 (TACLET)

• elim_double_block_8 (TACLET)

• elim_double_block_9 (TACLET)

• emptyModality (TACLET)

• emptyModalityBoxTransaction (TACLET)

• emptyModalityDiamondTransaction (TACLET)

• emptyStatement (TACLET)

• enhancedfor_iterable (TACLET)

• equality_comparison_new (TACLET)

• equality_comparison_simple (TACLET)

• eval_array_this_access (TACLET)

• eval_order_access1 (TACLET)

• eval_order_access2 (TACLET)

• eval_order_access4 (TACLET)

• eval_order_access4_this (TACLET)

• eval_order_array_access1 (TACLET)

• eval_order_array_access2 (TACLET)

• eval_order_array_access3 (TACLET)

• eval_order_array_access4 (TACLET)

• eval_order_array_access5 (TACLET)

• eval_order_array_access6 (TACLET)

• eval_order_iterated_assignments_0_0 (TACLET)

• eval_order_iterated_assignments_0_1 (TACLET)

• eval_order_iterated_assignments_10_0 (TACLET)

• eval_order_iterated_assignments_10_1 (TACLET)

• eval_order_iterated_assignments_11_0 (TACLET)

• eval_order_iterated_assignments_11_1 (TACLET)

• eval_order_iterated_assignments_1_0 (TACLET)

• eval_order_iterated_assignments_1_1 (TACLET)

• eval_order_iterated_assignments_2_0 (TACLET)

• eval_order_iterated_assignments_2_1 (TACLET)

• eval_order_iterated_assignments_3_0 (TACLET)

• eval_order_iterated_assignments_3_1 (TACLET)

• eval_order_iterated_assignments_4_0 (TACLET)

• eval_order_iterated_assignments_4_1 (TACLET)

• eval_order_iterated_assignments_5_0 (TACLET)

• eval_order_iterated_assignments_5_1 (TACLET)

• eval_order_iterated_assignments_6_0 (TACLET)

• eval_order_iterated_assignments_6_1 (TACLET)

• eval_order_iterated_assignments_7_0 (TACLET)

• eval_order_iterated_assignments_7_1 (TACLET)

• eval_order_iterated_assignments_8_0 (TACLET)

• eval_order_iterated_assignments_8_1 (TACLET)

• eval_order_iterated_assignments_9_0 (TACLET)

• eval_order_iterated_assignments_9_1 (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)

• greater_equal_than_comparison_new (TACLET)

• greater_equal_than_comparison_simple (TACLET)

• greater_than_comparison_new (TACLET)

• greater_than_comparison_simple (TACLET)

• ifElseFalse (TACLET)

• ifElseTrue (TACLET)

• ifFalse (TACLET)

• ifTrue (TACLET)

• inequality_comparison_new (TACLET)

• inequality_comparison_simple (TACLET)

• iterated_assignments_0 (TACLET)

• iterated_assignments_1 (TACLET)

• iterated_assignments_10 (TACLET)

• iterated_assignments_11 (TACLET)

• iterated_assignments_2 (TACLET)

• iterated_assignments_3 (TACLET)

• iterated_assignments_4 (TACLET)

• iterated_assignments_5 (TACLET)

• iterated_assignments_6 (TACLET)

• iterated_assignments_7 (TACLET)

• iterated_assignments_8 (TACLET)

• iterated_assignments_9 (TACLET)

• less_equal_than_comparison_new (TACLET)

• less_equal_than_comparison_simple (TACLET)

• less_than_comparison_new (TACLET)

• less_than_comparison_simple (TACLET)

• lsBreak (TACLET)

• lsContinue (TACLET)

• lsLblBreak (TACLET)

• lsLblContinueMatch (TACLET)

• lsLblContinueNoMatch1 (TACLET)

• lsLblContinueNoMatch2 (TACLET)

• lsReturnNonVoid (TACLET)

• lsReturnVoid (TACLET)

• lsThrow (TACLET)

• methodBodyExpand (TACLET)

• methodCallEmpty (TACLET)

• methodCallEmptyNoreturnBox (TACLET)

• methodCallEmptyReturn (TACLET)

• methodCallParamThrow (TACLET)

• methodCallReturn (TACLET)

• methodCallReturnIgnoreResult (TACLET)

• methodCallThrow (TACLET)

• reference_type_cast (TACLET)

• remove_parentheses_attribute_left (TACLET)

• remove_parentheses_lhs_left (TACLET)

• remove_parentheses_right (TACLET)

• returnUnfold (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)

• switch (TACLET)

• synchronizedBlockEmpty (TACLET)

• synchronizedBlockEmpty2 (TACLET)

• synchronizedBlockEvalSync (TACLET)

• throwBox (TACLET)

• throwDiamond (TACLET)

• throwLabel (TACLET)

• throwLabelBlock (TACLET)

• throwUnfold (TACLET)

• throwUnfoldMore (TACLET)

• tryBreak (TACLET)

• tryBreakLabel (TACLET)

• tryCatchFinallyThrow (TACLET)

• tryCatchThrow (TACLET)

• tryEmpty (TACLET)

• tryFinallyBreak (TACLET)

• tryFinallyBreakLabel (TACLET)

• tryFinallyEmpty (TACLET)

• tryFinallyReturn (TACLET)

• tryFinallyReturnNoValue (TACLET)

• tryFinallyThrow (TACLET)

• tryMultipleCatchThrow (TACLET)

• tryReturn (TACLET)

• tryReturnNoValue (TACLET)

• try_continue_1 (TACLET)

• try_continue_2 (TACLET)

• try_finally_continue_1 (TACLET)

• try_finally_continue_2 (TACLET)

• unusedLabel (TACLET)

• variableDeclaration (TACLET)

• variableDeclarationAssign (TACLET)

• variableDeclarationFinal (TACLET)

• variableDeclarationFinalAssign (TACLET)

• variableDeclarationGhost (TACLET)

• variableDeclarationGhostAssign (TACLET)

• variableDeclarationMult (TACLET)

simplify_prog_subset

• activeUseStaticFieldReadAccess (TACLET)

• activeUseStaticFieldReadAccess2 (TACLET)

• activeUseStaticFieldWriteAccess (TACLET)

• activeUseStaticFieldWriteAccess2 (TACLET)

• activeUseStaticFieldWriteAccess3 (TACLET)

• activeUseStaticFieldWriteAccess4 (TACLET)

• activeUseStaticFieldWriteAccess5 (TACLET)

• activeUseStaticFieldWriteAccess6 (TACLET)

• array_post_declaration (TACLET)

• assignment (TACLET)

• assignment_array2 (TACLET)

• assignment_read_attribute (TACLET)

• assignment_read_attribute_final (TACLET)

• assignment_read_attribute_this (TACLET)

• assignment_read_attribute_this_final (TACLET)

• assignment_read_length (TACLET)

• assignment_read_length_this (TACLET)

• assignment_read_static_attribute (TACLET)

• assignment_read_static_attribute_final (TACLET)

• assignment_to_primitive_array_component (TACLET)

• assignment_to_primitive_array_component_transaction (TACLET)

• assignment_to_reference_array_component (TACLET)

• assignment_to_reference_array_component_transaction (TACLET)

• assignment_write_array_this_access_normalassign (TACLET)

• assignment_write_attribute (TACLET)

• assignment_write_attribute_this (TACLET)

• assignment_write_static_attribute (TACLET)

• assignment_write_static_attribute_with_variable_prefix (TACLET)

• blockBreakNoLabel (TACLET)

• blockEmpty (TACLET)

• blockEmptyLabel (TACLET)

• blockReturn (TACLET)

• blockReturnLabel1 (TACLET)

• blockReturnLabel2 (TACLET)

• blockReturnNoValue (TACLET)

• blockThrow (TACLET)

• emptyStatement (TACLET)

• eval_array_this_access (TACLET)

• eval_order_access1 (TACLET)

• eval_order_access2 (TACLET)

• eval_order_access4 (TACLET)

• eval_order_access4_this (TACLET)

• eval_order_array_access1 (TACLET)

• eval_order_array_access2 (TACLET)

• eval_order_array_access3 (TACLET)

• eval_order_array_access4 (TACLET)

• eval_order_array_access5 (TACLET)

• eval_order_array_access6 (TACLET)

• stringAssignment (TACLET)

• stringConcat (TACLET)

• stringConcatBooleanLeft (TACLET)

• stringConcatBooleanRight (TACLET)

• stringConcatCharExpLeft (TACLET)

• stringConcatCharExpRight (TACLET)

• stringConcatIntExpLeft (TACLET)

• stringConcatIntExpRight (TACLET)

• stringConcatObjectLeft (TACLET)

• stringConcatObjectRight (TACLET)

• synchronizedBlockEmpty (TACLET)

• synchronizedBlockEmpty2 (TACLET)

• synchronizedBlockEvalSync (TACLET)

• variableDeclaration (TACLET)

• variableDeclarationAssign (TACLET)

• variableDeclarationFinal (TACLET)

• variableDeclarationFinalAssign (TACLET)

• variableDeclarationGhost (TACLET)

• variableDeclarationGhostAssign (TACLET)

• variableDeclarationMult (TACLET)

simplify_select

• simplifySelectOfAnon (TACLET)

• simplifySelectOfAnonEQ (TACLET)

• simplifySelectOfCreate (TACLET)

• simplifySelectOfCreateEQ (TACLET)

• simplifySelectOfMemset (TACLET)

• simplifySelectOfMemsetEQ (TACLET)

• simplifySelectOfStore (TACLET)

• simplifySelectOfStoreEQ (TACLET)

split_cond

• ifExthenelse1_split (TACLET)

• ifExthenelse1_split_for (TACLET)

• ifthenelse_split (TACLET)

• ifthenelse_split_for (TACLET)

split_if

• compound_assignment_3_nonsimple (TACLET)

• compound_assignment_5_nonsimple (TACLET)

• condition (TACLET)

• equality_comparison_new (TACLET)

• greater_equal_than_comparison_new (TACLET)

• greater_than_comparison_new (TACLET)

• ifElseSplit (TACLET)

• ifElseSplitLeft (TACLET)

• ifSplit (TACLET)

• ifSplitLeft (TACLET)

• inequality_comparison_new (TACLET)

• less_equal_than_comparison_new (TACLET)

• less_than_comparison_new (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)