Skip to content

Commit

Permalink
make information flow examples use traditional final treatment.
Browse files Browse the repository at this point in the history
  • Loading branch information
@mattulbrich
mattulbrich committed Feb 22, 2025
1 parent 27f1584 commit 022ce5a
Show file tree
Hide file tree
Showing 54 changed files with 54 additions and 54 deletions.
2 changes: 1 addition & 1 deletion key.ui/examples/InformationFlow/SimpleEvoting/README.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,4 +17,4 @@ Voters send their secrete votes (encrypted, but this not modeled throughout in t

The difficult part in this case-study is to show that indeed only the correct result of the election is declassified.


(This example expands constructors for classes with final fields. For this to work, final fields are treated like ordinary fields.)
2 changes: 1 addition & 1 deletion key.ui/examples/InformationFlow/SimpleEvoting/project.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...imple_evoting.Environment(simple_evoting.Environment___rep()).JML accessible clause.0.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...imple_evoting.Environment__untrustedInput()).JML normal_behavior operation contract.0.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...Environment(simple_evoting.Environment__untrustedInput()).Non-interference contract.0.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...vironment(simple_evoting.Environment__untrustedInput()).Non-interference contract.0.m.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...le_evoting.Environment__untrustedInput(int)).JML normal_behavior operation contract.0.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...ironment(simple_evoting.Environment__untrustedInput(int)).Non-interference contract.0.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...onment(simple_evoting.Environment__untrustedInput(int)).Non-interference contract.0.m.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...ting.Environment__untrustedInputMessage((B)).JML normal_behavior operation contract.0.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...nt(simple_evoting.Environment__untrustedInputMessage((B)).Non-interference contract.0.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...(simple_evoting.Environment__untrustedInputMessage((B)).Non-interference contract.0.m.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...voting.Environment__untrustedInputMessage()).JML normal_behavior operation contract.0.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...ment(simple_evoting.Environment__untrustedInputMessage()).Non-interference contract.0.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
2 changes: 1 addition & 1 deletion ...nt(simple_evoting.Environment__untrustedInputMessage()).Non-interference contract.0.m.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[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
[Choice]DefaultChoices=finalFields\\:onHeap , 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
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
Expand Down
Loading

0 comments on commit 022ce5a

Please sign in to comment.