Skip to content

Commit b9b778c

Browse files
wadoonwadoon
committed
application of #3590 
1 parent 1e09b38 commit b9b778c

1,097 files changed

Lines changed: 81503 additions & 38266 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).JML operation contract.0.key‎

Lines changed: 74 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1,42 +1,79 @@
11
\profile "Java Profile";
22

3-
\settings {
4-
"#Proof-Settings-Config-File
5-
#Wed Jun 04 18:34:33 CEST 2014
6-
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
7-
[SMTSettings]useUninterpretedMultiplication=true
8-
[SMTSettings]SelectedTaclets=
9-
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
10-
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
11-
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
12-
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
13-
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
14-
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
15-
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
16-
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
17-
[SMTSettings]instantiateHierarchyAssumptions=true
18-
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
19-
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
20-
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
21-
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
22-
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
23-
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
24-
[Strategy]Timeout=-1
25-
[Strategy]MaximumNumberOfAutomaticApplications=10000
26-
[SMTSettings]integersMaximum=2147483645
27-
[Choice]DefaultChoices=assertions-assertions\\:on , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , runtimeExceptions-runtimeExceptions\\:ban
28-
[SMTSettings]useConstantsForBigOrSmallIntegers=true
29-
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
30-
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
31-
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
32-
[SMTSettings]maxGenericSorts=2
33-
[SMTSettings]integersMinimum=-2147483645
34-
[SMTSettings]invariantForall=false
35-
[SMTSettings]UseBuiltUniqueness=false
36-
[SMTSettings]explicitTypeHierarchy=false
37-
[Strategy]ActiveStrategy=JavaCardDLStrategy
38-
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
39-
"
3+
\settings{
4+
"Choice" : {
5+
"JavaCard" : "JavaCard\:on",
6+
"Strings" : "Strings\:on",
7+
"assertions" : "assertions\:on",
8+
"bigint" : "bigint\:on",
9+
"finalFields" : "finalFields:immutable",
10+
"floatRules" : "floatRules:strictfpOnly",
11+
"initialisation" : "initialisation\:disableStaticInitialisation",
12+
"intRules" : "intRules\:arithmeticSemanticsIgnoringOF",
13+
"integerSimplificationRules" : "integerSimplificationRules\:full",
14+
"javaLoopTreatment" : "javaLoopTreatment:efficient",
15+
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
16+
"methodExpansion" : "methodExpansion:modularOnly",
17+
"modelFields" : "modelFields\:treatAsAxiom",
18+
"moreSeqRules" : "moreSeqRules:off",
19+
"optimisedSelectRules" : "optimisedSelectRules\:on",
20+
"permissions" : "permissions:off",
21+
"programRules" : "programRules\:Java",
22+
"reach" : "reach\:on",
23+
"runtimeExceptions" : "runtimeExceptions\:ban",
24+
"sequences" : "sequences\:on",
25+
"soundDefaultContracts" : "soundDefaultContracts:on",
26+
"wdChecks" : "wdChecks\:off",
27+
"wdOperator" : "wdOperator\:L"
28+
},
29+
"Labels" : {
30+
"UseOriginLabels" : true
31+
},
32+
"NewSMT" : {
33+
34+
},
35+
"SMTSettings" : {
36+
"SelectedTaclets" : [
37+
38+
],
39+
"UseBuiltUniqueness" : false,
40+
"explicitTypeHierarchy" : false,
41+
"instantiateHierarchyAssumptions" : true,
42+
"integersMaximum" : 2147483645,
43+
"integersMinimum" : -2147483645,
44+
"invariantForall" : false,
45+
"maxGenericSorts" : 2,
46+
"useConstantsForBigOrSmallIntegers" : true,
47+
"useUninterpretedMultiplication" : true
48+
},
49+
"Strategy" : {
50+
"ActiveStrategy" : "JavaCardDLStrategy",
51+
"MaximumNumberOfAutomaticApplications" : 10000,
52+
"Timeout" : -1,
53+
"options" : {
54+
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
55+
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
56+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
57+
"DEP_OPTIONS_KEY" : "DEP_ON",
58+
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
59+
"LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
60+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
61+
"MPS_OPTIONS_KEY" : "MPS_MERGE",
62+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE",
63+
"OSS_OPTIONS_KEY" : "OSS_ON",
64+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
65+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF",
66+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
67+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
68+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
69+
"SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
70+
"SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
71+
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
72+
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
73+
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
74+
"VBT_PHASE" : "VBT_SYM_EX"
75+
}
76+
}
4077
}
4178

4279
\javaSource "src/contract";

‎key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.key‎

Lines changed: 74 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1,42 +1,79 @@
11
\profile "Java Profile";
22

3-
\settings {
4-
"#Proof-Settings-Config-File
5-
#Wed Jun 04 18:34:33 CEST 2014
6-
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
7-
[SMTSettings]useUninterpretedMultiplication=true
8-
[SMTSettings]SelectedTaclets=
9-
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
10-
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
11-
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
12-
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
13-
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
14-
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
15-
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
16-
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
17-
[SMTSettings]instantiateHierarchyAssumptions=true
18-
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
19-
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
20-
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
21-
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
22-
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
23-
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
24-
[Strategy]Timeout=-1
25-
[Strategy]MaximumNumberOfAutomaticApplications=10000
26-
[SMTSettings]integersMaximum=2147483645
27-
[Choice]DefaultChoices=assertions-assertions\\:on , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , runtimeExceptions-runtimeExceptions\\:ban
28-
[SMTSettings]useConstantsForBigOrSmallIntegers=true
29-
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
30-
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
31-
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
32-
[SMTSettings]maxGenericSorts=2
33-
[SMTSettings]integersMinimum=-2147483645
34-
[SMTSettings]invariantForall=false
35-
[SMTSettings]UseBuiltUniqueness=false
36-
[SMTSettings]explicitTypeHierarchy=false
37-
[Strategy]ActiveStrategy=JavaCardDLStrategy
38-
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
39-
"
3+
\settings{
4+
"Choice" : {
5+
"JavaCard" : "JavaCard\:on",
6+
"Strings" : "Strings\:on",
7+
"assertions" : "assertions\:on",
8+
"bigint" : "bigint\:on",
9+
"finalFields" : "finalFields:immutable",
10+
"floatRules" : "floatRules:strictfpOnly",
11+
"initialisation" : "initialisation\:disableStaticInitialisation",
12+
"intRules" : "intRules\:arithmeticSemanticsIgnoringOF",
13+
"integerSimplificationRules" : "integerSimplificationRules\:full",
14+
"javaLoopTreatment" : "javaLoopTreatment:efficient",
15+
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
16+
"methodExpansion" : "methodExpansion:modularOnly",
17+
"modelFields" : "modelFields\:treatAsAxiom",
18+
"moreSeqRules" : "moreSeqRules:off",
19+
"optimisedSelectRules" : "optimisedSelectRules\:on",
20+
"permissions" : "permissions:off",
21+
"programRules" : "programRules\:Java",
22+
"reach" : "reach\:on",
23+
"runtimeExceptions" : "runtimeExceptions\:ban",
24+
"sequences" : "sequences\:on",
25+
"soundDefaultContracts" : "soundDefaultContracts:on",
26+
"wdChecks" : "wdChecks\:off",
27+
"wdOperator" : "wdOperator\:L"
28+
},
29+
"Labels" : {
30+
"UseOriginLabels" : true
31+
},
32+
"NewSMT" : {
33+
34+
},
35+
"SMTSettings" : {
36+
"SelectedTaclets" : [
37+
38+
],
39+
"UseBuiltUniqueness" : false,
40+
"explicitTypeHierarchy" : false,
41+
"instantiateHierarchyAssumptions" : true,
42+
"integersMaximum" : 2147483645,
43+
"integersMinimum" : -2147483645,
44+
"invariantForall" : false,
45+
"maxGenericSorts" : 2,
46+
"useConstantsForBigOrSmallIntegers" : true,
47+
"useUninterpretedMultiplication" : true
48+
},
49+
"Strategy" : {
50+
"ActiveStrategy" : "JavaCardDLStrategy",
51+
"MaximumNumberOfAutomaticApplications" : 10000,
52+
"Timeout" : -1,
53+
"options" : {
54+
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
55+
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
56+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
57+
"DEP_OPTIONS_KEY" : "DEP_ON",
58+
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
59+
"LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
60+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
61+
"MPS_OPTIONS_KEY" : "MPS_MERGE",
62+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE",
63+
"OSS_OPTIONS_KEY" : "OSS_ON",
64+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
65+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF",
66+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
67+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
68+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
69+
"SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
70+
"SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
71+
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
72+
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
73+
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
74+
"VBT_PHASE" : "VBT_SYM_EX"
75+
}
76+
}
4077
}
4178

4279
\javaSource "src/contract";

‎key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.m.key‎

Lines changed: 74 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1,42 +1,79 @@
11
\profile "Java Profile";
22

3-
\settings {
4-
"#Proof-Settings-Config-File
5-
#Wed Jun 04 18:34:33 CEST 2014
6-
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
7-
[SMTSettings]useUninterpretedMultiplication=true
8-
[SMTSettings]SelectedTaclets=
9-
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
10-
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
11-
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
12-
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
13-
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
14-
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
15-
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
16-
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
17-
[SMTSettings]instantiateHierarchyAssumptions=true
18-
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
19-
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
20-
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
21-
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
22-
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
23-
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
24-
[Strategy]Timeout=-1
25-
[Strategy]MaximumNumberOfAutomaticApplications=10000
26-
[SMTSettings]integersMaximum=2147483645
27-
[Choice]DefaultChoices=assertions-assertions\\:on , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , runtimeExceptions-runtimeExceptions\\:ban
28-
[SMTSettings]useConstantsForBigOrSmallIntegers=true
29-
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
30-
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
31-
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
32-
[SMTSettings]maxGenericSorts=2
33-
[SMTSettings]integersMinimum=-2147483645
34-
[SMTSettings]invariantForall=false
35-
[SMTSettings]UseBuiltUniqueness=false
36-
[SMTSettings]explicitTypeHierarchy=false
37-
[Strategy]ActiveStrategy=JavaCardDLStrategy
38-
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
39-
"
3+
\settings{
4+
"Choice" : {
5+
"JavaCard" : "JavaCard\:on",
6+
"Strings" : "Strings\:on",
7+
"assertions" : "assertions\:on",
8+
"bigint" : "bigint\:on",
9+
"finalFields" : "finalFields:immutable",
10+
"floatRules" : "floatRules:strictfpOnly",
11+
"initialisation" : "initialisation\:disableStaticInitialisation",
12+
"intRules" : "intRules\:arithmeticSemanticsIgnoringOF",
13+
"integerSimplificationRules" : "integerSimplificationRules\:full",
14+
"javaLoopTreatment" : "javaLoopTreatment:efficient",
15+
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
16+
"methodExpansion" : "methodExpansion:modularOnly",
17+
"modelFields" : "modelFields\:treatAsAxiom",
18+
"moreSeqRules" : "moreSeqRules:off",
19+
"optimisedSelectRules" : "optimisedSelectRules\:on",
20+
"permissions" : "permissions:off",
21+
"programRules" : "programRules\:Java",
22+
"reach" : "reach\:on",
23+
"runtimeExceptions" : "runtimeExceptions\:ban",
24+
"sequences" : "sequences\:on",
25+
"soundDefaultContracts" : "soundDefaultContracts:on",
26+
"wdChecks" : "wdChecks\:off",
27+
"wdOperator" : "wdOperator\:L"
28+
},
29+
"Labels" : {
30+
"UseOriginLabels" : true
31+
},
32+
"NewSMT" : {
33+
34+
},
35+
"SMTSettings" : {
36+
"SelectedTaclets" : [
37+
38+
],
39+
"UseBuiltUniqueness" : false,
40+
"explicitTypeHierarchy" : false,
41+
"instantiateHierarchyAssumptions" : true,
42+
"integersMaximum" : 2147483645,
43+
"integersMinimum" : -2147483645,
44+
"invariantForall" : false,
45+
"maxGenericSorts" : 2,
46+
"useConstantsForBigOrSmallIntegers" : true,
47+
"useUninterpretedMultiplication" : true
48+
},
49+
"Strategy" : {
50+
"ActiveStrategy" : "JavaCardDLStrategy",
51+
"MaximumNumberOfAutomaticApplications" : 10000,
52+
"Timeout" : -1,
53+
"options" : {
54+
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
55+
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
56+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
57+
"DEP_OPTIONS_KEY" : "DEP_ON",
58+
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
59+
"LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
60+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
61+
"MPS_OPTIONS_KEY" : "MPS_MERGE",
62+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE",
63+
"OSS_OPTIONS_KEY" : "OSS_ON",
64+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
65+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF",
66+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
67+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
68+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
69+
"SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
70+
"SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
71+
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
72+
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
73+
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
74+
"VBT_PHASE" : "VBT_SYM_EX"
75+
}
76+
}
4077
}
4178

4279
\javaSource "src/contract";

0 commit comments

Comments
 (0)