...
 
Commits (5)
\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_EXTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\includeFile "rules.key";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::CredTool(java.lang.String,java.lang.String,java.lang.String)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\includeFile "rules.key";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::<init>(java.lang.String,java.lang.String,java.lang.String)].JML normal_behavior block contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\includeFile "rules.key";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::<init>(java.lang.String,java.lang.String,java.lang.String)].JML normal_behavior block contract.1";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\includeFile "rules.key";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::<init>(java.lang.String,java.lang.String,java.lang.String)].JML normal_behavior block contract.2";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::addInputCol(java.util.ArrayList,java.lang.String,org.apache.commons.csv.CSVRecord)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::addInputCol(java.util.ArrayList,java.lang.String,org.apache.commons.csv.CSVRecord)].Non-interference contract.0";
\proofScript "auto steps=100000;"
......@@ -47,4 +47,4 @@
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::addInputCols()].JML normal_behavior operation contract.0";
\proofScript "script 'addInputCols_functional.script';"
\proofScript "script 'CredTool_addInputCols_functional.script';"
macro autopilot;
# Invariant Initially Valid:
rule castAdd
formula="java.lang.Object::<inv>(heapAfter_iterator, result)"
on="result";
auto;
# Body Preserves Invariant:
# Normal Execution
rule castAdd
formula="java.lang.Object::<inv>(heapAfter_addInputCol, result)"
on="result";
auto;
rule "One Step Simplification";
macro autopilot;
rule applyEqReverse
......
......@@ -47,4 +47,4 @@
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::addInputCols()].Non-interference contract.0";
\proofScript "script 'addInputCols_inf_flow.script';"
\proofScript "script 'CredTool_addInputCols_inf_flow.script';"
......@@ -4,9 +4,22 @@ rule andLeft;
macro symbex occ=0;
select branch="Invariant Initially Valid";
rule andRight
matches="&.*&.*java\.lang\.Object::<inv>\(heapAfter_iterator, result\)";
auto;
rule castAdd
formula="java.lang.Object::<inv>(heapAfter_iterator, result)"
on="result";
rule Class_invariant_axiom_for_java_util_CollectionIterator
formula="java.lang.Object::<inv>(heapAfter_iterator, (java.util.CollectionIterator)result)";
auto;
select branch="Pre (hasNext)";
rule castAdd
formula="java.lang.Object::<inv>(heapAfter_iterator, result)"
on="result";
rule Class_invariant_axiom_for_java_util_CollectionIterator
formula="java.lang.Object::<inv>(heapAfter_iterator, (java.util.CollectionIterator)result)";
auto;
select branch="Information Flow Validity";
......@@ -16,7 +29,7 @@ rule andLeft;
macro symbex occ=0;
select branch="Pre (hasNext)";
rule "castAdd"
formula="it_A.<inv>@heapAfter_addInputCol"
formula="java.lang.Object::<inv>(heapAfter_addInputCol, it_A)"
on="it_A";
auto;
......@@ -43,7 +56,6 @@ macro symbex occ=0;
select branch="Pre (addInputCol)";
rule "One Step Simplification";
macro autopilot;
macro autopilot;
select branch="Pre (hasNext)";
rule "One Step Simplification";
rule "castAdd"
......@@ -54,14 +66,39 @@ macro symbex occ=0;
auto steps=50000;
macro autopilot;
macro symbex;
tryclose;
assert goals=2;
assert goals=4;
select number=1;
select branch="Invariant Initially Valid";
rule "One Step Simplification";
macro autopilot;
auto;
rule castAdd
formula="java.lang.Object::<inv>(heapAfter_iterator_0, result_3)"
on="result_3";
rule Class_invariant_axiom_for_java_util_CollectionIterator
formula="java.lang.Object::<inv>(heapAfter_iterator_0, (java.util.CollectionIterator)result_3)";
auto;
auto;
rule castAdd
formula="java.lang.Object::<inv>(heapAfter_iterator_0, result_3)"
on="result_3";
rule Class_invariant_axiom_for_java_util_CollectionIterator
formula="java.lang.Object::<inv>(heapAfter_iterator_0, (java.util.CollectionIterator)result_3)";
auto;
select branch="Pre (hasNext)";
rule castAdd
formula="java.lang.Object::<inv>(heapAfter_iterator_0, result_3)"
on="result_3";
rule Class_invariant_axiom_for_java_util_CollectionIterator
formula="java.lang.Object::<inv>(heapAfter_iterator_0, (java.util.CollectionIterator)result_3)";
auto;
select branch="Information Flow Validity";
rule "One Step Simplification";
rule impRight;
rule andLeft;
......@@ -113,14 +150,3 @@ macro symbex occ=0;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::exitIfIdInvalid(java.lang.String)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::exitIfIdInvalid(java.lang.String)].Non-interference contract.0";
\proofScript "auto steps=100000;"
......@@ -47,4 +47,4 @@
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::extractInputColsForDist(java.util.LinkedList,java.lang.String)].JML normal_behavior operation contract.0";
\proofScript "script 'extractInputColsForDist.script';"
\proofScript "script 'CredTool_extractInputColsForDist.script';"
......@@ -5,9 +5,24 @@ rule applyEqReverse
formula="java.lang.String::instance(result_4) = TRUE"
on="result_4";
rule seqCastInstance
formula="java.lang.String::instance(java.lang.Object::seqGet(Seq::select(anon_heap_iterator<<anonHeapFunction>>, result_0, java.util.Iterator::$seq), int::select(anon_heap_LOOP<<anonHeapFunction>>, result_0, java.util.Iterator::$index))) = TRUE";
formula="java.lang.String::instance(java.lang.Object::seqGet(Seq::select(heap, cols, java.util.Collection::$seq), int::select(anon_heap_LOOP<<anonHeapFunction>>, result_0, java.util.Iterator::$index))) = TRUE";
tryclose;
select branch="Invariant Initially Valid";
rule "One Step Simplification";
macro autopilot;
rule castAdd
formula="java.lang.Object::<inv>(heapAfter_iterator, result_0)"
on="result_0";
auto;
select branch="if x_1 false";
macro autopilot;
rule castAdd
formula="java.lang.Object::<inv>(heapAfter_equals, result_0)"
on="result_0";
auto;
macro autopilot;
select formula="\forall int i; (     geq(i, Z(0(#))) & lt(i, seqLen(Seq::select(heapAfter_add, self, java.util.Collection::$seq))) -> !  java.lang.String::seqGet(Seq::select(heapAfter_add, self, java.util.Collection::$seq), i) = null)";
......@@ -16,8 +31,17 @@ rule impRight;
cut "seqLen(Seq::select(anon_heap_LOOP<<anonHeapFunction>>, self, java.util.Collection::$seq)) = i_0";
select branch="CUT: seqLen(Seq::select(anon_heap_LOOP<<anonHeapFunction>>, self, java.util.Collection::$seq)) = i_0 TRUE";
rule ifthenelse_split;
auto;
auto;
auto;
tryclose steps=1000000;
select formula="java.lang.Object::<inv>(heapAfter_add, result_0)";
rule castAdd
formula="java.lang.Object::<inv>(heapAfter_add, result_0)"
on="result_0";
rule Class_invariant_axiom_for_java_util_CollectionIterator
formula="java.lang.Object::<inv>(heapAfter_add, (java.util.CollectionIterator)result_0)";
auto;
select formula="\forall int i; (     geq(i, Z(0(#))) & lt(i, seqLen(Seq::select(heapAfter_add, self, java.util.Collection::$seq))) -> !  java.lang.String::seqGet(Seq::select(heapAfter_add, self, java.util.Collection::$seq), i) = null)";
rule allRight;
......@@ -25,24 +49,16 @@ rule impRight;
cut "seqLen(Seq::select(anon_heap_LOOP<<anonHeapFunction>>, self, java.util.Collection::$seq)) = i_0";
select branch="CUT: seqLen(Seq::select(anon_heap_LOOP<<anonHeapFunction>>, self, java.util.Collection::$seq)) = i_0 TRUE";
rule ifthenelse_split;
tryclose steps=1000000;
select number=0;
select branch="lt(Z(0(#)), add(mul(seqLen(Seq::select(anon_heap_LOOP<<anonHeapFunction>>, self, java.util.Collection::$seq)), Z(neglit(1(#)))), seqLen(Seq::select(anon_heap_add<<anonHeapFunction>>, self, java.util.Collection::$seq)))) TRUE";
rule applyEqReverse
formula="!java.lang.String::seqGet(Seq::select(heapAfter_add, self, java.util.Collection::$seq), i_0) = null"
on="i_0";
rule replaceKnownSelect_taclet00000000100_20
rule replaceKnownSelect_taclet00000000100_19
formula="!  java.lang.String::seqGet(Seq::select(heapAfter_add, self, java.util.Collection::$seq), seqLen(Seq::select(anon_heap_LOOP<<anonHeapFunction>>, self, java.util.Collection::$seq))) = null"
on="Seq::select(heapAfter_add, self, java.util.Collection::$seq)"
inst_EQ="heapAfter_add"
inst_o="self"
inst_f="java.util.Collection::$seq"
inst_sk="java_util_Collection_seq_5<<selectSK>>";
rule replaceKnownAuxiliaryConstant_taclet00000000100_21
formula="!java.lang.String::seqGet(java_util_Collection_seq_5<<selectSK>>, seqLen(Seq::select(anon_heap_LOOP<<anonHeapFunction>>, self, java.util.Collection::$seq))) = null"
on="java_util_Collection_seq_5<<selectSK>>";
on="Seq::select(heapAfter_add, self, java.util.Collection::$seq)";
rule replaceKnownAuxiliaryConstant_taclet00000000100_20
formula="!java.lang.String::seqGet(java_util_Collection_seq_4<<selectSK>>, seqLen(Seq::select(anon_heap_LOOP<<anonHeapFunction>>, self, java.util.Collection::$seq))) = null"
on="java_util_Collection_seq_4<<selectSK>>";
rule seqGetAlphaCast
formula="!  java.lang.String::seqGet(Seq::select(anon_heap_add<<anonHeapFunction>>, self, java.util.Collection::$seq), seqLen(Seq::select(anon_heap_LOOP<<anonHeapFunction>>, self, java.util.Collection::$seq))) = null"
on="java.lang.String::seqGet(Seq::select(anon_heap_add<<anonHeapFunction>>, self, java.util.Collection::$seq), seqLen(Seq::select(anon_heap_LOOP<<anonHeapFunction>>, self, java.util.Collection::$seq)))";
......@@ -56,3 +72,19 @@ rule castDel
formula="!(java.lang.String)((java.lang.String)result_4) = null"
on="(java.lang.String)((java.lang.String)result_4)";
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
auto;
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\includeFile "rules.key";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::extractInputColsForPolyas(java.util.LinkedList,java.lang.String)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::generateDataForVoter(org.apache.commons.csv.CSVRecord,java.lang.String)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\includeFile "rules.key";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::initDistVals(org.apache.commons.csv.CSVRecord,de.polyas.core3.open.cred.CredentialGenerator.GeneratedDataForVoter)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::initPolyasValsAddDataForVoter(org.apache.commons.csv.CSVRecord,de.polyas.core3.open.cred.CredentialGenerator.GeneratedDataForVoter)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\includeFile "rules.key";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::initPolyasValsAddInputCols(org.apache.commons.csv.CSVRecord)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::initPolyasVals(org.apache.commons.csv.CSVRecord,de.polyas.core3.open.cred.CredentialGenerator.GeneratedDataForVoter)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::parseInput(java.lang.String)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::parseInputCols(java.lang.String)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::printDist(java.util.ArrayList)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::printPolyas(java.util.ArrayList)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::printStatus()].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::printStatus()].Non-interference contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\includeFile "rules.key";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::processCSVRecord(org.apache.commons.csv.CSVRecord,java.lang.String)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
......@@ -47,4 +47,4 @@
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::processCSVRecord(org.apache.commons.csv.CSVRecord,java.lang.String)].Non-interference contract.0";
\proofScript "script 'processCSVRecord_inf_flow.script';"
\proofScript "script 'CredTool_processCSVRecord_inf_flow.script';"
This diff is collapsed.
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::readPublicKey(java.lang.String)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
......@@ -47,4 +47,4 @@
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::toArray(java.util.ArrayList)].JML normal_behavior operation contract.0";
\proofScript "script 'toArray.script';"
\proofScript "script 'CredTool_toArray.script';"
......@@ -47,4 +47,4 @@
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::toList(java.lang.String,java.util.ArrayList)].JML normal_behavior operation contract.0";
\proofScript "script 'toList.script';"
\proofScript "script 'CredTool_toList.script';"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\includeFile "rules.key";
\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 "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\includeFile "rules.key";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::toList(java.util.ArrayList)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::voterIdCheck(java.lang.String)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredTool[de.polyas.core3.open.cred.CredTool::voterIdCheck(java.lang.String)].Non-interference contract.0";
\proofScript "auto steps=100000;"
\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_INTERNAL
[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
"
}
\bootclasspath "boot";
\javaSource "src/main";
\chooseContract "de.polyas.core3.open.cred.CredentialGenerator[de.polyas.core3.open.cred.CredentialGenerator::generateDataForVoter(java.lang.String,java.lang.String)].JML normal_behavior operation contract.0";
\proofScript "auto steps=100000;"
\settings {
"#Proof-Settings-Config-File