JavaCard Strings assertions bigint finalFields floatRules initialisation intRules integerSimplificationRules javaLoopTreatment mergeGenerateIsWeakeningGoal methodExpansion modelFields moreSeqRules permissions programRules reach runtimeExceptions sequences soundDefaultContracts wdChecks wdOperator

JavaCard:off JavaCard:on Strings:off Strings:on assertions:off assertions:on assertions:safe bigint:off bigint:on finalFields:immutable finalFields:onHeap floatRules:assumeStrictfp floatRules:strictfpOnly initialisation:disableStaticInitialisation initialisation:enableStaticInitialisation intRules:arithmeticSemanticsCheckingOF intRules:arithmeticSemanticsIgnoringOF intRules:javaSemantics integerSimplificationRules:full integerSimplificationRules:minimal javaLoopTreatment:efficient javaLoopTreatment:teaching mergeGenerateIsWeakeningGoal:off mergeGenerateIsWeakeningGoal:on methodExpansion:modularOnly methodExpansion:noRestriction modelFields:showSatisfiability modelFields:treatAsAxiom moreSeqRules:off moreSeqRules:on permissions:off permissions:on programRules:Java programRules:None reach:off reach:on runtimeExceptions:allow runtimeExceptions:ban runtimeExceptions:ignore sequences:off sequences:on soundDefaultContracts:off soundDefaultContracts:on wdChecks:off wdChecks:on wdOperator:D wdOperator:L wdOperator:Y

C CSub E Field Free G G G G G G2 GOS GSub H H H Heap J J K Map Pair S1 S2 SORT alph alphSub alpha alphaObj alphaObj alphaObj any bet beta betaObj betaObj boolean deltaObject gamma java.io.Serializable java.lang.Cloneable java.lang.Object java.lang.String

acc arrayStoreValid assignable inDomain inDomainImpliesCreated isFinite measuredBy measuredByCheck measuredByEmpty newObjectsIsomorphic newOnHeap nonNull objectIsomorphic objectsIsomorphic prec reach sameType sameTypes ssubsort wellFormed wellOrderLeqInt

$classErroneous $classInitializationInProgress $classInitialized $classPrepared FALSE TRUE anon anySORT arr atom cast create defaultValue exactInstance final first instance java.lang.Object::#$created java.lang.Object::#$initialized java.lang.Object::#$transactionConditionallyUpdated java.lang.Object::#$transient length mapEmpty mapForeach mapGet mapOverride mapRemove mapSingleton mapSize mapUndef mapUpdate memset null pair second select seq2map ssort store strContent strPool

F T WD wd

alpha apply_auxiliary_eq apply_equations apply_equations_andOr apply_select_eq auto_induction auto_induction_lemma beta boolean_cases boxDiamondConv cast_deletion charLiteral_to_intLiteral classAxiom closure cnf_andAssoc cnf_andComm cnf_dist cnf_expandIfThenElse cnf_orAssoc cnf_orComm cnf_setComm comprehension_split comprehensions comprehensions_high_costs comprehensions_low_costs concrete concrete_java confluence_restricted conjNormalForm cut cut_direct defOpsConcat defOpsReplace defOpsReplaceInline defOpsSeqEquality defOpsStartsEndsWith defOps_div defOps_divModPullOut defOps_expandJNumericOp defOps_expandModulo defOps_expandRanges defOps_jdiv defOps_jdiv_inline defOps_mod defOps_modHomoEq delayedExpansion delta delta distrQuantifier elimQuantifier elimQuantifierWithCast eval_literals evaluate_instanceof executeDoubleAssignment executeFloatAssignment executeIntegerAssignment find_term_not_in_assumes gamma gamma_destructive hide_auxiliary_eq hide_auxiliary_eq_const inEqSimp_andOr_subsumption inEqSimp_and_contradInEqs inEqSimp_and_subsumptionEq inEqSimp_antiSymm inEqSimp_balance inEqSimp_commute inEqSimp_contradEqs inEqSimp_contradInEqs inEqSimp_directInEquations inEqSimp_exactShadow inEqSimp_expand inEqSimp_forNormalisation inEqSimp_homo inEqSimp_makeNonStrict inEqSimp_moveLeft inEqSimp_nonLin inEqSimp_nonLin_divide inEqSimp_nonLin_multiply inEqSimp_nonLin_neg inEqSimp_nonLin_pos inEqSimp_nonNegSquares inEqSimp_normalise inEqSimp_or_antiSymm inEqSimp_or_tautInEqs inEqSimp_or_weaken inEqSimp_propagation inEqSimp_pullOutGcd inEqSimp_pullOutGcd_antec inEqSimp_pullOutGcd_geq inEqSimp_pullOutGcd_leq inEqSimp_saturate inEqSimp_signCases inEqSimp_special_nonLin inEqSimp_split_eq inEqSimp_strengthen inEqSimp_subsumption inReachableStateImplication induction_var information_flow_contract_appl insert_eq_nonrigid instanceof_to_exists int_arithmetic integerToString javaFloatSemantics javaIntegerSemantics limitObserver loopInvariant loop_expand loop_scope_expand loop_scope_inv_taclet merge_point method_expand modal_tautology moveQuantToLeft negationNormalForm no_self_application nonDuplicateAppCheckEq notHumanReadable obsolete order_terms partialInvAxiom polyDivision polySimp_addAssoc polySimp_addOrder polySimp_applyEq polySimp_applyEqPseudo polySimp_applyEqRigid polySimp_balance polySimp_critPair polySimp_directEquations polySimp_dist polySimp_elimOneLeft polySimp_elimOneRight polySimp_elimSubNeg polySimp_expand polySimp_homo polySimp_leftNonUnit polySimp_mulAssoc polySimp_mulOne polySimp_mulOrder polySimp_newSmallSym polySimp_newSym polySimp_normalise polySimp_pullOutFactor polySimp_pullOutGcd polySimp_saturate pullOutQuantifierAll pullOutQuantifierEx pullOutQuantifierUnifying pull_out_quantifier pull_out_select query_axiom replace_known_left replace_known_right semantics_blasting setEqualityBlastingRight simplify simplify_ENLARGING simplify_autoname simplify_boolean simplify_enlarging simplify_expression simplify_heap_high_costs simplify_instanceof_static simplify_int simplify_java simplify_literals simplify_prog simplify_prog_subset simplify_select split_cond split_if std_taclets stringNormalisationReduce stringsConcatNotBothLiterals stringsContainsDefInline stringsExpandDefNormalOp stringsIntroduceNewSym stringsMoveReplaceInside stringsReduceConcat stringsReduceOrMoveOutsideConcat stringsReduceSubstring stringsSimplify swapQuantifiers system_invariant test_gen test_gen_empty_modality_hide test_gen_quan test_gen_quan_num triggered try_apply_subst type_hierarchy_def update_apply update_apply_on_update update_elim update_join userTaclets1 userTaclets2 userTaclets3

abortJavaCardTransactionAPI abortJavaCardTransactionBox abortJavaCardTransactionDiamond accDefinition activeUseAddition activeUseAddition activeUseBitwiseAnd activeUseBitwiseAnd activeUseBitwiseNegation activeUseBitwiseNegation activeUseBitwiseOr activeUseBitwiseOr activeUseBitwiseXOr activeUseBitwiseXOr activeUseByteCast activeUseByteCast activeUseCharCast activeUseCharCast activeUseDivision activeUseDivision activeUseIntCast activeUseIntCast activeUseMinus activeUseModulo activeUseModulo activeUseMultiplication activeUseMultiplication activeUseShiftLeft activeUseShiftLeft activeUseShiftRight activeUseShiftRight activeUseShortCast activeUseShortCast activeUseStaticFieldReadAccess activeUseStaticFieldReadAccess activeUseStaticFieldReadAccess2 activeUseStaticFieldReadAccess2 activeUseStaticFieldWriteAccess activeUseStaticFieldWriteAccess activeUseStaticFieldWriteAccess2 activeUseStaticFieldWriteAccess2 activeUseStaticFieldWriteAccess3 activeUseStaticFieldWriteAccess3 activeUseStaticFieldWriteAccess4 activeUseStaticFieldWriteAccess4 activeUseStaticFieldWriteAccess5 activeUseStaticFieldWriteAccess5 activeUseStaticFieldWriteAccess6 activeUseStaticFieldWriteAccess6 activeUseSubtraction activeUseSubtraction activeUseUnaryMinus activeUseUnsignedShiftRight activeUseUnsignedShiftRight allFieldsUnfold allObjectsAssignment all_bool allocateInstance allocateInstance allocateInstanceWithLength allocateInstanceWithLength applyOnElementary applyOnPV applyOnParallel applyOnRigidFormula applyOnRigidTerm applyOnSkip applySkip1 applySkip2 applySkip3 apply_eq_boolean apply_eq_boolean_2 apply_eq_boolean_rigid apply_eq_boolean_rigid_2 arrayCreation arrayCreationWithInitializers arrayInitialisation arrayLengthIsAShort arrayLengthIsAnInt arrayLengthNotNegative array_post_declaration array_self_reference array_self_reference_eq array_store_known_dynamic_array_type assert assertSafe assertSafeWithMessage assertWithPrimitiveMessage assertWithReferenceMessage assertWithReferenceMessageNull assignableDefinition assignment assignment_array2 assignment_array2 assignment_array2 assignment_read_attribute assignment_read_attribute assignment_read_attribute assignment_read_attribute assignment_read_attribute assignment_read_attribute_final assignment_read_attribute_final assignment_read_attribute_this assignment_read_attribute_this assignment_read_attribute_this assignment_read_attribute_this assignment_read_attribute_this assignment_read_attribute_this_final assignment_read_attribute_this_final assignment_read_length assignment_read_length assignment_read_length assignment_read_length_this assignment_read_static_attribute assignment_read_static_attribute assignment_read_static_attribute_final assignment_read_static_attribute_with_variable_prefix assignment_to_primitive_array_component assignment_to_primitive_array_component assignment_to_primitive_array_component assignment_to_primitive_array_component_transaction assignment_to_primitive_array_component_transaction assignment_to_primitive_array_component_transaction assignment_to_reference_array_component assignment_to_reference_array_component assignment_to_reference_array_component assignment_to_reference_array_component_transaction assignment_to_reference_array_component_transaction assignment_to_reference_array_component_transaction assignment_write_array_this_access_normalassign assignment_write_array_this_access_normalassign assignment_write_attribute assignment_write_attribute assignment_write_attribute assignment_write_attribute_this assignment_write_attribute_this assignment_write_static_attribute assignment_write_static_attribute_with_variable_prefix beginJavaCardTransactionAPI beginJavaCardTransactionBox beginJavaCardTransactionDiamond blockBreak blockBreakLabel blockBreakLabeled blockBreakNoLabel blockContinue blockContinueLabeled blockEmpty blockEmptyLabel blockReturn blockReturnLabel1 blockReturnLabel2 blockReturnNoValue blockThrow boolean_equal boolean_equal_2 boolean_false_commute boolean_not_equal_1 boolean_not_equal_2 boolean_true_commute boxToDiamond boxToDiamondTransaction box_and_left box_and_right box_or_left box_or_right box_true break castAdd castAdd2 castDel castDel2 castToBoolean castTrueImpliesOriginalTrue castType castType2 class_being_initialized_is_prepared class_erroneous_excludes_class_in_init class_initialized_excludes_class_init_in_progress closeType closeTypeSwitched commitJavaCardTransactionAPI commitJavaCardTransactionBox commitJavaCardTransactionDiamond compound_addition_1 compound_addition_2 compound_assignment_1_new compound_assignment_2 compound_assignment_3_mixed compound_assignment_3_nonsimple compound_assignment_3_simple compound_assignment_4_nonsimple compound_assignment_4_simple compound_assignment_5_mixed compound_assignment_5_nonsimple compound_assignment_5_simple compound_assignment_6_nonsimple compound_assignment_6_simple compound_assignment_op_and compound_assignment_op_and_array compound_assignment_op_and_attr compound_assignment_op_div compound_assignment_op_div_array compound_assignment_op_div_attr compound_assignment_op_minus compound_assignment_op_minus_array compound_assignment_op_minus_attr compound_assignment_op_mod compound_assignment_op_mod_array compound_assignment_op_mod_attr compound_assignment_op_mul compound_assignment_op_mul_array compound_assignment_op_mul_attr compound_assignment_op_or compound_assignment_op_or_array compound_assignment_op_or_attr compound_assignment_op_plus compound_assignment_op_plus_array compound_assignment_op_plus_attr compound_assignment_op_shiftleft compound_assignment_op_shiftleft_array compound_assignment_op_shiftleft_attr compound_assignment_op_shiftright compound_assignment_op_shiftright_array compound_assignment_op_shiftright_attr compound_assignment_op_unsigned_shiftright compound_assignment_op_unsigned_shiftright_array compound_assignment_op_unsigned_shiftright_attr compound_assignment_op_xor compound_assignment_op_xor_array compound_assignment_op_xor_attr compound_assignment_xor_nonsimple compound_assignment_xor_simple compound_binary_AND_1 compound_binary_AND_2 compound_binary_OR_1 compound_binary_OR_2 compound_binary_XOR_1 compound_binary_XOR_2 compound_byte_cast_expression compound_division_1 compound_division_2 compound_equality_comparison_1 compound_equality_comparison_2 compound_greater_equal_than_comparison_1 compound_greater_equal_than_comparison_2 compound_greater_than_comparison_1 compound_greater_than_comparison_2 compound_inequality_comparison_1 compound_inequality_comparison_2 compound_int_cast_expression compound_invert_bits compound_less_equal_than_comparison_1 compound_less_equal_than_comparison_2 compound_less_than_comparison_1 compound_less_than_comparison_2 compound_long_cast_expression compound_modulo_1 compound_modulo_2 compound_multiplication_1 compound_multiplication_2 compound_reference_cast_expression compound_reference_cast_expression_primitive compound_shiftleft_1 compound_shiftleft_2 compound_shiftright_1 compound_shiftright_2 compound_short_cast_expression compound_subtraction_1 compound_subtraction_2 compound_unsigned_shiftright_1 compound_unsigned_shiftright_2 condition condition_not_simple condition_simple crossInst cutUpperBound defInDomainImpliesCreated defIsFinite defMapEmpty defMapEquality defMapOverride defMapRemove defMapSingleton defMapUpdate defSeq2Map def_wellOrderLeqInt definitionOfNewObjectsIsomorphic definitionOfNewOnHeap definitionOfObjectIsomorphic definitionOfObjectsIsomorphic definitionOfSameTypes deleteMergePoint delete_unnecessary_cast diamondToBox diamondToBoxTransaction diamond_and_left diamond_and_right diamond_false diamond_or_left diamond_or_right diamond_split_termination dismissNonSelectedField dismissNonSelectedFieldEQ doWhileUnwind dropEffectlessStores dynamic_type_for_null elim_double_block elim_double_block_2 elim_double_block_3 elim_double_block_4 elim_double_block_5 elim_double_block_6 elim_double_block_7 elim_double_block_8 elim_double_block_9 emptyModality emptyModalityBoxTransaction emptyModalityDiamondTransaction emptyStatement enhancedfor_iterable equalityToSelect equality_comparison_new equality_comparison_simple erroneous_class_has_no_initialized_sub_class eval_array_this_access eval_order_access1 eval_order_access2 eval_order_access4 eval_order_access4_this eval_order_array_access1 eval_order_array_access2 eval_order_array_access3 eval_order_array_access3 eval_order_array_access4 eval_order_array_access5 eval_order_array_access6 eval_order_iterated_assignments_0_0 eval_order_iterated_assignments_0_1 eval_order_iterated_assignments_10_0 eval_order_iterated_assignments_10_1 eval_order_iterated_assignments_11_0 eval_order_iterated_assignments_11_1 eval_order_iterated_assignments_1_0 eval_order_iterated_assignments_1_1 eval_order_iterated_assignments_2_0 eval_order_iterated_assignments_2_1 eval_order_iterated_assignments_3_0 eval_order_iterated_assignments_3_1 eval_order_iterated_assignments_4_0 eval_order_iterated_assignments_4_1 eval_order_iterated_assignments_5_0 eval_order_iterated_assignments_5_1 eval_order_iterated_assignments_6_0 eval_order_iterated_assignments_6_1 eval_order_iterated_assignments_7_0 eval_order_iterated_assignments_7_1 eval_order_iterated_assignments_8_0 eval_order_iterated_assignments_8_1 eval_order_iterated_assignments_9_0 eval_order_iterated_assignments_9_1 evaluateAssertCondition_1 evaluateAssertCondition_2 evaluateAssertMessage ex_bool exact_instance_definition_boolean exact_instance_definition_int exact_instance_definition_null exact_instance_for_interfaces_or_abstract_classes exact_instance_known_dynamic_type execBreak execBreakEliminateBreakLabel execBreakEliminateBreakLabelWildcard execBreakEliminateContinue execBreakEliminateContinueLabel execBreakEliminateContinueLabelWildcard execBreakEliminateExcCcatch execBreakEliminateReturn execBreakEliminateReturnVal execBreakLabelEliminateBreak execBreakLabelEliminateBreakLabelNoMatch execBreakLabelEliminateContinue execBreakLabelEliminateContinueLabel execBreakLabelEliminateContinueLabelWildcard execBreakLabelEliminateExcCcatch execBreakLabelEliminateReturn execBreakLabelEliminateReturnVal execBreakLabelMatch execBreakLabelWildcard execCatchThrow execContinue execContinueEliminateBreak execContinueEliminateBreakLabel execContinueEliminateBreakLabelWildcard execContinueEliminateExcCcatch execContinueEliminateReturn execContinueEliminateReturnVal execContinueLabelEliminateBreak execContinueLabelEliminateBreakLabel execContinueLabelEliminateBreakLabelWildcard execContinueLabelEliminateContinue execContinueLabelEliminateContinueLabelNoMatch execContinueLabelEliminateExcCcatch execContinueLabelEliminateReturn execContinueLabelEliminateReturnVal execContinueLabelMatch execContinueLabelWildcard execEmpty execMultipleCatchThrow execNoCcatch execReturn execReturnEliminateBreak execReturnEliminateBreakLabel execReturnEliminateBreakLabelWildcard execReturnEliminateContinue execReturnEliminateContinueLabel execReturnEliminateContinueLabelWildcard execReturnEliminateExcCcatch execReturnEliminateReturnVal execReturnVal execReturnValEliminateBreak execReturnValEliminateBreakLabel execReturnValEliminateBreakLabelWildcard execReturnValEliminateContinue execReturnValEliminateContinueLabel execReturnValEliminateContinueLabelWildcard execReturnValEliminateExcCcatch execReturnValEliminateReturn execReturnValNonMatchingType execThrowEliminateBreak execThrowEliminateBreakLabel execThrowEliminateBreakLabelWildcard execThrowEliminateContinue execThrowEliminateContinueLabel execThrowEliminateContinueLabelWildcard execThrowEliminateReturn execThrowEliminateReturnVal false_to_not_true finishJavaCardTransactionBox finishJavaCardTransactionDiamond firstOfPair forInitUnfold for_to_while getJavaCardTransient getOfMapEmpty getOfMapForeach getOfMapOverride getOfMapRemove getOfMapSingleton getOfMapUpdate getOfSeq2Map greater_equal_than_comparison_new greater_equal_than_comparison_simple greater_than_comparison_new greater_than_comparison_simple hideAuxiliaryEq hideAuxiliaryEqConcrete hideAuxiliaryEqConcrete2 if ifElse ifElseFalse ifElseSkipElse ifElseSkipElseConditionInBlock ifElseSkipThen ifElseSkipThenConditionInBlock ifElseSplit ifElseSplitLeft ifElseTrue ifElseUnfold ifEnterThen ifEnterThenConditionInBlock ifExthenelse1_eq ifExthenelse1_eq2 ifExthenelse1_eq2_for ifExthenelse1_eq2_for_phi ifExthenelse1_eq2_phi ifExthenelse1_eq_for ifExthenelse1_eq_for_phi ifExthenelse1_eq_phi ifExthenelse1_false ifExthenelse1_false_for ifExthenelse1_min ifExthenelse1_min_for ifExthenelse1_solve ifExthenelse1_solve_for ifExthenelse1_split ifExthenelse1_split_for ifExthenelse1_unused_var ifExthenelse1_unused_var_for ifFalse ifSkipThen ifSkipThenConditionInBlock ifSplit ifSplitLeft ifTrue ifUnfold ifthenelse_concrete ifthenelse_concrete2 ifthenelse_concrete3 ifthenelse_concrete4 ifthenelse_equals ifthenelse_equals_1 ifthenelse_equals_2 ifthenelse_false ifthenelse_false_for ifthenelse_negated ifthenelse_negated_for ifthenelse_same_branches ifthenelse_same_branches_for ifthenelse_split ifthenelse_split_for ifthenelse_true ifthenelse_true_for inDomainConcrete inDomainOfMapEmpty inDomainOfMapForeach inDomainOfMapOverride inDomainOfMapRemove inDomainOfMapSingleton inDomainOfMapUpdate inDomainOfSeq2Map ineffectiveCast ineffectiveCast2 ineffectiveCast3 inequality_comparison_new inequality_comparison_simple initialized_class_is_not_erroneous initialized_class_is_prepared insert_constant_string_value insert_constant_value instanceCreation instanceCreationAssignment instanceCreationAssignmentUnfoldArguments instanceCreationUnfoldArguments instance_for_final_types instanceof_eval instanceof_known_dynamic_type instanceof_known_dynamic_type_2 instanceof_not_compatible instanceof_not_compatible_2 instanceof_not_compatible_3 instanceof_not_compatible_4 instanceof_not_compatible_5 instanceof_static_type instanceof_static_type_2 isFiniteOfMapEmpty isFiniteOfMapRemove isFiniteOfMapSingleton isFiniteOfMapUpdate isFiniteOfSeq2Map iterated_assignments_0 iterated_assignments_1 iterated_assignments_10 iterated_assignments_11 iterated_assignments_2 iterated_assignments_3 iterated_assignments_4 iterated_assignments_5 iterated_assignments_6 iterated_assignments_7 iterated_assignments_8 iterated_assignments_9 less_equal_than_comparison_new less_equal_than_comparison_simple less_than_comparison_new less_than_comparison_simple loopScopeInvBox loopScopeInvDia loopUnwind lsBreak lsContinue lsLblBreak lsLblContinueMatch lsLblContinueNoMatch1 lsLblContinueNoMatch2 lsReturnNonVoid lsReturnVoid lsThrow mapEqualityRight mapRemoveUnchanged mapRemoveUnchanged2 mapSizeNotNegativeForFiniteMaps mapUpdateUnchanged mapUpdateUnchanged2 maxAxiom measuredByCheck measuredByCheckEmpty memsetEmpty methodBodyExpand methodCall methodCall methodCall methodCallEmpty methodCallEmptyNoreturnBox methodCallEmptyReturn methodCallParamThrow methodCallReturn methodCallReturnIgnoreResult methodCallSuper methodCallThrow methodCallUnfoldArguments methodCallUnfoldTarget methodCallWithAssignment methodCallWithAssignment methodCallWithAssignment methodCallWithAssignmentSuper methodCallWithAssignmentUnfoldArguments methodCallWithAssignmentUnfoldTarget methodCallWithAssignmentWithinClass methodCallWithAssignmentWithinClass methodCallWithinClass methodCallWithinClass minAxiom narrowFinalArrayType narrowSelectArrayType narrowSelectType narrowTypeFinal nonNull nonNullZero notInDomain nullCreated nullIsNotNonNull nullString null_can_always_be_stored_in_a_reference_type_array observerDependency observerDependencyEQ observerDependencyEquiv observerDependencyFormula onlyCreatedObjectsAreInLocSets onlyCreatedObjectsAreInLocSetsEQ onlyCreatedObjectsAreInLocSetsEQFinal onlyCreatedObjectsAreInLocSetsFinal onlyCreatedObjectsAreObserved onlyCreatedObjectsAreObservedInLocSets onlyCreatedObjectsAreObservedInLocSetsEQ onlyCreatedObjectsAreReferenced onlyCreatedObjectsAreReferencedFinal only_created_objects_are_reachable parallelWithSkip1 parallelWithSkip2 passiveMethodCallStatic passiveMethodCallStaticWithAssignment passiveMethodCallWithAssignmentWithinClass passiveMethodCallWithinClass poolIsInjective poolKeyIsContentOfValue postdecrement postdecrement_array postdecrement_assignment postdecrement_assignment_array postdecrement_assignment_attribute postdecrement_attribute postincrement postincrement_array postincrement_assignment postincrement_assignment_array postincrement_assignment_attribute postincrement_attribute precOfInt precOfIntPair precOfPair precOfPairInt precOfSeq predecrement predecrement_array predecrement_assignment predecrement_assignment_array predecrement_assignment_attribute predecrement_attribute preincrement preincrement_array preincrement_assignment preincrement_assignment_array preincrement_assignment_attribute preincrement_attribute pullOutSelect reachAddOne reachAddOne2 reachDefinition reachDependenciesAnon reachDependenciesAnonCoarse reachDependenciesStore reachDependenciesStoreEQ reachDependenciesStoreSimple reachDependenciesStoreSimpleEQ reachDoesNotDependOnCreatedness reachEndOfUniquePath reachEndOfUniquePath2 reachNull reachNull2 reachOne reachUniquePathSameSteps reachZero reach_does_not_depend_on_fresh_locs reach_does_not_depend_on_fresh_locs_EQ reference_type_cast reference_type_cast reference_type_cast remove_parentheses_attribute_left remove_parentheses_lhs_left remove_parentheses_right returnUnfold sameTypeFalse sameTypeTrue same_boxes_left same_boxes_right same_diamonds_left same_diamonds_right secondOfPair selectCreatedOfAnon selectCreatedOfAnonAsFormula selectCreatedOfAnonAsFormulaEQ selectCreatedOfAnonEQ selectOfAnon selectOfAnonEQ selectOfCreate selectOfCreateEQ selectOfMemset selectOfMemsetEQ selectOfStore selectOfStoreEQ seqConcatUnfoldLeft seqConcatUnfoldRight seqGetUnfoldLeft seqGetUnfoldRight seqIndexOfUnfoldLeft seqIndexOfUnfoldRight seqLengthUnfold seqReverseUnfold seqSingletonUnfold seqSubUnfoldLeft seqSubUnfoldMiddle seqSubUnfoldRight sequentialToParallel1 sequentialToParallel2 sequentialToParallel3 setIntersectUnfoldLeft setIntersectUnfoldRight setJavaCardTransient setMinusUnfoldLeft setMinusUnfoldRight setUnionUnfoldLeft setUnionUnfoldRight simplifyIfThenElseUpdate1 simplifyIfThenElseUpdate2 simplifyIfThenElseUpdate3 simplifyIfThenElseUpdate4 simplifySelectOfAnon simplifySelectOfAnonEQ simplifySelectOfCreate simplifySelectOfCreateEQ simplifySelectOfMemset simplifySelectOfMemsetEQ simplifySelectOfStore simplifySelectOfStoreEQ simplifyUpdate1 simplifyUpdate2 simplifyUpdate3 singletonAssignment singletonUnfold sizeOfMapEmpty sizeOfMapRemove sizeOfMapSingleton sizeOfMapUpdate sizeOfSeq2Map skipAssert skipAssert_2 sortsDisjoint1 sortsDisjoint2 sortsDisjointModuloNull special_constructor_call ssubsortDirect ssubsortSup ssubsortTop staticMethodCall staticMethodCall staticMethodCallStaticViaTypereference staticMethodCallStaticViaTypereference staticMethodCallStaticWithAssignmentViaTypereference staticMethodCallStaticWithAssignmentViaTypereference staticMethodCallWithAssignment staticMethodCallWithAssignment stringAssignment stringConcat stringConcatBooleanLeft stringConcatBooleanRight stringConcatCharExpLeft stringConcatCharExpRight stringConcatIntExpLeft stringConcatIntExpRight stringConcatObjectLeft stringConcatObjectRight subsortTrans superclasses_of_initialized_classes_are_initialized superclasses_of_initialized_classes_are_prepared switch synchronizedBlockEmpty synchronizedBlockEmpty synchronizedBlockEmpty synchronizedBlockEmpty2 synchronizedBlockEvalSync threeBranchLoopScopeInvRuleBox threeBranchLoopScopeInvRuleDia throwBox throwDiamond throwLabel throwLabelBlock throwNull throwUnfold throwUnfoldMore true_to_not_false tryBreak tryBreakLabel tryCatchFinallyThrow tryCatchThrow tryEmpty tryFinallyBreak tryFinallyBreakLabel tryFinallyEmpty tryFinallyReturn tryFinallyReturnNoValue tryFinallyThrow tryMultipleCatchThrow tryReturn tryReturnNoValue try_continue_1 try_continue_2 try_finally_continue_1 try_finally_continue_2 typeEq typeEqDerived typeEqDerived2 typeStatic unusedLabel unwindLoopScope variableDeclaration variableDeclarationAssign variableDeclarationFinal variableDeclarationFinalAssign variableDeclarationGhost variableDeclarationGhostAssign variableDeclarationMult wd_Constant_Formula wd_Constant_Term wd_Equality_Pred wd_F_Logical_Op_And wd_F_Logical_Op_Cond_Form wd_F_Logical_Op_Eqv wd_F_Logical_Op_ExCond_Form wd_F_Logical_Op_Imp wd_F_Logical_Op_Neg wd_F_Logical_Op_Or wd_F_Logical_Quant_All wd_F_Logical_Quant_Exist wd_F_Resolve wd_F_Subst_Formula wd_Heap_Anon wd_Heap_ArrLength wd_Heap_Create wd_Heap_Memset wd_Heap_Pred_ArrStoreValid wd_Heap_Pred_NonNull wd_Heap_Pred_WellFormed wd_Heap_Reference wd_Heap_Reference_Array wd_Heap_Reference_Created wd_Heap_Reference_Static wd_Heap_Store wd_LocSet_AllElemsArr wd_LocSet_AllElemsArrLocsets wd_LocSet_AllFields wd_LocSet_AllFieldsArr wd_LocSet_AllObjects wd_LocSet_ArrRange wd_LocSet_Diff wd_LocSet_FreshLocs wd_LocSet_InfiniteUnion wd_LocSet_InfiniteUnion2 wd_LocSet_Intersect wd_LocSet_Pred_Disjoint wd_LocSet_Pred_ElementOf wd_LocSet_Pred_ElementOf_Static wd_LocSet_Pred_InHeap wd_LocSet_Pred_Subset wd_LocSet_Singleton wd_LocSet_Singleton_Arr wd_LocSet_Singleton_Quant wd_LocSet_Singleton_Static wd_LocSet_Union wd_Logical_Op_And wd_Logical_Op_And wd_Logical_Op_AndSC wd_Logical_Op_Cond_Expr wd_Logical_Op_Cond_Expr wd_Logical_Op_Cond_Expr wd_Logical_Op_Cond_Form wd_Logical_Op_Cond_Form wd_Logical_Op_Eqv wd_Logical_Op_Eqv wd_Logical_Op_ExCond_Expr wd_Logical_Op_ExCond_Expr wd_Logical_Op_ExCond_Expr wd_Logical_Op_ExCond_Form wd_Logical_Op_ExCond_Form wd_Logical_Op_Imp wd_Logical_Op_Imp wd_Logical_Op_Neg wd_Logical_Op_Neg wd_Logical_Op_Or wd_Logical_Op_Or wd_Logical_Op_OrSC wd_Logical_Quant_All wd_Logical_Quant_All wd_Logical_Quant_Exist wd_Logical_Quant_Exist wd_Numerical_Cast_Byte wd_Numerical_Cast_ByteOverFlow wd_Numerical_Cast_Char wd_Numerical_Cast_CharOverFlow wd_Numerical_Cast_Int wd_Numerical_Cast_IntOverFlow wd_Numerical_Cast_Long wd_Numerical_Cast_LongOverFlow wd_Numerical_Cast_Short wd_Numerical_Cast_ShortOverFlow wd_Numerical_Const wd_Numerical_Const_C wd_Numerical_Const_Z wd_Numerical_Mod_Byte wd_Numerical_Mod_Char wd_Numerical_Mod_Int wd_Numerical_Mod_Long wd_Numerical_Mod_Short wd_Numerical_Op_Add wd_Numerical_Op_AddInt wd_Numerical_Op_AddIntOverFlow wd_Numerical_Op_AddJInt wd_Numerical_Op_AddJLong wd_Numerical_Op_AddLong wd_Numerical_Op_AddLongOverFlow wd_Numerical_Op_AndJInt wd_Numerical_Op_AndJLong wd_Numerical_Op_BitAndInt wd_Numerical_Op_BitAndLong wd_Numerical_Op_BitNegInt wd_Numerical_Op_BitNegLong wd_Numerical_Op_BitOrInt wd_Numerical_Op_BitOrLong wd_Numerical_Op_BitXOrInt wd_Numerical_Op_BitXOrLong wd_Numerical_Op_CheckedAddInt wd_Numerical_Op_CheckedAddLong wd_Numerical_Op_CheckedBitNegInt wd_Numerical_Op_CheckedBitNegLong wd_Numerical_Op_CheckedBitwiseAndInt wd_Numerical_Op_CheckedBitwiseOrInt wd_Numerical_Op_CheckedBitwiseOrLong wd_Numerical_Op_CheckedBitwiseXOrInt wd_Numerical_Op_CheckedBitwiseXOrLong wd_Numerical_Op_CheckedDivInt wd_Numerical_Op_CheckedDivLong wd_Numerical_Op_CheckedMinusInt wd_Numerical_Op_CheckedMinusLong wd_Numerical_Op_CheckedMulInt wd_Numerical_Op_CheckedMulLong wd_Numerical_Op_CheckedShiftLeftInt wd_Numerical_Op_CheckedShiftLeftLong wd_Numerical_Op_CheckedShiftRightInt wd_Numerical_Op_CheckedShiftRightLong wd_Numerical_Op_CheckedSubInt wd_Numerical_Op_CheckedSubLong wd_Numerical_Op_CheckedUShiftRightInt wd_Numerical_Op_CheckedUShiftRightLong wd_Numerical_Op_Div wd_Numerical_Op_DivInt wd_Numerical_Op_DivIntOverFlow wd_Numerical_Op_DivJInt wd_Numerical_Op_DivJLong wd_Numerical_Op_DivLong wd_Numerical_Op_DivLongOverFlow wd_Numerical_Op_JDiv wd_Numerical_Op_JMod wd_Numerical_Op_JavaMod wd_Numerical_Op_JavaModOverFlow wd_Numerical_Op_JavaShiftLeftInt wd_Numerical_Op_JavaShiftLeftLong wd_Numerical_Op_JavaShiftRightInt wd_Numerical_Op_JavaShiftRightLong wd_Numerical_Op_JavaUnsignedShiftRightInt wd_Numerical_Op_JavaUnsignedShiftRightLong wd_Numerical_Op_MinusInt wd_Numerical_Op_MinusIntOverFlow wd_Numerical_Op_MinusJInt wd_Numerical_Op_MinusJLong wd_Numerical_Op_MinusLong wd_Numerical_Op_MinusLongOverFlow wd_Numerical_Op_Mod wd_Numerical_Op_ModJInt wd_Numerical_Op_ModJLong wd_Numerical_Op_Mul wd_Numerical_Op_MulInt wd_Numerical_Op_MulIntOverFlow wd_Numerical_Op_MulJInt wd_Numerical_Op_MulJLong wd_Numerical_Op_MulLong wd_Numerical_Op_MulLongOverFlow wd_Numerical_Op_Neg wd_Numerical_Op_OrJInt wd_Numerical_Op_OrJLong wd_Numerical_Op_ShiftLeftInt wd_Numerical_Op_ShiftLeftLong wd_Numerical_Op_ShiftRightInt wd_Numerical_Op_ShiftRightLong wd_Numerical_Op_Sub wd_Numerical_Op_SubInt wd_Numerical_Op_SubIntOverFlow wd_Numerical_Op_SubJInt wd_Numerical_Op_SubJLong wd_Numerical_Op_SubLong wd_Numerical_Op_SubLongOverFlow wd_Numerical_Op_UShiftRightInt wd_Numerical_Op_UShiftRightLong wd_Numerical_Op_XorJInt wd_Numerical_Op_XorJLong wd_Numerical_Op_checkedBitwiseAndLong wd_Numerical_Pred_Geq wd_Numerical_Pred_Gt wd_Numerical_Pred_InByte wd_Numerical_Pred_InChar wd_Numerical_Pred_InInt wd_Numerical_Pred_InLong wd_Numerical_Pred_InShort wd_Numerical_Pred_Leq wd_Numerical_Pred_Lt wd_Numerical_Pred_WellOrdered wd_Numerical_Pred_inRangeByte wd_Numerical_Pred_inRangeChar wd_Numerical_Pred_inRangeInt wd_Numerical_Pred_inRangeLong wd_Numerical_Pred_inRangeShort wd_Numerical_Quant_Bprod wd_Numerical_Quant_Bsum wd_Numerical_Quant_Max wd_Numerical_Quant_Min wd_Numerical_Quant_Prod wd_Numerical_Quant_Sum wd_Pair wd_Reach_Pred_Acc wd_Reach_Pred_Reach wd_RegEx wd_RegEx_Alt wd_RegEx_Concat wd_RegEx_Opt wd_RegEx_Plus wd_RegEx_Pred_Match wd_RegEx_Repeat wd_RegEx_Star wd_Seq_Concat wd_Seq_Def wd_Seq_Get wd_Seq_IndexOf wd_Seq_Length wd_Seq_NPermInv wd_Seq_Pred_NPerm wd_Seq_Pred_Perm wd_Seq_Remove wd_Seq_Reverse wd_Seq_Singleton wd_Seq_Sub wd_Seq_Swap wd_String_Hash wd_String_IndexOfChar wd_String_IndexOfStr wd_String_LastIndexOfChar wd_String_LastIndexOfStr wd_String_Pred_Contains wd_String_Pred_EndsWith wd_String_Pred_StartsWith wd_String_Replace wd_String_RmvZeros wd_String_Translate wd_Subst_Formula wd_Subst_Term wd_T_Logical_Op_And wd_T_Logical_Op_Cond_Form wd_T_Logical_Op_Eqv wd_T_Logical_Op_ExCond_Form wd_T_Logical_Op_Imp wd_T_Logical_Op_Neg wd_T_Logical_Op_Or wd_T_Logical_Quant_All wd_T_Logical_Quant_Exist wd_T_Resolve wd_T_Subst_Formula wd_Type_Cast wd_Type_ExactInstance wd_Type_Instance wd_Undef_Formula wd_Undef_Term wd_Y_Split wellFormedAnon wellFormedAnonEQ wellFormedCreate wellFormedMemsetArrayObject wellFormedMemsetArrayPrimitive wellFormedStoreArray wellFormedStoreLocSet wellFormedStoreLocSetEQ wellFormedStoreObject wellFormedStoreObjectEQ wellFormedStorePrimitive wellFormedStorePrimitiveArray wellFormedStorePrimitiveEQ

String activeUse adtProgramDecompositionRules assertions boolean booleanRules epsilon execRules forLoopRules freeADT genericRules heap heapRules ifThenElseRules infFlow instanceAllocation java5 javaHeader javaRules ldt loopInvariantRules loopRules loopScopeRules map mapSize optionsDeclarations precRules reach reachRules ruleSetsDeclarations soundDefaultContracts standardRules stringDef types updateRules wd wdFormulaRules wdGeneralRules wdHeader wdHeapRules wdLocSetRules wdNumericalRules wdReachRules wdRegExRules wdSeqRules wdStringRules wellfound

ABSTRACT ADD ADDPROGVARS ADDRULES ALIAS ANTECEDENTPOLARITY APPLY_UPDATE_ON_RIGID ASSIGN ASSUMES AT AVOID AXIOMS BOOTCLASSPATH CHOOSECONTRACT CLASSPATH CLOSEGOAL COLON COMMA CONTAINERTYPE CONTAINS_ASSIGNMENT CONTRACTS DATATYPES DEPENDINGON DIFFERENT DIFFERENTFIELDS DISJOINTMODULONULL DISPLAYNAME DOC_COMMENT DOT DOUBLECOLON DROP_EFFECTLESS_ELEMENTARIES DROP_EFFECTLESS_STORES ELEMSORT ELSE ENUM_CONST EQUALS EQUAL_UNIQUE EXP EXTENDS FALSE FIELDTYPE FINAL FIND FORMULA FREE FREELABELIN FUNCTIONS GENERIC GET_FREE_INVARIANT GET_INVARIANT GET_VARIANT GREATER HASLABEL HASSORT HASSUBFORMULAS HAS_ELEMENTARY_SORT HAS_INVARIANT HELPTEXT HEURISTICS HEURISTICSDECL IF IFEX INCLUDE INCLUDELDTS INSEQUENTSTATE INSTANTIATE_GENERIC INVARIANTS IN_TYPE ISARRAY ISARRAYLENGTH ISCONSTANT ISENUMTYPE ISINDUCTVAR ISINSTRICTFP ISLOCALVARIABLE ISMODELFIELD ISOBSERVER ISREFERENCE ISREFERENCEARRAY ISSTATICFIELD ISSUBTYPE ISTHISREFERENCE IS_ABSTRACT_OR_INTERFACE IS_FINAL IS_LABELED JAVASOURCE KEYSETTINGS LBRACE LBRACKET LEMMA LESS LPAREN MAXEXPANDMETHOD METADISJOINT MINUS ML_COMMENT MODAILITYGENERIC1 MODAILITYGENERIC2 MODAILITYGENERIC3 MODAILITYGENERIC4 MODAILITYGENERIC5 MODAILITYGENERIC6 MODAILITYGENERIC7 MODALITYB MODALITYBB MODALITYBB_END MODALITYB_END MODALITYD MODALITYD_END MODALITYG_END MODALOPERATOR MODIFIABLE NEW NEWLABEL NEW_DEPENDING_ON NEW_LOCAL_VARS NEW_TYPE_OF NODEFAULTCLASSES NONINTERACTIVE NOTFREEIN NOT_ ONEOF OPTIONSDECL PERCENT PLUS PREDICATES PROBLEM PROFILE PROGRAM PROGRAMVARIABLES PROOF PROOFOBLIGATION PROOFSCRIPT PROXY RBRACE RBRACKET REPLACEWITH RPAREN RULES SAME SAMEUPDATELEVEL SAME_OBSERVER SCHEMAVAR SCHEMAVARIABLES SEMI SIMPLIFY_IF_THEN_ELSE_UPDATE SKOLEMFORMULA SKOLEMTERM SLASH SORTS STAR STATIC STATICMETHODREFERENCE STORE_STMT_IN STORE_TERM_IN STRICT SUBST SUCCEDENTPOLARITY TERM TERMLABEL THEN TILDE TRANSFORMERS TRIGGER TRUE TYPEOF UNIQUE UPDATE VARCOND VARIABLE VARIABLES WITHOPTIONS