diff --git a/.DS_Store b/.DS_Store index c60448a7a..e021de18c 100644 Binary files a/.DS_Store and b/.DS_Store differ diff --git a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccount/Statement1.key b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccount/Statement1.key index 1bf4069e8..f1ffd4320 100644 --- a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccount/Statement1.key +++ b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccount/Statement1.key @@ -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 @@ -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, @@ -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")) diff --git a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimit/Statement1.key b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimit/Statement1.key index 331942bdc..59fb05aeb 100644 --- a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimit/Statement1.key +++ b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimit/Statement1.key @@ -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 @@ -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, @@ -67,7 +77,7 @@ } \proof { -(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) +(keyLog "0" (keyUser "conni" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) (autoModeTime "100") diff --git a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitInterest/Statement1.key b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitInterest/Statement1.key index 56602e942..aa6be4082 100644 --- a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitInterest/Statement1.key +++ b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitInterest/Statement1.key @@ -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::) - = TRUE - & Account::exactInstance(self) = TRUE - & !self = null - & java.lang.Object::(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.=TRUE & Account::exactInstance(self)=TRUE & !self = null & self. & wellFormed(heap)) -> {heapAtPre := heap || x_old := x || ret_old := ret} \<{newBalance = self.balance - x;}\> ((newBalance = self.balance - x) & x = x_old & ret = ret_old)} \ No newline at end of file diff --git a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitInterestTransaction/Statement1.key b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitInterestTransaction/Statement1.key index 64696f371..aa6be4082 100644 --- a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitInterestTransaction/Statement1.key +++ b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitInterestTransaction/Statement1.key @@ -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::) - = TRUE - & Account::exactInstance(self) = TRUE - & !self = null - & java.lang.Object::(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.=TRUE & Account::exactInstance(self)=TRUE & !self = null & self. & wellFormed(heap)) -> {heapAtPre := heap || x_old := x || ret_old := ret} \<{newBalance = self.balance - x;}\> ((newBalance = self.balance - x) & x = x_old & ret = ret_old)} \ No newline at end of file diff --git a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitTransaction/Statement1.key b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitTransaction/Statement1.key index 44d0893f3..f8dfcb40b 100644 --- a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitTransaction/Statement1.key +++ b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountDailyLimitTransaction/Statement1.key @@ -2,7 +2,7 @@ \settings { "#Proof-Settings-Config-File -#Tue Aug 23 16:25:00 CEST 2022 +#Tue Oct 31 20:31:51 CET 2023 [StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON [SMTSettings]invariantForall=false [Strategy]ActiveStrategy=JavaCardDLStrategy @@ -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, @@ -67,9 +77,9 @@ } \proof { -(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) +(keyLog "0" (keyUser "conni" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) -(autoModeTime "108") +(autoModeTime "68") (branch "dummy ID" (builtin "One Step Simplification" (formula "1")) diff --git a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountInterest/Statement1.key b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountInterest/Statement1.key index 0290f8390..aa6be4082 100644 --- a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountInterest/Statement1.key +++ b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountInterest/Statement1.key @@ -1,131 +1,11 @@ -\profile "Java Profile"; - -\settings { -"#Proof-Settings-Config-File -#Tue Aug 23 16:25:05 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::) - = TRUE - & Account::exactInstance(self) = TRUE - & !self = null - & java.lang.Object::(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 "85") - -(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.=TRUE & Account::exactInstance(self)=TRUE & !self = null & self. & wellFormed(heap)) -> {heapAtPre := heap || x_old := x || ret_old := ret} \<{newBalance = self.balance - x;}\> ((newBalance = self.balance - x) & x = x_old & ret = ret_old)} \ No newline at end of file diff --git a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountInterestTransaction/Statement1.key b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountInterestTransaction/Statement1.key index da93c06e9..aa6be4082 100644 --- a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountInterestTransaction/Statement1.key +++ b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountInterestTransaction/Statement1.key @@ -1,131 +1,11 @@ -\profile "Java Profile"; - -\settings { -"#Proof-Settings-Config-File -#Tue Aug 23 16:25:10 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::) - = TRUE - & Account::exactInstance(self) = TRUE - & !self = null - & java.lang.Object::(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 "105") - -(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.=TRUE & Account::exactInstance(self)=TRUE & !self = null & self. & wellFormed(heap)) -> {heapAtPre := heap || x_old := x || ret_old := ret} \<{newBalance = self.balance - x;}\> ((newBalance = self.balance - x) & x = x_old & ret = ret_old)} \ No newline at end of file diff --git a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountTransaction/Statement1.key b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountTransaction/Statement1.key index 320a52d04..7ae513df3 100644 --- a/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountTransaction/Statement1.key +++ b/BankAccount/features/BankAccount/Account/proveundoUpdate/BankAccountTransaction/Statement1.key @@ -2,7 +2,7 @@ \settings { "#Proof-Settings-Config-File -#Tue Aug 23 16:24:49 CEST 2022 +#Tue Oct 31 20:31:49 CET 2023 [StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON [SMTSettings]invariantForall=false [Strategy]ActiveStrategy=JavaCardDLStrategy @@ -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, @@ -67,9 +77,9 @@ } \proof { -(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) +(keyLog "0" (keyUser "conni" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) -(autoModeTime "87") +(autoModeTime "71") (branch "dummy ID" (builtin "One Step Simplification" (formula "1")) diff --git a/BankAccount/src/.gitkeep b/BankAccount/src/.gitkeep deleted file mode 100644 index 46bb3546a..000000000 --- a/BankAccount/src/.gitkeep +++ /dev/null @@ -1,2 +0,0 @@ -/.gitkeep -/Account_helper.java diff --git a/BankAccount/src/Account_helper.java b/BankAccount/src/Account_helper.java deleted file mode 100644 index 80ed30a75..000000000 --- a/BankAccount/src/Account_helper.java +++ /dev/null @@ -1,20 +0,0 @@ -public class Account_helper { - - int interest; - int balance; - - //begin - final static int INTEREST_RATE = 2; - - /*@ - @ normal_behavior - @ requires true; - @ ensures (balance >= 0 ==> \result >= 0) && (balance <= 0 ==> \result <= 0); - @ assignable \nothing; - @*/ - public /*@helper pure@*/ int interestCalculate() { - int result; - result = balance * INTEREST_RATE / 36500; - return result; - } -} \ No newline at end of file diff --git a/BankAccount/src_gen/Account.java b/BankAccount/src_gen/Account.java index 3a7d858b3..273f78553 100644 --- a/BankAccount/src_gen/Account.java +++ b/BankAccount/src_gen/Account.java @@ -32,7 +32,10 @@ public boolean original_undoUpdate(int x) { /*@ @ normal_behavior @ requires true; - @ ensures (\result == false ==> (withdraw == \old(withdraw) && balance == \old(balance))) && (\result == true ==> (withdraw >= \old(withdraw)) && balance == \old(balance) - x); + @ ensures (\result == false ==> + (withdraw == \old(withdraw) && balance == \old(balance))) + && (\result == true ==> + (withdraw >= \old(withdraw)) && balance == \old(balance) - x); @ assignable withdraw; @*/ public boolean undoUpdate(int x) { @@ -83,11 +86,14 @@ public boolean original_update(int x) { } /*@ - @ public normal_behavior - @ requires true; - @ ensures (\result == false ==> (withdraw == \old(withdraw) && balance == \old(balance))) && (\result == true ==> (withdraw <= \old(withdraw)) && balance == \old(balance) + x) && balance >= OVERDRAFT_LIMIT; - @ assignable withdraw; - @*/ + @ normal_behavior + @ requires true; + @ ensures (\result == false ==> + (withdraw == \old(withdraw) && balance == \old(balance))) + && (\result == true ==> + (withdraw <= \old(withdraw)) && balance == \old(balance) + x); + @ assignable withdraw; + @*/ public boolean update(int x) { int newWithdraw; boolean ret; @@ -114,20 +120,4 @@ public boolean update(int x) { } } - -// Code from C:/Users/mko/Documents/ISF/0_feat-CorC2.0modifiable/runtime-EclipseApplication/BankAccount/src/Account_helper.java - final static int INTEREST_RATE = 2; - - /*@ - @ normal_behavior - @ requires true; - @ ensures (balance >= 0 ==> \result >= 0) && (balance <= 0 ==> \result <= 0); - @ assignable \nothing; - @*/ - public /*@helper pure@*/ int interestCalculate() { - int result; - result = balance * INTEREST_RATE / 36500; - return result; - } -// End of code from C:/Users/mko/Documents/ISF/0_feat-CorC2.0modifiable/runtime-EclipseApplication/BankAccount/src/Account_helper.java -} +} \ No newline at end of file diff --git a/BankAccount/src_gen/Transaction.java b/BankAccount/src_gen/Transaction.java index 0a46f8b79..8f5542c20 100644 --- a/BankAccount/src_gen/Transaction.java +++ b/BankAccount/src_gen/Transaction.java @@ -8,7 +8,10 @@ public class Transaction { /*@ @ normal_behavior @ requires source != destination; - @ ensures \result == true ==> (\old(destination.balance) + amount == destination.balance) && \result == true ==> (\old(source.balance) - amount == source.balance) && \result == false ==> (\old(destination.balance) == destination.balance) && \result == false ==> (\old(source.balance) == source.balance); + @ ensures \result == true ==> (\old(destination.balance) + amount == destination.balance) + && \result == true ==> (\old(source.balance) - amount == source.balance) + && \result == false ==> (\old(destination.balance) == destination.balance) + && \result == false ==> (\old(source.balance) == source.balance); @ assignable \nothing; @*/ public boolean transfer(int amount) { diff --git a/BankAccountOO/src/Account/provetransactionAccountLock/ReturnStatement1.key b/BankAccountOO/src/Account/provetransactionAccountLock/ReturnStatement1.key deleted file mode 100644 index 9dfc985fe..000000000 --- a/BankAccountOO/src/Account/provetransactionAccountLock/ReturnStatement1.key +++ /dev/null @@ -1,116 +0,0 @@ -\profile "Java Profile"; - -\settings { -"#Proof-Settings-Config-File -#Sun Sep 25 18:14:18 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_corc2.0/runtime-EclipseApplication/BankAccountOO";\include "helper.key";\programVariables {Account source; Account destination; boolean ret; Account source_old; Account destination_old; Account self; Heap heapAtPre;}\problem { - true - & Account::isLocked(heap, source) = TRUE - & !destination = source - & Account::exactInstance(source) = TRUE - & boolean::select(heap, - source, - java.lang.Object::) - = TRUE - & !source = null - & Account::exactInstance(destination) = TRUE - & boolean::select(heap, - destination, - java.lang.Object::) - = TRUE - & !destination = null - & boolean::select(heap, - self, - java.lang.Object::) - = TRUE - & Account::exactInstance(self) = TRUE - & !self = null - & java.lang.Object::(heap, self) - & wellFormed(heap) --> {heapAtPre:=heap - || source_old:=source - || destination_old:=destination} - \<{ - ret=false; - }\> ( ( ret = TRUE - -> Account::isLocked(heap, source) - = TRUE - & Account::isLocked(heap, - destination) - = TRUE) - & source = source_old - & destination = destination_old) - -} - -\proof { -(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) - -(autoModeTime "181") - -(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 "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "notLeft" (formula "2")) -(rule "eqSymm" (formula "14") (term "1,0,0,1")) -(rule "eqSymm" (formula "14") (term "1,0,1")) -(rule "eqSymm" (formula "10")) -(rule "assignment" (formula "14") (term "1")) -(builtin "One Step Simplification" (formula "14")) -(rule "emptyModality" (formula "14") (term "1")) -(builtin "One Step Simplification" (formula "14") (ifInst "" (formula "1"))) -(rule "closeTrue" (formula "14")) -) - -} diff --git a/BankAccountOO/src/Account/provetransactionAccountLock/ReturnStatement2.key b/BankAccountOO/src/Account/provetransactionAccountLock/ReturnStatement2.key index 81f21db29..dbeafe612 100644 --- a/BankAccountOO/src/Account/provetransactionAccountLock/ReturnStatement2.key +++ b/BankAccountOO/src/Account/provetransactionAccountLock/ReturnStatement2.key @@ -1,116 +1,10 @@ -\profile "Java Profile"; - -\settings { -"#Proof-Settings-Config-File -#Sun Sep 25 18:14:21 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_corc2.0/runtime-EclipseApplication/BankAccountOO";\include "helper.key";\programVariables {Account source; Account destination; boolean ret; Account source_old; Account destination_old; Account self; Heap heapAtPre;}\problem { - true - & Account::isLocked(heap, destination) = TRUE - & !destination = source - & Account::exactInstance(source) = TRUE - & boolean::select(heap, - source, - java.lang.Object::) - = TRUE - & !source = null - & Account::exactInstance(destination) = TRUE - & boolean::select(heap, - destination, - java.lang.Object::) - = TRUE - & !destination = null - & boolean::select(heap, - self, - java.lang.Object::) - = TRUE - & Account::exactInstance(self) = TRUE - & !self = null - & java.lang.Object::(heap, self) - & wellFormed(heap) --> {heapAtPre:=heap - || source_old:=source - || destination_old:=destination} - \<{ - ret=false; - }\> ( ( ret = TRUE - -> Account::isLocked(heap, source) - = TRUE - & Account::isLocked(heap, - destination) - = TRUE) - & source = source_old - & destination = destination_old) - -} - -\proof { -(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) - -(autoModeTime "66") - -(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 "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "notLeft" (formula "2")) -(rule "eqSymm" (formula "14") (term "1,0,0,1")) -(rule "eqSymm" (formula "14") (term "1,0,1")) -(rule "eqSymm" (formula "10")) -(rule "assignment" (formula "14") (term "1")) -(builtin "One Step Simplification" (formula "14")) -(rule "emptyModality" (formula "14") (term "1")) -(builtin "One Step Simplification" (formula "14") (ifInst "" (formula "1"))) -(rule "closeTrue" (formula "14")) -) - -} +\javaSource "/Users/conni/Documents/Uni/hiwi/current_testFile/CorC/BankAccountOO"; +\include "helper.key"; +\programVariables { +boolean result_transactionAccountLock; +Account source; +Account source_old; +Account destination_old; +Account self; +Heap heapAtPre; +}\problem {(((true) & (destination.isLocked() = TRUE)) & Account::exactInstance(source) = TRUE & source. = TRUE & source != null & Account::exactInstance(destination) = TRUE & destination. = TRUE & destination != null & destination != source & self.=TRUE & Account::exactInstance(self)=TRUE & !self = null & self. & wellFormed(heap)) -> {heapAtPre := heap || source_old := source || destination_old := destination} \<{result_transactionAccountLock = false;}\> ((ret = TRUE -> source.isLocked() = TRUE& destination.isLocked() = TRUE) & source = source_old & destination = destination_old)} \ No newline at end of file diff --git a/BankAccountOO/src/Account/provetransactionAccountLock/ReturnStatement3.key b/BankAccountOO/src/Account/provetransactionAccountLock/ReturnStatement3.key deleted file mode 100644 index 2647e3154..000000000 --- a/BankAccountOO/src/Account/provetransactionAccountLock/ReturnStatement3.key +++ /dev/null @@ -1,120 +0,0 @@ -\profile "Java Profile"; - -\settings { -"#Proof-Settings-Config-File -#Sun Sep 25 18:14:26 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_corc2.0/runtime-EclipseApplication/BankAccountOO";\include "helper.key";\programVariables {Account source; Account destination; boolean ret; Account source_old; Account destination_old; Account self; Heap heapAtPre;}\problem { - ret = TRUE - & Account::isLocked(heap, source) = TRUE - & Account::isLocked(heap, destination) = TRUE - & !destination = source - & Account::exactInstance(source) = TRUE - & boolean::select(heap, - source, - java.lang.Object::) - = TRUE - & !source = null - & Account::exactInstance(destination) = TRUE - & boolean::select(heap, - destination, - java.lang.Object::) - = TRUE - & !destination = null - & boolean::select(heap, - self, - java.lang.Object::) - = TRUE - & Account::exactInstance(self) = TRUE - & !self = null - & java.lang.Object::(heap, self) - & wellFormed(heap) --> {heapAtPre:=heap - || source_old:=source - || destination_old:=destination} - \<{ - ret=ret; - }\> ( ( ret = TRUE - -> Account::isLocked(heap, source) - = TRUE - & Account::isLocked(heap, - destination) - = TRUE) - & source = source_old - & destination = destination_old) - -} - -\proof { -(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) - -(autoModeTime "111") - -(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 "andLeft" (formula "1")) -(rule "notLeft" (formula "2")) -(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 "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) -(rule "andLeft" (formula "1")) -(rule "eqSymm" (formula "16") (term "1,0,1")) -(rule "eqSymm" (formula "16") (term "1,0,0,1")) -(rule "eqSymm" (formula "12")) -(rule "assignment" (formula "16") (term "1")) -(builtin "One Step Simplification" (formula "16")) -(rule "applyEq" (formula "16") (term "0,1,0") (ifseqformula "1")) -(rule "emptyModality" (formula "16") (term "1")) -(builtin "One Step Simplification" (formula "16") (ifInst "" (formula "2")) (ifInst "" (formula "3"))) -(rule "closeTrue" (formula "16")) -) - -} diff --git a/BankAccountOO/src/Account/provetransactionAccountLock/SelectionStatement1.key b/BankAccountOO/src/Account/provetransactionAccountLock/SelectionStatement1.key deleted file mode 100644 index ee9cae8e0..000000000 --- a/BankAccountOO/src/Account/provetransactionAccountLock/SelectionStatement1.key +++ /dev/null @@ -1,81 +0,0 @@ -\profile "Java Profile"; - -\settings { -"#Proof-Settings-Config-File -#Sun Sep 25 18:14: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_corc2.0/runtime-EclipseApplication/BankAccountOO";\include "helper.key";\programVariables {Account source; Account destination; boolean ret; Account self; Heap heapAtPre;}\problem { - true - & !destination = source - & Account::exactInstance(source) = TRUE - & boolean::select(heap, - source, - java.lang.Object::) - = TRUE - & !source = null - & Account::exactInstance(destination) = TRUE - & boolean::select(heap, - destination, - java.lang.Object::) - = TRUE - & !destination = null - & boolean::select(heap, - self, - java.lang.Object::) - = TRUE - & Account::exactInstance(self) = TRUE - & !self = null - & java.lang.Object::(heap, self) - & wellFormed(heap) --> {heapAtPre:=heap} - ( Account::isLocked(heap, source) = TRUE - | Account::isLocked(heap, source) = FALSE) - -} - -\proof { -(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) - -(autoModeTime "19") - -(branch "dummy ID" -(builtin "One Step Simplification" (formula "1")) -(rule "closeTrue" (formula "1")) -) - -} diff --git a/BankAccountOO/src/Account/provetransactionAccountLock/SelectionStatement2.key b/BankAccountOO/src/Account/provetransactionAccountLock/SelectionStatement2.key deleted file mode 100644 index 6a98f1e29..000000000 --- a/BankAccountOO/src/Account/provetransactionAccountLock/SelectionStatement2.key +++ /dev/null @@ -1,81 +0,0 @@ -\profile "Java Profile"; - -\settings { -"#Proof-Settings-Config-File -#Sun Sep 25 18:14:23 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_corc2.0/runtime-EclipseApplication/BankAccountOO";\include "helper.key";\programVariables {Account source; Account destination; boolean ret; Account self; Heap heapAtPre;}\problem { - true - & !destination = source - & Account::exactInstance(source) = TRUE - & boolean::select(heap, - source, - java.lang.Object::) - = TRUE - & !source = null - & Account::exactInstance(destination) = TRUE - & boolean::select(heap, - destination, - java.lang.Object::) - = TRUE - & !destination = null - & boolean::select(heap, - self, - java.lang.Object::) - = TRUE - & Account::exactInstance(self) = TRUE - & !self = null - & java.lang.Object::(heap, self) - & wellFormed(heap) --> {heapAtPre:=heap} - ( Account::isLocked(heap, destination) = TRUE - | Account::isLocked(heap, destination) = FALSE) - -} - -\proof { -(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) - -(autoModeTime "20") - -(branch "dummy ID" -(builtin "One Step Simplification" (formula "1")) -(rule "closeTrue" (formula "1")) -) - -} diff --git a/BankAccountOO/src/Account/provetransactionAccountLock/SkipStatement1.key b/BankAccountOO/src/Account/provetransactionAccountLock/SkipStatement1.key index add3fb42a..186853126 100644 --- a/BankAccountOO/src/Account/provetransactionAccountLock/SkipStatement1.key +++ b/BankAccountOO/src/Account/provetransactionAccountLock/SkipStatement1.key @@ -2,7 +2,7 @@ \settings { "#Proof-Settings-Config-File -#Sun Sep 25 18:14:19 CEST 2022 +#Tue Oct 31 20:32:16 CET 2023 [StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON [SMTSettings]invariantForall=false [Strategy]ActiveStrategy=JavaCardDLStrategy @@ -39,10 +39,20 @@ " } -\javaSource "C:/Users/mko/Documents/ISF/0_corc2.0/runtime-EclipseApplication/BankAccountOO";\include "helper.key";\programVariables {Account source; Account destination; boolean ret; Account source_old; Account destination_old; boolean ret_old; Account self; Heap heapAtPre;}\problem { +\javaSource "../../.."; +\include "helper.key"; +\programVariables { +Account source; +Account destination; +boolean ret; +Account source_old; +Account destination_old; +boolean ret_old; +Account self; +Heap heapAtPre; +}\problem { true & Account::isLocked(heap, source) = FALSE - & !destination = source & Account::exactInstance(source) = TRUE & boolean::select(heap, source, @@ -55,6 +65,7 @@ java.lang.Object::) = TRUE & !destination = null + & !destination = source & boolean::select(heap, self, java.lang.Object::) @@ -77,9 +88,9 @@ } \proof { -(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) +(keyLog "0" (keyUser "conni" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) -(autoModeTime "134") +(autoModeTime "33") (branch "dummy ID" (builtin "One Step Simplification" (formula "1")) @@ -87,24 +98,24 @@ (rule "andLeft" (formula "1")) (rule "andLeft" (formula "1")) (rule "andLeft" (formula "1")) +(rule "notLeft" (formula "2")) (rule "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) (rule "andLeft" (formula "1")) (rule "andLeft" (formula "1")) +(rule "notLeft" (formula "2")) (rule "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) +(rule "notLeft" (formula "2")) (rule "andLeft" (formula "1")) (rule "andLeft" (formula "1")) (rule "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) +(rule "notLeft" (formula "2")) (rule "andLeft" (formula "1")) (rule "andLeft" (formula "1")) (rule "notLeft" (formula "1")) -(rule "notLeft" (formula "1")) (rule "eqSymm" (formula "14") (term "0,0,0,1")) (rule "eqSymm" (formula "14") (term "1,0,0,1")) (rule "eqSymm" (formula "14") (term "1,0,1")) -(rule "eqSymm" (formula "9")) +(rule "eqSymm" (formula "12")) (rule "emptyStatement" (formula "14") (term "1")) (rule "emptyModality" (formula "14") (term "1")) (builtin "One Step Simplification" (formula "14")) diff --git a/BankAccountOO/src/Account/provetransactionAccountLock/SkipStatement2.key b/BankAccountOO/src/Account/provetransactionAccountLock/SkipStatement2.key deleted file mode 100644 index 1677736f7..000000000 --- a/BankAccountOO/src/Account/provetransactionAccountLock/SkipStatement2.key +++ /dev/null @@ -1,111 +0,0 @@ -\profile "Java Profile"; - -\settings { -"#Proof-Settings-Config-File -#Sun Sep 25 18:14:22 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_corc2.0/runtime-EclipseApplication/BankAccountOO";\include "helper.key";\programVariables {Account source; Account destination; boolean ret; Account source_old; Account destination_old; Account self; Heap heapAtPre;}\problem { - true - & Account::isLocked(heap, destination) = FALSE - & !destination = source - & Account::exactInstance(source) = TRUE - & boolean::select(heap, - source, - java.lang.Object::) - = TRUE - & !source = null - & Account::exactInstance(destination) = TRUE - & boolean::select(heap, - destination, - java.lang.Object::) - = TRUE - & !destination = null - & boolean::select(heap, - self, - java.lang.Object::) - = TRUE - & Account::exactInstance(self) = TRUE - & !self = null - & java.lang.Object::(heap, self) - & wellFormed(heap) --> {heapAtPre:=heap - || source_old:=source - || destination_old:=destination} - \<{ - ; - }\> ( true - & source = source_old - & destination = destination_old) - -} - -\proof { -(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) - -(autoModeTime "56") - -(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 "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "notLeft" (formula "1")) -(rule "notLeft" (formula "1")) -(rule "eqSymm" (formula "14") (term "0,0,1")) -(rule "eqSymm" (formula "14") (term "1,0,1")) -(rule "eqSymm" (formula "9")) -(rule "emptyStatement" (formula "14") (term "1")) -(rule "emptyModality" (formula "14") (term "1")) -(builtin "One Step Simplification" (formula "14")) -(rule "closeTrue" (formula "14")) -) - -} diff --git a/BankAccountOO/src/Account/provetransactionAccountLock/Statement1.key b/BankAccountOO/src/Account/provetransactionAccountLock/Statement1.key deleted file mode 100644 index 3603d89ad..000000000 --- a/BankAccountOO/src/Account/provetransactionAccountLock/Statement1.key +++ /dev/null @@ -1,410 +0,0 @@ -\profile "Java Profile"; - -\settings { -"#Proof-Settings-Config-File -#Sun Sep 25 18:14:25 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_corc2.0/runtime-EclipseApplication/BankAccountOO";\include "helper.key";\programVariables {Account source; Account destination; boolean ret; Account source_old; Account destination_old; Account self; Heap heapAtPre;}\problem { - true - & !destination = source - & Account::exactInstance(source) = TRUE - & boolean::select(heap, - source, - java.lang.Object::) - = TRUE - & !source = null - & Account::exactInstance(destination) = TRUE - & boolean::select(heap, - destination, - java.lang.Object::) - = TRUE - & !destination = null - & boolean::select(heap, - self, - java.lang.Object::) - = TRUE - & Account::exactInstance(self) = TRUE - & !self = null - & java.lang.Object::(heap, self) - & wellFormed(heap) --> {heapAtPre:=heap - || source_old:=source - || destination_old:=destination} - \<{ - source.lock(); - destination.lock(); - ret=true; - }\> ( ret = TRUE - & Account::isLocked(heap, source) = TRUE - & Account::isLocked(heap, destination) - = TRUE - & source = source_old - & destination = destination_old) - -} - -\proof { -(keyLog "0" (keyUser "mko" ) (keyVersion "19f0b8c2a4fe689cd76be6cd1753b36e2e825a89")) - -(autoModeTime "965") - -(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 "andLeft" (formula "1")) -(rule "notLeft" (formula "3")) -(rule "andLeft" (formula "1")) -(rule "andLeft" (formula "1")) -(rule "notLeft" (formula "2")) -(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 "notLeft" (formula "1")) -(rule "eqSymm" (formula "13") (term "1,0,0,1")) -(rule "eqSymm" (formula "13") (term "1,0,1")) -(rule "eqSymm" (formula "9")) -(builtin "Use Operation Contract" (formula "13") (newnames "heapBefore_lock,exc,heapAfter_lock,anon_heap_lock") (contract "Account[Account::lock()].JML normal_behavior operation contract.0")) -(branch "Post (lock)" - (builtin "One Step Simplification" (formula "15")) - (builtin "One Step Simplification" (formula "10")) - (rule "andLeft" (formula "10")) - (rule "andLeft" (formula "11")) - (rule "andLeft" (formula "12")) - (rule "pullOutSelect" (formula "12") (term "0") (inst "selectSK=Account_lock_0")) - (rule "simplifySelectOfAnonEQ" (formula "12") (ifseqformula "10")) - (builtin "One Step Simplification" (formula "12") (ifInst "" (formula "15")) (ifInst "" (formula "2"))) - (rule "elementOfSingleton" (formula "12") (term "0,0")) - (builtin "One Step Simplification" (formula "12")) - (rule "applyEqReverse" (formula "13") (term "0") (ifseqformula "12")) - (rule "hideAuxiliaryEq" (formula "12")) - (builtin "Use Operation Contract" (formula "17") (newnames "heapBefore_lock_0,exc_0,heapAfter_lock_0,anon_heap_lock_0") (contract "Account[Account::lock()].JML normal_behavior operation contract.0")) - (branch "Post (lock)" - (builtin "One Step Simplification" (formula "19")) - (builtin "One Step Simplification" (formula "14")) - (rule "andLeft" (formula "14")) - (rule "andLeft" (formula "15")) - (rule "andLeft" (formula "16")) - (rule "assignment" (formula "21") (term "1")) - (builtin "One Step Simplification" (formula "21")) - (rule "pullOutSelect" (formula "16") (term "0") (inst "selectSK=Account_lock_1")) - (rule "simplifySelectOfAnonEQ" (formula "16") (ifseqformula "14")) - (builtin "One Step Simplification" (formula "16") (ifInst "" (formula "20"))) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "16") (term "0,1,0,0") (ifseqformula "10")) - (rule "replace_known_left" (formula "16") (term "0,0,1,0,0") (ifseqformula "4")) - (builtin "One Step Simplification" (formula "16")) - (rule "elementOfSingleton" (formula "16") (term "0,0")) - (builtin "One Step Simplification" (formula "16")) - (rule "applyEqReverse" (formula "17") (term "0") (ifseqformula "16")) - (rule "hideAuxiliaryEq" (formula "16")) - (rule "emptyModality" (formula "21") (term "1")) - (builtin "One Step Simplification" (formula "21")) - (rule "commute_and" (formula "21")) - (rule "cut_direct" (formula "21") (term "1")) - (branch "CUT: source.isLocked()@heapAfter_lock_0 = TRUE TRUE" - (builtin "One Step Simplification" (formula "22")) - (builtin "Evaluate Query" (formula "1") (term "0") (newnames "callee,queryResult_0,res_isLocked_0")) - (rule "replaceKnownQuery_Account_isLocked(heapAfter_lock_0,source)_000_4" (formula "2") (term "0")) - (rule "notLeft" (formula "1")) - (rule "eqSymm" (formula "18") (term "0,0,1")) - (rule "variableDeclaration" (formula "18") (term "1") (newnames "queryResult_0")) - (rule "applyEqRigid" (formula "18") (term "0,0,0,1") (ifseqformula "1")) - (rule "eqSymm" (formula "18") (term "0,0,1")) - (builtin "Use Operation Contract" (formula "18") (newnames "heapBefore_isLocked_0,result_0,exc_2,heapAfter_isLocked_0,anon_heap_isLocked_0") (contract "Account[Account::isLocked()].JML normal_behavior operation contract.0")) - (branch "Post (isLocked)" - (builtin "One Step Simplification" (formula "19")) - (builtin "One Step Simplification" (formula "20")) - (rule "andLeft" (formula "19")) - (rule "andLeft" (formula "20")) - (rule "andLeft" (formula "21")) - (rule "eqSymm" (formula "21")) - (rule "assignment" (formula "22") (term "1")) - (builtin "One Step Simplification" (formula "22")) - (rule "pullOutSelect" (formula "21") (term "0") (inst "selectSK=Account_lock_4")) - (rule "simplifySelectOfAnonEQ" (formula "21") (ifseqformula "19")) - (builtin "One Step Simplification" (formula "21") (ifInst "" (formula "25"))) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "21") (term "0,0,0") (ifseqformula "15")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "21") (term "0,0,0,0") (ifseqformula "11")) - (rule "eqSymm" (formula "22")) - (rule "applyEqReverse" (formula "21") (term "1") (ifseqformula "22")) - (rule "hideAuxiliaryEq" (formula "22")) - (rule "replace_known_left" (formula "21") (term "0,0,0,0,0") (ifseqformula "3")) - (builtin "One Step Simplification" (formula "21")) - (rule "pullOutSelect" (formula "21") (term "0") (inst "selectSK=Account_lock_5")) - (rule "simplifySelectOfAnonEQ" (formula "21") (ifseqformula "15")) - (builtin "One Step Simplification" (formula "21") (ifInst "" (formula "25"))) - (rule "replaceKnownSelect_taclet0_0" (formula "21") (term "2,0")) - (rule "replaceKnownAuxiliaryConstant_taclet0_1" (formula "21") (term "2,0")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "21") (term "0,1,0,0") (ifseqformula "11")) - (rule "eqSymm" (formula "22")) - (rule "applyEqReverse" (formula "21") (term "1") (ifseqformula "22")) - (rule "hideAuxiliaryEq" (formula "22")) - (rule "replace_known_left" (formula "21") (term "0,0,1,0,0") (ifseqformula "3")) - (builtin "One Step Simplification" (formula "21")) - (rule "elementOfSingleton" (formula "21") (term "0,0")) - (builtin "One Step Simplification" (formula "21") (ifInst "" (formula "23"))) - (rule "applyEq" (formula "13") (term "0") (ifseqformula "21")) - (rule "applyEq" (formula "22") (term "0,1,0") (ifseqformula "13")) - (rule "applyEq" (formula "21") (term "1") (ifseqformula "13")) - (rule "methodCallEmpty" (formula "22") (term "1")) - (builtin "One Step Simplification" (formula "22")) - (rule "emptyModality" (formula "22") (term "1")) - (builtin "One Step Simplification" (formula "22")) - (rule "false_right" (formula "22")) - (builtin "Evaluate Query" (formula "26") (term "0") (newnames "callee,queryResult_1,res_isLocked_1")) - (rule "replaceKnownQuery_Account_isLocked(heapAfter_lock_0,destination)_0000_9" (formula "27") (term "0")) - (rule "notLeft" (formula "1")) - (rule "eqSymm" (formula "22") (term "0,0,1")) - (rule "variableDeclaration" (formula "22") (term "1") (newnames "queryResult_1")) - (rule "apply_eq_boolean_rigid" (formula "22") (term "0,0,0,1") (ifseqformula "27")) - (rule "eqSymm" (formula "22") (term "0,0,1")) - (builtin "One Step Simplification" (formula "22")) - (builtin "Use Operation Contract" (formula "22") (newnames "heapBefore_isLocked_1,result_1,exc_3,heapAfter_isLocked_1,anon_heap_isLocked_1") (contract "Account[Account::isLocked()].JML normal_behavior operation contract.0")) - (branch "Post (isLocked)" - (builtin "One Step Simplification" (formula "24")) - (builtin "One Step Simplification" (formula "23")) - (rule "andLeft" (formula "23")) - (rule "andLeft" (formula "24")) - (rule "andLeft" (formula "25")) - (rule "eqSymm" (formula "25")) - (rule "assignment" (formula "26") (term "1")) - (builtin "One Step Simplification" (formula "26")) - (rule "pullOutSelect" (formula "25") (term "0") (inst "selectSK=Account_lock_6")) - (rule "simplifySelectOfAnonEQ" (formula "25") (ifseqformula "23")) - (builtin "One Step Simplification" (formula "25") (ifInst "" (formula "30"))) - (rule "replaceKnownSelect_taclet00_2" (formula "25") (term "2,0")) - (rule "replaceKnownAuxiliaryConstant_taclet00_3" (formula "25") (term "2,0")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "25") (term "0,0,0") (ifseqformula "15")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "25") (term "0,0,0,0") (ifseqformula "11")) - (rule "eqSymm" (formula "26")) - (rule "applyEqReverse" (formula "25") (term "1") (ifseqformula "26")) - (rule "hideAuxiliaryEq" (formula "26")) - (rule "replace_known_left" (formula "25") (term "0,0,0,0,0") (ifseqformula "5")) - (builtin "One Step Simplification" (formula "25")) - (rule "applyEq" (formula "17") (term "0") (ifseqformula "25")) - (rule "applyEq" (formula "25") (term "1") (ifseqformula "17")) - (rule "applyEq" (formula "26") (term "0,1,0") (ifseqformula "17")) - (rule "methodCallEmpty" (formula "26") (term "1")) - (builtin "One Step Simplification" (formula "26")) - (rule "emptyModality" (formula "26") (term "1")) - (builtin "One Step Simplification" (formula "26")) - (rule "closeTrue" (formula "26")) - ) - (branch "Exceptional Post (isLocked)" - (builtin "One Step Simplification" (formula "24")) - (builtin "One Step Simplification" (formula "23")) - (rule "andLeft" (formula "23")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "24") (term "1,0") (ifseqformula "23")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "24") (term "0,1,0") (ifseqformula "15")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "24") (term "0,0,1,0") (ifseqformula "11")) - (rule "andLeft" (formula "24")) - (rule "andLeft" (formula "24")) - (rule "andLeft" (formula "26")) - (rule "notLeft" (formula "24")) - (rule "close" (formula "27") (ifseqformula "26")) - ) - (branch "Pre (isLocked)" - (builtin "One Step Simplification" (formula "22")) - (rule "wellFormedAnonEQ" (formula "22") (ifseqformula "15")) - (rule "wellFormedAnonEQ" (formula "22") (term "0") (ifseqformula "11")) - (rule "replace_known_left" (formula "22") (term "1") (ifseqformula "14")) - (builtin "One Step Simplification" (formula "22") (ifInst "" (formula "9")) (ifInst "" (formula "10"))) - (rule "closeTrue" (formula "22")) - ) - (branch "Null reference (callee = null)" - (builtin "One Step Simplification" (formula "22") (ifInst "" (formula "25"))) - (rule "closeTrue" (formula "22")) - ) - ) - (branch "Exceptional Post (isLocked)" - (builtin "One Step Simplification" (formula "19")) - (builtin "One Step Simplification" (formula "20")) - (rule "andLeft" (formula "19")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "20") (term "1,0") (ifseqformula "19")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "20") (term "0,1,0") (ifseqformula "15")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "20") (term "0,0,1,0") (ifseqformula "11")) - (rule "andLeft" (formula "20")) - (rule "andLeft" (formula "20")) - (rule "andLeft" (formula "22")) - (rule "notLeft" (formula "20")) - (rule "close" (formula "23") (ifseqformula "22")) - ) - (branch "Pre (isLocked)" - (builtin "One Step Simplification" (formula "18")) - (rule "wellFormedAnonEQ" (formula "18") (ifseqformula "15")) - (rule "wellFormedAnonEQ" (formula "18") (term "0") (ifseqformula "11")) - (rule "replace_known_left" (formula "18") (term "1") (ifseqformula "14")) - (builtin "One Step Simplification" (formula "18") (ifInst "" (formula "9")) (ifInst "" (formula "10"))) - (rule "closeTrue" (formula "18")) - ) - (branch "Null reference (callee = null)" - (builtin "One Step Simplification" (formula "18") (ifInst "" (formula "20"))) - (rule "closeTrue" (formula "18")) - ) - ) - (branch "CUT: source.isLocked()@heapAfter_lock_0 = TRUE FALSE" - (builtin "One Step Simplification" (formula "22")) - (rule "false_right" (formula "22")) - (builtin "Evaluate Query" (formula "21") (term "0") (newnames "callee,queryResult,res_isLocked")) - (rule "replaceKnownQuery_Account_isLocked(heapAfter_lock_0,source)_100_4" (formula "22") (term "0")) - (rule "notLeft" (formula "1")) - (rule "eqSymm" (formula "17") (term "0,0,1")) - (rule "variableDeclaration" (formula "17") (term "1") (newnames "queryResult")) - (rule "apply_eq_boolean_rigid" (formula "17") (term "0,0,0,1") (ifseqformula "22")) - (rule "eqSymm" (formula "17") (term "0,0,1")) - (builtin "One Step Simplification" (formula "17")) - (builtin "Use Operation Contract" (formula "17") (newnames "heapBefore_isLocked,result,exc_1,heapAfter_isLocked,anon_heap_isLocked") (contract "Account[Account::isLocked()].JML normal_behavior operation contract.0")) - (branch "Post (isLocked)" - (builtin "One Step Simplification" (formula "18")) - (builtin "One Step Simplification" (formula "19")) - (rule "andLeft" (formula "18")) - (rule "andLeft" (formula "19")) - (rule "andLeft" (formula "20")) - (rule "eqSymm" (formula "20")) - (rule "assignment" (formula "21") (term "1")) - (builtin "One Step Simplification" (formula "21")) - (rule "pullOutSelect" (formula "20") (term "0") (inst "selectSK=Account_lock_2")) - (rule "simplifySelectOfAnonEQ" (formula "20") (ifseqformula "18")) - (builtin "One Step Simplification" (formula "20") (ifInst "" (formula "24"))) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "20") (term "0,0,0") (ifseqformula "14")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "20") (term "0,0,0,0") (ifseqformula "10")) - (rule "eqSymm" (formula "21")) - (rule "applyEqReverse" (formula "20") (term "1") (ifseqformula "21")) - (rule "hideAuxiliaryEq" (formula "21")) - (rule "replace_known_left" (formula "20") (term "0,0,0,0,0") (ifseqformula "2")) - (builtin "One Step Simplification" (formula "20")) - (rule "pullOutSelect" (formula "20") (term "0") (inst "selectSK=Account_lock_3")) - (rule "simplifySelectOfAnonEQ" (formula "20") (ifseqformula "14")) - (builtin "One Step Simplification" (formula "20") (ifInst "" (formula "24"))) - (rule "replaceKnownSelect_taclet0_0" (formula "20") (term "2,0")) - (rule "replaceKnownAuxiliaryConstant_taclet0_1" (formula "20") (term "2,0")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "20") (term "0,1,0,0") (ifseqformula "10")) - (rule "eqSymm" (formula "21")) - (rule "applyEqReverse" (formula "20") (term "1") (ifseqformula "21")) - (rule "hideAuxiliaryEq" (formula "21")) - (rule "replace_known_left" (formula "20") (term "0,0,1,0,0") (ifseqformula "2")) - (builtin "One Step Simplification" (formula "20")) - (rule "elementOfSingleton" (formula "20") (term "0,0")) - (builtin "One Step Simplification" (formula "20") (ifInst "" (formula "22"))) - (rule "applyEq" (formula "20") (term "0") (ifseqformula "12")) - (rule "eqSymm" (formula "20")) - (rule "applyEq" (formula "21") (term "0,1,0") (ifseqformula "20")) - (rule "methodCallEmpty" (formula "21") (term "1")) - (builtin "One Step Simplification" (formula "21")) - (rule "emptyModality" (formula "21") (term "1")) - (builtin "One Step Simplification" (formula "21")) - (rule "closeTrue" (formula "21")) - ) - (branch "Exceptional Post (isLocked)" - (builtin "One Step Simplification" (formula "18")) - (builtin "One Step Simplification" (formula "19")) - (rule "andLeft" (formula "18")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "19") (term "1,0") (ifseqformula "18")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "19") (term "0,1,0") (ifseqformula "14")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "19") (term "0,0,1,0") (ifseqformula "10")) - (rule "andLeft" (formula "19")) - (rule "andLeft" (formula "19")) - (rule "andLeft" (formula "21")) - (rule "notLeft" (formula "19")) - (rule "close" (formula "22") (ifseqformula "21")) - ) - (branch "Pre (isLocked)" - (builtin "One Step Simplification" (formula "17")) - (rule "wellFormedAnonEQ" (formula "17") (ifseqformula "14")) - (rule "wellFormedAnonEQ" (formula "17") (term "0") (ifseqformula "10")) - (rule "replace_known_left" (formula "17") (term "1") (ifseqformula "13")) - (builtin "One Step Simplification" (formula "17") (ifInst "" (formula "8")) (ifInst "" (formula "9"))) - (rule "closeTrue" (formula "17")) - ) - (branch "Null reference (callee = null)" - (builtin "One Step Simplification" (formula "17") (ifInst "" (formula "19"))) - (rule "closeTrue" (formula "17")) - ) - ) - ) - (branch "Exceptional Post (lock)" - (builtin "One Step Simplification" (formula "14")) - (builtin "One Step Simplification" (formula "19")) - (rule "andLeft" (formula "14")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "15") (term "1,0") (ifseqformula "14")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "15") (term "0,1,0") (ifseqformula "10")) - (rule "andLeft" (formula "15")) - (rule "andLeft" (formula "16")) - (rule "andLeft" (formula "15")) - (rule "notLeft" (formula "15")) - (rule "close" (formula "18") (ifseqformula "17")) - ) - (branch "Pre (lock)" - (builtin "One Step Simplification" (formula "17")) - (rule "wellFormedAnonEQ" (formula "17") (ifseqformula "10")) - (rule "replace_known_left" (formula "17") (term "1") (ifseqformula "9")) - (builtin "One Step Simplification" (formula "17") (ifInst "" (formula "8"))) - (rule "closeTrue" (formula "17")) - ) - (branch "Null reference (destination = null)" - (builtin "One Step Simplification" (formula "17") (ifInst "" (formula "15"))) - (rule "closeTrue" (formula "17")) - ) -) -(branch "Exceptional Post (lock)" - (builtin "One Step Simplification" (formula "15")) - (builtin "One Step Simplification" (formula "10")) - (rule "andLeft" (formula "10")) - (rule "selectCreatedOfAnonAsFormulaEQ" (formula "11") (term "1,0") (ifseqformula "10")) - (rule "andLeft" (formula "11")) - (rule "andLeft" (formula "12")) - (rule "andLeft" (formula "11")) - (rule "notLeft" (formula "11")) - (rule "close" (formula "14") (ifseqformula "13")) -) -(branch "Pre (lock)" - (builtin "One Step Simplification" (formula "13") (ifInst "" (formula "8"))) - (rule "closeTrue" (formula "13")) -) -(branch "Null reference (source = null)" - (builtin "One Step Simplification" (formula "13") (ifInst "" (formula "10"))) - (rule "closeTrue" (formula "13")) -) -) - -} diff --git a/de.tu-bs.cs.isf.cbc.model/.DS_Store b/de.tu-bs.cs.isf.cbc.model/.DS_Store index 4e8df724f..d992d3d1b 100644 Binary files a/de.tu-bs.cs.isf.cbc.model/.DS_Store and b/de.tu-bs.cs.isf.cbc.model/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.model/src-gen/.DS_Store b/de.tu-bs.cs.isf.cbc.model/src-gen/.DS_Store new file mode 100644 index 000000000..9981f4102 Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.model/src-gen/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.model/src-gen/de/.DS_Store b/de.tu-bs.cs.isf.cbc.model/src-gen/de/.DS_Store new file mode 100644 index 000000000..4ebc6a84b Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.model/src-gen/de/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/.DS_Store b/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/.DS_Store new file mode 100644 index 000000000..64347c27f Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/cs/.DS_Store b/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/cs/.DS_Store new file mode 100644 index 000000000..190cb510e Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/cs/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/cs/isf/.DS_Store b/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/cs/isf/.DS_Store new file mode 100644 index 000000000..fcb3aea29 Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/cs/isf/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/cs/isf/cbc/.DS_Store b/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/cs/isf/cbc/.DS_Store new file mode 100644 index 000000000..bc4f9b73d Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/cs/isf/cbc/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/cs/isf/cbc/cbcclass/.DS_Store b/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/cs/isf/cbc/cbcclass/.DS_Store new file mode 100644 index 000000000..f463945fd Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.model/src-gen/de/tu_bs/cs/isf/cbc/cbcclass/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.util/.DS_Store b/de.tu-bs.cs.isf.cbc.util/.DS_Store index 48b7969c1..18bcb1c73 100644 Binary files a/de.tu-bs.cs.isf.cbc.util/.DS_Store and b/de.tu-bs.cs.isf.cbc.util/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.util/.classpath b/de.tu-bs.cs.isf.cbc.util/.classpath index 67a024ac2..d4df12c32 100644 --- a/de.tu-bs.cs.isf.cbc.util/.classpath +++ b/de.tu-bs.cs.isf.cbc.util/.classpath @@ -1,14 +1,19 @@ - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + diff --git a/de.tu-bs.cs.isf.cbc.util/META-INF/MANIFEST.MF b/de.tu-bs.cs.isf.cbc.util/META-INF/MANIFEST.MF index 85ab5cd74..8c6ebaf69 100644 --- a/de.tu-bs.cs.isf.cbc.util/META-INF/MANIFEST.MF +++ b/de.tu-bs.cs.isf.cbc.util/META-INF/MANIFEST.MF @@ -16,7 +16,11 @@ Require-Bundle: de.tu-bs.cs.isf.cbc.model;bundle-version="0.1.0", org.emftext.language.java, org.key_project.ui, de.tu_bs.cs.isf.cbc.statistics, - com.google.guava + com.google.guava, + org.mockito.mockito-core;bundle-version="4.8.1";resolution:=optional, + org.junit;bundle-version="4.13.2", + org.junit.jupiter.api;bundle-version="5.9.1";resolution:=optional, + org.junit.platform.commons;bundle-version="1.9.1";resolution:=optional Export-Package: de.tu_bs.cs.isf.cbc.util Import-Package: com.google.common.collect;version="10.0.1", org.emftext.language.java.resource.java.util diff --git a/de.tu-bs.cs.isf.cbc.util/lib/.DS_Store b/de.tu-bs.cs.isf.cbc.util/lib/.DS_Store new file mode 100644 index 000000000..5008ddfcf Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.util/lib/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.util/lib/junit-4.13.2.jar b/de.tu-bs.cs.isf.cbc.util/lib/junit-4.13.2.jar new file mode 100644 index 000000000..6da55d8b8 Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.util/lib/junit-4.13.2.jar differ diff --git a/de.tu-bs.cs.isf.cbc.util/lib/junit-jupiter-api-5.9.1.jar b/de.tu-bs.cs.isf.cbc.util/lib/junit-jupiter-api-5.9.1.jar new file mode 100644 index 000000000..b35d1b799 Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.util/lib/junit-jupiter-api-5.9.1.jar differ diff --git a/de.tu-bs.cs.isf.cbc.util/lib/junit-platform-commons-1.9.1.jar b/de.tu-bs.cs.isf.cbc.util/lib/junit-platform-commons-1.9.1.jar new file mode 100644 index 000000000..76ebc3966 Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.util/lib/junit-platform-commons-1.9.1.jar differ diff --git a/de.tu-bs.cs.isf.cbc.util/lib/mockito-core-4.8.1.jar b/de.tu-bs.cs.isf.cbc.util/lib/mockito-core-4.8.1.jar new file mode 100644 index 000000000..c66162bb8 Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.util/lib/mockito-core-4.8.1.jar differ diff --git a/de.tu-bs.cs.isf.cbc.util/lib/mockito-inline-4.8.1.jar b/de.tu-bs.cs.isf.cbc.util/lib/mockito-inline-4.8.1.jar new file mode 100644 index 000000000..33dd71b50 Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.util/lib/mockito-inline-4.8.1.jar differ diff --git a/de.tu-bs.cs.isf.cbc.util/lib/mockito-inline.jar b/de.tu-bs.cs.isf.cbc.util/lib/mockito-inline.jar new file mode 100644 index 000000000..33dd71b50 Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.util/lib/mockito-inline.jar differ diff --git a/de.tu-bs.cs.isf.cbc.util/pom.xml b/de.tu-bs.cs.isf.cbc.util/pom.xml index f1b24d15f..fdba7acf8 100644 --- a/de.tu-bs.cs.isf.cbc.util/pom.xml +++ b/de.tu-bs.cs.isf.cbc.util/pom.xml @@ -10,5 +10,68 @@ de.tu-bs.cbc de.tu-bs.cs.isf.cbc.util 1.0.0-SNAPSHOT - eclipse-plugin + eclipse-test-plugin + + + + + org.eclipse.tycho + tycho-surefire-plugin + ${tycho-version} + + + + p2-installable-unit + org.eclipse.equinox.ds + + + + + + + org.apache.maven.plugins + maven-dependency-plugin + + + copy-libraries + validate + + copy + + + + + + + org.mockito + mockito-inline + 4.8.1 + + + org.mockito + mockito-core + 4.8.1 + + + junit + junit + 4.13.2 + + + org.junit.jupiter + junit-jupiter-api + 5.9.1 + + + org.junit.platform + junit-platform-commons + 1.9.1 + + + false + ${basedir}/lib + + + + diff --git a/de.tu-bs.cs.isf.cbc.util/src/.DS_Store b/de.tu-bs.cs.isf.cbc.util/src/.DS_Store index 6c7e12ac0..6be6a5c65 100644 Binary files a/de.tu-bs.cs.isf.cbc.util/src/.DS_Store and b/de.tu-bs.cs.isf.cbc.util/src/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/KeYFileContent.java b/de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/KeYFileContent.java index 97ec10755..0e6ea839c 100644 --- a/de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/KeYFileContent.java +++ b/de.tu-bs.cs.isf.cbc.util/src/de/tu_bs/cs/isf/cbc/util/KeYFileContent.java @@ -129,6 +129,18 @@ public JavaVariable readVariables(JavaVariables vars) { } programVariables.getVariables().add(variable); } + /* + int originalSize = vars.getParams().size(); + for (int i = 0; i < originalSize; i++) { + Parameter param = vars.getParams().get(0); + if (param.getName().equals("ret")) { + returnVariable = CbcmodelFactory.eINSTANCE.createJavaVariable(); + returnVariable.setKind(VariableKind.RETURNPARAM); + returnVariable.setName(param.getType() + " " + param.getName()); + } + programVariables.getParams().add(param); + } + */ for (Parameter param : vars.getParams()) { if (param.getName().equals("ret")) { returnVariable = CbcmodelFactory.eINSTANCE.createJavaVariable(); diff --git a/de.tu-bs.cs.isf.cbc.util/src/test/.DS_Store b/de.tu-bs.cs.isf.cbc.util/src/test/.DS_Store new file mode 100644 index 000000000..6f4218e2d Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.util/src/test/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.util/src/test/java/KeYFileContentTest.java b/de.tu-bs.cs.isf.cbc.util/src/test/java/KeYFileContentTest.java new file mode 100644 index 000000000..ff41087ea --- /dev/null +++ b/de.tu-bs.cs.isf.cbc.util/src/test/java/KeYFileContentTest.java @@ -0,0 +1,715 @@ +package test.java; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.mock; +import static org.mockito.Mockito.mockStatic; +import static org.mockito.Mockito.when; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; + +import org.eclipse.core.resources.IProject; +import org.eclipse.emf.common.util.BasicEList; +import org.eclipse.emf.common.util.EList; +import org.eclipse.emf.ecore.EObject; +import org.eclipse.emf.ecore.resource.Resource; +import org.eclipse.emf.ecore.resource.impl.ResourceFactoryImpl; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import org.mockito.MockedStatic; + +import de.tu_bs.cs.isf.cbc.cbcclass.CbcclassFactory; +import de.tu_bs.cs.isf.cbc.cbcclass.Field; +import de.tu_bs.cs.isf.cbc.cbcclass.ModelClass; +import de.tu_bs.cs.isf.cbc.cbcclass.Parameter; +import de.tu_bs.cs.isf.cbc.cbcclass.Visibility; +import de.tu_bs.cs.isf.cbc.cbcclass.impl.ModelClassImpl; +import de.tu_bs.cs.isf.cbc.cbcmodel.CbCFormula; +import de.tu_bs.cs.isf.cbc.cbcmodel.CbcmodelFactory; +import de.tu_bs.cs.isf.cbc.cbcmodel.CbcmodelPackage; +import de.tu_bs.cs.isf.cbc.cbcmodel.Condition; +import de.tu_bs.cs.isf.cbc.cbcmodel.GlobalConditions; +import de.tu_bs.cs.isf.cbc.cbcmodel.JavaVariable; +import de.tu_bs.cs.isf.cbc.cbcmodel.JavaVariables; +import de.tu_bs.cs.isf.cbc.cbcmodel.VariableKind; +import de.tu_bs.cs.isf.cbc.util.Console; +import de.tu_bs.cs.isf.cbc.util.FileUtil; +import de.tu_bs.cs.isf.cbc.util.KeYFileContent; + +class KeYFileContentTest { + KeYFileContent content; + + Collection createMockResources() { + Collection resources = new ArrayList<>(); + Resource resource = mock(Resource.class); + resources.add(resource); + + Field field = CbcclassFactory.eINSTANCE.createField(); + field.setName("foo"); + field.setType("int"); + + EList classes = new BasicEList<>(); + ModelClass class_ = CbcclassFactory.eINSTANCE.createModelClass(); + class_.setName("TestClass"); + class_.getFields().add(field); + + classes.add(class_); + + when(resource.getContents()).thenReturn(classes); + + return resources; + } + + @BeforeEach + void before() { + IProject mockedProject = mock(IProject.class); + Collection resources = createMockResources(); + + try (MockedStatic mocked = mockStatic(FileUtil.class)) { + mocked.when(() -> FileUtil.getProjectFromProjectPath("location/")).thenReturn(mockedProject); + mocked.when(() -> FileUtil.getCbCClasses(mockedProject)).thenReturn(resources); + + content = new KeYFileContent("location/"); + content.setSrcFolder("src"); + } + } + + @Test + void testEmptyKeyFile() { + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " (wellFormed(heap)) -> {" + + " heapAtPre := heap" + + " } " + + " \\<{}\\> ()" + + "}", + content.getKeYStatementContent()); + } + + @Test + void testAddNullVariables() { + assertNull(content.readVariables(null)); + } + + @Test + void testAddVariables() { + EList list = new BasicEList<>(); + JavaVariable var; + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("int foo"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("static int bar"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("non-null int foobar"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("static non-null int baz"); + list.add(var); + + + JavaVariables variables = CbcmodelFactory.eINSTANCE.createJavaVariables(); + variables.eSet(CbcmodelPackage.eINSTANCE.getJavaVariables_Variables(), list); + + + content.readVariables(variables); + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " int foo;" + + " int bar;" + + " int foobar;" + + " int baz;" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " (wellFormed(heap)) -> {" + + " heapAtPre := heap" + + " } \\<{}\\> ()" + + "}", + content.getKeYStatementContent()); + } + + @Test + void testAddVariablesArray() { + EList list = new BasicEList<>(); + JavaVariable var; + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("int[] foo"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("static int[] bar"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("non-null int[] foobar"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("static non-null int[] baz"); + list.add(var); + + JavaVariables variables = CbcmodelFactory.eINSTANCE.createJavaVariables(); + variables.eSet(CbcmodelPackage.eINSTANCE.getJavaVariables_Variables(), list); + + + content.readVariables(variables); + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " int[] foo;" + + " int[] bar;" + + " int[] foobar;" + + " int[] baz;" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " (" + + " foo.=TRUE" + + " & bar.=TRUE" + + " & foobar.=TRUE" + + " & baz.=TRUE " + + " & wellFormed(heap)" + + " ) -> {" + + " heapAtPre := heap" + + " } \\<{}\\> ()" + + "}", + content.getKeYStatementContent()); + } + + @Test + void testAddVariablesParam() { + EList list = new BasicEList<>(); + JavaVariable var; + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("Object foo"); + var.setKind(VariableKind.PARAM); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("static Object bar"); + var.setKind(VariableKind.PARAM); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("non-null Object foobar"); + var.setKind(VariableKind.PARAM); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("static non-null Object baz"); + var.setKind(VariableKind.PARAM); + list.add(var); + + JavaVariables variables = CbcmodelFactory.eINSTANCE.createJavaVariables(); + variables.eSet(CbcmodelPackage.eINSTANCE.getJavaVariables_Variables(), list); + + + content.readVariables(variables); + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " Object foo;" + + " Object bar;" + + " Object foobar;" + + " Object baz;" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " (" + + " Object::exactInstance(foobar)=TRUE" + + " & foobar.=TRUE" + + " & foobar!=null" + + " & Object::exactInstance(baz)=TRUE" + + " & baz.=TRUE" + + " & baz!=null" + + " & wellFormed(heap)" + + " ) -> {" + + " heapAtPre := heap" + + " } \\<{}\\> ()" + + "}", + content.getKeYStatementContent()); + } + + @Test + void testAddVariablesReturn() { + EList list = new BasicEList<>(); + JavaVariable var; + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("int foo"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("static int bar"); + list.add(var); + + JavaVariable returnVar = CbcmodelFactory.eINSTANCE.createJavaVariable(); + returnVar.setName("int here"); + returnVar.setKind(VariableKind.RETURN); + list.add(returnVar); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("non-null int foobar"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("static non-null int baz"); + list.add(var); + + JavaVariables variables = CbcmodelFactory.eINSTANCE.createJavaVariables(); + variables.eSet(CbcmodelPackage.eINSTANCE.getJavaVariables_Variables(), list); + + + //assertEquals(returnVar, content.readVariables(variables)); + content.readVariables(variables); + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " int foo;" + + " int bar;" + + " int here;" + + " int foobar;" + + " int baz;" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " (wellFormed(heap)) -> {" + + " heapAtPre := heap" + + " } \\<{}\\> ()" + + "}", + content.getKeYStatementContent()); + } + + @Test + void testAddFields() { + EList list = new BasicEList<>(); + Field field; + + + field = CbcclassFactory.eINSTANCE.createField(); + field.setName("foo"); + field.setType("int"); + field.setVisibility(Visibility.PUBLIC); + //field.setIsStatic(false); + list.add(field); + + field = CbcclassFactory.eINSTANCE.createField(); + field.setName("bar"); + field.setType("Object"); + field.setVisibility(Visibility.PUBLIC); + //field.setIsStatic(false); + list.add(field); + + + JavaVariables variables = CbcmodelFactory.eINSTANCE.createJavaVariables(); + variables.eSet(CbcmodelPackage.eINSTANCE.getJavaVariables_Fields(), list); + + + content.readVariables(variables); + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " (" + + " Object::exactInstance(self.bar)=TRUE" + + " & self.bar.=TRUE" + + " & self.bar!=null" + + " & wellFormed(heap)" + + " ) -> {" + + " heapAtPre := heap" + + " } \\<{}\\> ()" + + "}", + content.getKeYStatementContent()); + } + + /* + @Test + void testAddParams() { + EList list = new BasicEList<>(); + Parameter param; + + param = CbcclassFactory.eINSTANCE.createParameter(); + param.setName("foo"); + param.setType("int"); + list.add(param); + + param = CbcclassFactory.eINSTANCE.createParameter(); + param.setName("bar"); + param.setType("Object"); + list.add(param); + + JavaVariables variables = CbcmodelFactory.eINSTANCE.createJavaVariables(); + variables.eSet(CbcmodelPackage.eINSTANCE.getJavaVariables_Params(), list); + + content.readVariables(variables); + + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " int foo;" + + " Object bar;" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " (" + + " wellFormed(heap)" + + " ) -> {" + + " heapAtPre := heap" + + " } \\<{}\\> ()" + + "}", + content.getKeYStatementContent()); + } + + @Test + void testAddParamsArray() { + EList list = new BasicEList<>(); + Parameter param; + + + param = CbcclassFactory.eINSTANCE.createParameter(); + param.setName("foo"); + param.setType("int[]"); + list.add(param); + + param = CbcclassFactory.eINSTANCE.createParameter(); + param.setName("bar"); + param.setType("Object[]"); + list.add(param); + + + JavaVariables variables = CbcmodelFactory.eINSTANCE.createJavaVariables(); + variables.eSet(CbcmodelPackage.eINSTANCE.getJavaVariables_Params(), list); + + + content.readVariables(variables); + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " int[] foo;" + + " Object[] bar;" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " (" + + " foo. = TRUE" + + " & bar. = TRUE" + + " & wellFormed(heap)" + + " ) -> {" + + " heapAtPre := heap" + + " } \\<{}\\> ()" + + "}", + content.getKeYStatementContent()); + } + + @Test + void testAddParamsNonNull() { + EList list = new BasicEList<>(); + Parameter param; + + + param = CbcclassFactory.eINSTANCE.createParameter(); + param.setName("foo"); + param.setType("non-null int"); + list.add(param); + + param = CbcclassFactory.eINSTANCE.createParameter(); + param.setName("bar"); + param.setType("non-null Object"); + list.add(param); + + + JavaVariables variables = CbcmodelFactory.eINSTANCE.createJavaVariables(); + variables.eSet(CbcmodelPackage.eINSTANCE.getJavaVariables_Params(), list); + + + content.readVariables(variables); + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " int foo;" + + " Object bar;" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " (" + + " Object::exactInstance(bar)=TRUE" + + " & bar.=TRUE" + + " & bar!=null" + + " & wellFormed(heap)" + + " ) -> {" + + " heapAtPre := heap" + + " } \\<{}\\> ()" + + "}", + content.getKeYStatementContent()); + } + + @Test + void testAddParamReturn() { + EList list = new BasicEList<>(); + Parameter var; + + var = CbcclassFactory.eINSTANCE.createParameter(); + var.setName("foo"); + var.setType("int"); + list.add(var); + + var = CbcclassFactory.eINSTANCE.createParameter(); + var.setName("bar"); + var.setType("int"); + list.add(var); + + Parameter returnParam = CbcclassFactory.eINSTANCE.createParameter(); + returnParam.setName("ret"); + returnParam.setType("int"); + list.add(returnParam); + + var = CbcclassFactory.eINSTANCE.createParameter(); + var.setName("foobar"); + var.setType("int"); + list.add(var); + + var = CbcclassFactory.eINSTANCE.createParameter(); + var.setName("baz"); + var.setType("int"); + list.add(var); + + + + JavaVariables variables = CbcmodelFactory.eINSTANCE.createJavaVariables(); + variables.eSet(CbcmodelPackage.eINSTANCE.getJavaVariables_Params(), list); + + JavaVariable returnVar = content.readVariables(variables); + + assertEquals(returnVar.getName(), returnParam.getType() + " " + returnParam.getName()); + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " int foo;" + + " int bar;" + + " int ret;" + + " int foobar;" + + " int baz;" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " ( wellFormed(heap)) -> {" + + " heapAtPre := heap" + + " } \\<{}\\> ()" + + "}", + content.getKeYStatementContent()); + } + */ + + @Test + void testAddGlobalConditions() { + EList list = new BasicEList<>(); + Condition cond; + + cond = CbcmodelFactory.eINSTANCE.createCondition(); + cond.setName("cond1"); + list.add(cond); + + cond = CbcmodelFactory.eINSTANCE.createCondition(); + cond.setName("cond2"); + list.add(cond); + + cond = CbcmodelFactory.eINSTANCE.createCondition(); + cond.setName("cond3"); + list.add(cond); + + + GlobalConditions conditions = CbcmodelFactory.eINSTANCE.createGlobalConditions(); + conditions.eSet(CbcmodelPackage.eINSTANCE.getGlobalConditions_Conditions(), list); + + content.readGlobalConditions(conditions); + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " (" + + " cond1" + + " & cond2" + + " & cond3" + + " & wellFormed(heap)" + + " ) -> {" + + " heapAtPre := heap" + + " } \\<{}\\> ()" + + "}", + content.getKeYStatementContent()); + } + + @Test + void testAddUnmofiableVars() { + EList list = new BasicEList<>(); + JavaVariable var; + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("int foo"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("static int bar"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("non-null int foobar"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("static non-null int baz"); + list.add(var); + + + JavaVariables variables = CbcmodelFactory.eINSTANCE.createJavaVariables(); + variables.eSet(CbcmodelPackage.eINSTANCE.getJavaVariables_Variables(), list); + + + content.readVariables(variables); + content.addUnmodifiableVars(list.stream().map(JavaVariable::getName).toList()); + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " int foo;" + + " int bar;" + + " int foobar;" + + " int baz;" + + " int foo_old;" + + " int bar_old;" + + " int foobar_old;" + + " int baz_old;" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " (wellFormed(heap)) -> {" + + " heapAtPre := heap" + + " || foo_old := foo" + + " || bar_old := bar" + + " || foobar_old := foobar" + + " || baz_old := baz" + + " } \\<{}\\> (" + + " foo = foo_old" + + " & bar = bar_old" + + " & foobar = foobar_old" + + " & baz = baz_old" + + " )" + + "}", + content.getKeYStatementContent()); + } + + @Test + void testOld() { + EList list = new BasicEList<>(); + JavaVariable var; + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("int foo"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("static int bar"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("non-null int foobar"); + list.add(var); + + var = CbcmodelFactory.eINSTANCE.createJavaVariable(); + var.setName("static non-null int baz"); + list.add(var); + + JavaVariables variables = CbcmodelFactory.eINSTANCE.createJavaVariables(); + variables.eSet(CbcmodelPackage.eINSTANCE.getJavaVariables_Variables(), list); + + content.readVariables(variables); + + EList condList = new BasicEList<>(); + Condition cond; + + cond = CbcmodelFactory.eINSTANCE.createCondition(); + cond.setName("cond2"); + condList.add(cond); + + cond = CbcmodelFactory.eINSTANCE.createCondition(); + cond.setName("cond3"); + condList.add(cond); + + + GlobalConditions conditions = CbcmodelFactory.eINSTANCE.createGlobalConditions(); + conditions.eSet(CbcmodelPackage.eINSTANCE.getGlobalConditions_Conditions(), condList); + + CbCFormula formula = mock(CbCFormula.class); + when(formula.getClassName()).thenReturn("TestClass"); + content.addSelf(formula); + + cond = CbcmodelFactory.eINSTANCE.createCondition(); + cond.setName("\\old(foo) == foo - 1"); + + content.addPostCondition(cond); + + content.readGlobalConditions(conditions); + + try (MockedStatic mocked = mockStatic(Console.class)) { + assertEqualsNormalized( + "\\javaSource \"location/src\";" + + "\\include \"helper.key\";" + + "\\programVariables {" + + " int foo;" + + " int bar;" + + " int foobar;" + + " int baz;" + + " int foo1_oldVal;" + + " TestClass self;" + + " Heap heapAtPre;" + + "}" + + "\\problem {" + + " (" + + " cond2" + + " &cond3" + + " &self.=TRUE&TestClass::exactInstance(self)=TRUE&!self=null&self.&wellFormed(heap)" + + " ) -> {" + + " heapAtPre := heap||foo1_oldVal := foo}" + + " \\<{}\\>(foo1_oldVal == foo - 1)" + + "}", + content.getKeYStatementContent()); + } + } + + static void assertEqualsNormalized(String expected, String actual) { + //KeYFileContent is really inconsistent with its spacing, so we normalize it. + String expectedNormalized = expected.replaceAll("( |\n)+", " ").replaceAll("([^\\w]) ", "$1").replaceAll(" ([^\\w])", "$1"); + String actualNormalized = actual.replaceAll("( |\n)+", " ").replaceAll("([^\\w]) ", "$1").replaceAll(" ([^\\w])", "$1"); + + assertEquals(expectedNormalized, actualNormalized); + } + +} \ No newline at end of file diff --git a/de.tu-bs.cs.isf.cbc.util/src/test/resources/.DS_Store b/de.tu-bs.cs.isf.cbc.util/src/test/resources/.DS_Store new file mode 100644 index 000000000..44967587b Binary files /dev/null and b/de.tu-bs.cs.isf.cbc.util/src/test/resources/.DS_Store differ diff --git a/de.tu-bs.cs.isf.cbc.util/src/test/resources/mockito-extensions/org.mockito.plugins.MockMaker b/de.tu-bs.cs.isf.cbc.util/src/test/resources/mockito-extensions/org.mockito.plugins.MockMaker new file mode 100644 index 000000000..1f0955d45 --- /dev/null +++ b/de.tu-bs.cs.isf.cbc.util/src/test/resources/mockito-extensions/org.mockito.plugins.MockMaker @@ -0,0 +1 @@ +mock-maker-inline diff --git a/de.tu_bs.cs.isf.cbc.tool.update/.DS_Store b/de.tu_bs.cs.isf.cbc.tool.update/.DS_Store index 8c12f0002..386539117 100644 Binary files a/de.tu_bs.cs.isf.cbc.tool.update/.DS_Store and b/de.tu_bs.cs.isf.cbc.tool.update/.DS_Store differ diff --git a/targetplatform.target b/targetplatform.target index 49a60ed5f..a03d7534b 100644 --- a/targetplatform.target +++ b/targetplatform.target @@ -2,23 +2,41 @@ - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + +