Skip to content

Commit

Permalink
Added test cases
Browse files Browse the repository at this point in the history
  • Loading branch information
Cornelius committed Nov 1, 2023
1 parent 878fe9e commit c386d39
Show file tree
Hide file tree
Showing 48 changed files with 999 additions and 1,664 deletions.
Binary file modified .DS_Store
View file
Binary file not shown.
18 changes: 14 additions & 4 deletions BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccount/Statement1.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

\settings {
"#Proof-Settings-Config-File
#Tue Aug 23 16:24:44 CEST 2022
#Tue Oct 31 20:31:48 CET 2023
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
[SMTSettings]invariantForall=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
Expand Down Expand Up @@ -39,7 +39,17 @@
"
}

\javaSource "C:/Users/mko/Documents/ISF/0_feat-CorC2.0modifiable/runtime-EclipseApplication/BankAccount";\include "helper.key";\programVariables {int newBalance; int x; boolean ret; int x_old; boolean ret_old; Account self; Heap heapAtPre;}\problem {
\javaSource "../../../../..";
\include "helper.key";
\programVariables {
int newBalance;
int x;
boolean ret;
int x_old;
boolean ret_old;
Account self;
Heap heapAtPre;
}\problem {
true
& int::select(heap,
self,
Expand Down Expand Up @@ -67,9 +77,9 @@
}

\proof {
(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89"))
(keyLog "0" (keyUser "conni" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89"))

(autoModeTime "86")
(autoModeTime "73")

(branch "dummy ID"
(builtin "One Step Simplification" (formula "1"))
Expand Down
16 changes: 13 additions & 3 deletions ...Account/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimit/Statement1.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

\settings {
"#Proof-Settings-Config-File
#Tue Aug 23 16:24:55 CEST 2022
#Tue Oct 31 20:31:50 CET 2023
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
[SMTSettings]invariantForall=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
Expand Down Expand Up @@ -39,7 +39,17 @@
"
}

\javaSource "C:/Users/mko/Documents/ISF/0_feat-CorC2.0modifiable/runtime-EclipseApplication/BankAccount";\include "helper.key";\programVariables {int newBalance; int x; boolean ret; int x_old; boolean ret_old; Account self; Heap heapAtPre;}\problem {
\javaSource "../../../../..";
\include "helper.key";
\programVariables {
int newBalance;
int x;
boolean ret;
int x_old;
boolean ret_old;
Account self;
Heap heapAtPre;
}\problem {
true
& int::select(heap,
self,
Expand Down Expand Up @@ -67,7 +77,7 @@
}

\proof {
(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89"))
(keyLog "0" (keyUser "conni" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89"))

(autoModeTime "100")

Expand Down
142 changes: 11 additions & 131 deletions ...features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitInterest/Statement1.key
View file
Original file line number Diff line number Diff line change
@@ -1,131 +1,11 @@
\profile "Java Profile";

\settings {
"#Proof-Settings-Config-File
#Tue Aug 23 16:25:15 CEST 2022
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
[SMTSettings]invariantForall=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
[Choice]DefaultChoices=initialisation-initialisation\\:disableStaticInitialisation , wdChecks-wdChecks\\:off , optimisedSelectRules-optimisedSelectRules\\:on , reach-reach\\:on , moreSeqRules-moreSeqRules\\:off , sequences-sequences\\:on , Strings-Strings\\:on , joinGenerateIsWeakeningGoal-joinGenerateIsWeakeningGoal\\:off , runtimeExceptions-runtimeExceptions\\:ban , wdOperator-wdOperator\\:L , JavaCard-JavaCard\\:off , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , modelFields-modelFields\\:showSatisfiability , assertions-assertions\\:on , intRules-intRules\\:arithmeticSemanticsIgnoringOF , bigint-bigint\\:on , programRules-programRules\\:Java
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_EXPAND
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
[SMTSettings]UseBuiltUniqueness=false
[SMTSettings]explicitTypeHierarchy=false
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS
[SMTSettings]SelectedTaclets=
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[Strategy]MaximumNumberOfAutomaticApplications=2147483647
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_NONCLOSE
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
[Strategy]Timeout=-1
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_RESTRICTED
[SMTSettings]useUninterpretedMultiplication=true
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
[SMTSettings]maxGenericSorts=2
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
[SMTSettings]integersMinimum=-2147483645
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
[SMTSettings]integersMaximum=2147483645
"
}

\javaSource "C:/Users/mko/Documents/ISF/0_feat-CorC2.0modifiable/runtime-EclipseApplication/BankAccount";\include "helper.key";\programVariables {int newBalance; int x; boolean ret; int x_old; boolean ret_old; Account self; Heap heapAtPre;}\problem {
true
& int::select(heap,
self,
Account::$OVERDRAFT_LIMIT)
= Z(0(#))
& boolean::select(heap,
self,
java.lang.Object::<created>)
= TRUE
& Account::exactInstance(self) = TRUE
& !self = null
& java.lang.Object::<inv>(heap, self)
& wellFormed(heap)
-> {heapAtPre:=heap || x_old:=x || ret_old:=ret}
\<{
newBalance=self.balance-x;
}\> ( newBalance
= sub(int::select(heap,
self,
Account::$balance),
x)
& x = x_old
& ret = ret_old)

}

\proof {
(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89"))

(autoModeTime "94")

(branch "dummy ID"
(builtin "One Step Simplification" (formula "1"))
(rule "impRight" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "notLeft" (formula "2"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "eqSymm" (formula "7") (term "1,0,0,1"))
(rule "eqSymm" (formula "7") (term "1,0,1"))
(rule "eqSymm" (formula "7") (term "0,0,0,1"))
(rule "polySimp_elimSub" (formula "7") (term "0,0,0,0,1"))
(rule "polySimp_homoEq" (formula "7") (term "0,0,0,1"))
(rule "polySimp_mulComm0" (formula "7") (term "1,0,0,0,0,1"))
(rule "polySimp_addComm0" (formula "7") (term "1,1,0,0,0,0,1"))
(rule "polySimp_rightDist" (formula "7") (term "1,0,0,0,0,1"))
(rule "polySimp_mulAssoc" (formula "7") (term "0,1,0,0,0,0,1"))
(rule "polySimp_mulComm0" (formula "7") (term "0,0,1,0,0,0,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "0,1,0,0,0,0,1"))
(rule "polySimp_elimOne" (formula "7") (term "0,1,0,0,0,0,1"))
(rule "polySimp_addAssoc" (formula "7") (term "0,0,0,0,1"))
(rule "polySimp_sepNegMonomial" (formula "7") (term "0,0,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "0,0,0,0,1"))
(rule "polySimp_elimOne" (formula "7") (term "0,0,0,0,1"))
(rule "compound_subtraction_1" (formula "7") (term "1") (inst "#v=x_1"))
(rule "variableDeclarationAssign" (formula "7") (term "1"))
(rule "variableDeclaration" (formula "7") (term "1") (newnames "x_1"))
(rule "assignment_read_attribute" (formula "7"))
(branch "Normal Execution (self != null)"
(builtin "One Step Simplification" (formula "7"))
(rule "assignmentSubtractionInt" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "translateJavaSubInt" (formula "7") (term "0,1,0"))
(rule "polySimp_elimSub" (formula "7") (term "0,1,0"))
(rule "polySimp_addComm0" (formula "7") (term "0,1,0"))
(rule "emptyModality" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "polySimp_homoEq" (formula "7"))
(rule "polySimp_addComm1" (formula "7") (term "0,0"))
(rule "polySimp_pullOutFactor1b" (formula "7") (term "0"))
(rule "add_literals" (formula "7") (term "1,1,0"))
(rule "times_zero_1" (formula "7") (term "1,0"))
(rule "add_zero_right" (formula "7") (term "0"))
(rule "polySimp_pullOutFactor2" (formula "7") (term "0"))
(rule "add_literals" (formula "7") (term "1,0"))
(rule "times_zero_1" (formula "7") (term "0"))
(builtin "One Step Simplification" (formula "7"))
(rule "closeTrue" (formula "7"))
)
(branch "Null Reference (self = null)"
(rule "false_right" (formula "8"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "7")))
(rule "closeFalse" (formula "1"))
)
)

}
\javaSource "/Users/conni/Documents/Uni/hiwi/current_testFile/CorC/BankAccount";
\include "helper.key";
\programVariables {
int newBalance;
int x;
boolean ret;
int x_old;
boolean ret_old;
Account self;
Heap heapAtPre;
}\problem {((true) & self.OVERDRAFT_LIMIT = 0 & self.<created>=TRUE & Account::exactInstance(self)=TRUE & !self = null & self.<inv> & wellFormed(heap)) -> {heapAtPre := heap || x_old := x || ret_old := ret} \<{newBalance = self.balance - x;}\> ((newBalance = self.balance - x) & x = x_old & ret = ret_old)}
142 changes: 11 additions & 131 deletions ...nkAccount/Account/proveundoUpdate/BankAccountDailyLimitInterestTransaction/Statement1.key
View file
Original file line number Diff line number Diff line change
@@ -1,131 +1,11 @@
\profile "Java Profile";

\settings {
"#Proof-Settings-Config-File
#Tue Aug 23 16:25:20 CEST 2022
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
[SMTSettings]invariantForall=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
[Choice]DefaultChoices=initialisation-initialisation\\:disableStaticInitialisation , wdChecks-wdChecks\\:off , optimisedSelectRules-optimisedSelectRules\\:on , reach-reach\\:on , moreSeqRules-moreSeqRules\\:off , sequences-sequences\\:on , Strings-Strings\\:on , joinGenerateIsWeakeningGoal-joinGenerateIsWeakeningGoal\\:off , runtimeExceptions-runtimeExceptions\\:ban , wdOperator-wdOperator\\:L , JavaCard-JavaCard\\:off , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , modelFields-modelFields\\:showSatisfiability , assertions-assertions\\:on , intRules-intRules\\:arithmeticSemanticsIgnoringOF , bigint-bigint\\:on , programRules-programRules\\:Java
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_EXPAND
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
[SMTSettings]UseBuiltUniqueness=false
[SMTSettings]explicitTypeHierarchy=false
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS
[SMTSettings]SelectedTaclets=
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[Strategy]MaximumNumberOfAutomaticApplications=2147483647
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_NONCLOSE
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
[Strategy]Timeout=-1
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_RESTRICTED
[SMTSettings]useUninterpretedMultiplication=true
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
[SMTSettings]maxGenericSorts=2
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
[SMTSettings]integersMinimum=-2147483645
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
[SMTSettings]integersMaximum=2147483645
"
}

\javaSource "C:/Users/mko/Documents/ISF/0_feat-CorC2.0modifiable/runtime-EclipseApplication/BankAccount";\include "helper.key";\programVariables {int newBalance; int x; boolean ret; int x_old; boolean ret_old; Account self; Heap heapAtPre;}\problem {
true
& int::select(heap,
self,
Account::$OVERDRAFT_LIMIT)
= Z(0(#))
& boolean::select(heap,
self,
java.lang.Object::<created>)
= TRUE
& Account::exactInstance(self) = TRUE
& !self = null
& java.lang.Object::<inv>(heap, self)
& wellFormed(heap)
-> {heapAtPre:=heap || x_old:=x || ret_old:=ret}
\<{
newBalance=self.balance-x;
}\> ( newBalance
= sub(int::select(heap,
self,
Account::$balance),
x)
& x = x_old
& ret = ret_old)

}

\proof {
(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89"))

(autoModeTime "95")

(branch "dummy ID"
(builtin "One Step Simplification" (formula "1"))
(rule "impRight" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "notLeft" (formula "2"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "eqSymm" (formula "7") (term "1,0,0,1"))
(rule "eqSymm" (formula "7") (term "1,0,1"))
(rule "eqSymm" (formula "7") (term "0,0,0,1"))
(rule "polySimp_elimSub" (formula "7") (term "0,0,0,0,1"))
(rule "polySimp_homoEq" (formula "7") (term "0,0,0,1"))
(rule "polySimp_mulComm0" (formula "7") (term "1,0,0,0,0,1"))
(rule "polySimp_addComm0" (formula "7") (term "1,1,0,0,0,0,1"))
(rule "polySimp_rightDist" (formula "7") (term "1,0,0,0,0,1"))
(rule "polySimp_mulAssoc" (formula "7") (term "0,1,0,0,0,0,1"))
(rule "polySimp_mulComm0" (formula "7") (term "0,0,1,0,0,0,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "0,1,0,0,0,0,1"))
(rule "polySimp_elimOne" (formula "7") (term "0,1,0,0,0,0,1"))
(rule "polySimp_addAssoc" (formula "7") (term "0,0,0,0,1"))
(rule "polySimp_sepNegMonomial" (formula "7") (term "0,0,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "0,0,0,0,1"))
(rule "polySimp_elimOne" (formula "7") (term "0,0,0,0,1"))
(rule "compound_subtraction_1" (formula "7") (term "1") (inst "#v=x_1"))
(rule "variableDeclarationAssign" (formula "7") (term "1"))
(rule "variableDeclaration" (formula "7") (term "1") (newnames "x_1"))
(rule "assignment_read_attribute" (formula "7"))
(branch "Normal Execution (self != null)"
(builtin "One Step Simplification" (formula "7"))
(rule "assignmentSubtractionInt" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "translateJavaSubInt" (formula "7") (term "0,1,0"))
(rule "polySimp_elimSub" (formula "7") (term "0,1,0"))
(rule "polySimp_addComm0" (formula "7") (term "0,1,0"))
(rule "emptyModality" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "polySimp_homoEq" (formula "7"))
(rule "polySimp_addComm1" (formula "7") (term "0,0"))
(rule "polySimp_pullOutFactor1b" (formula "7") (term "0"))
(rule "add_literals" (formula "7") (term "1,1,0"))
(rule "times_zero_1" (formula "7") (term "1,0"))
(rule "add_zero_right" (formula "7") (term "0"))
(rule "polySimp_pullOutFactor2" (formula "7") (term "0"))
(rule "add_literals" (formula "7") (term "1,0"))
(rule "times_zero_1" (formula "7") (term "0"))
(builtin "One Step Simplification" (formula "7"))
(rule "closeTrue" (formula "7"))
)
(branch "Null Reference (self = null)"
(rule "false_right" (formula "8"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "7")))
(rule "closeFalse" (formula "1"))
)
)

}
\javaSource "/Users/conni/Documents/Uni/hiwi/current_testFile/CorC/BankAccount";
\include "helper.key";
\programVariables {
int newBalance;
int x;
boolean ret;
int x_old;
boolean ret_old;
Account self;
Heap heapAtPre;
}\problem {((true) & self.OVERDRAFT_LIMIT = 0 & self.<created>=TRUE & Account::exactInstance(self)=TRUE & !self = null & self.<inv> & wellFormed(heap)) -> {heapAtPre := heap || x_old := x || ret_old := ret} \<{newBalance = self.balance - x;}\> ((newBalance = self.balance - x) & x = x_old & ret = ret_old)}
Loading

0 comments on commit c386d39

Please sign in to comment.