Commit 355cbdea authored by uiekn's avatar uiekn

Add proof script for toList method

parent 6250d812
......@@ -16,7 +16,8 @@ rule replaceKnownSelect_taclet000100_14
on="Seq::select(heapAfter_add, result_0, java.util.Collection::$seq)"
inst_EQ="heapAfter_add"
inst_o="result_0"
inst_f="java.util.Collection::$seq";
inst_f="java.util.Collection::$seq"
inst_sk="java_util_Collection_seq_5<<selectSK>>";
rule replaceKnownAuxiliaryConstant_taclet000100_15
formula="!java.lang.String::seqGet(java_util_Collection_seq_5<<selectSK>>, i_1) = null"
on="java_util_Collection_seq_5<<selectSK>>";
......@@ -35,6 +36,7 @@ rule applyEq
rule applyEqReverse
formula="!(java.lang.String)result_2 = null"
on="result_2"
inst_t1="result_2"
inst_s="(java.lang.Object::seqGet(java_util_Collection_seq_3<<selectSK>>, i_0))";
rule seqCastRemoveBeta
formula="!(java.lang.String)(java.lang.Object::seqGet(java_util_Collection_seq_3<<selectSK>>, i_0)) = null";
......
\settings {
"#Proof-Settings-Config-File
#Wed Jun 26 10:00:00 CEST 2019
[Labels]UseOriginLabels=false
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
[SMTSettings]useUninterpretedMultiplication=true
[SMTSettings]SelectedTaclets=
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[Choice]DefaultChoices=programRules-programRules\\:Java , intRules-intRules\\:javaSemantics , assertions-assertions\\:on , initialisation-initialisation\\:disableStaticInitialisation , runtimeExceptions-runtimeExceptions\\:allow , JavaCard-JavaCard\\:off , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\:off
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
[SMTSettings]maxGenericSorts=2
[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
[SMTSettings]integersMinimum=-2147483645
[SMTSettings]integersMaximum=2147483645
[SMTSettings]invariantForall=false
[SMTSettings]UseBuiltUniqueness=false
[SMTSettings]explicitTypeHierarchy=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
"
}
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::toList(java.util.ArrayList,java.lang.String)].JML normal_behavior operation contract.0";
\proofScript "script 'toList2.script';"
macro autopilot steps;
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment