-
Notifications
You must be signed in to change notification settings - Fork 23
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Adding new test - failing (old behavior)
- Loading branch information
1 parent
3271651
commit 5f91b99
Showing
4 changed files
with
3,309 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortOps{}, SortKItem{}}(Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),inj{SortOp{}, SortOps{}}(Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1")))))))) | ||
|
|
37 changes: 37 additions & 0 deletions
37
test/output/same-name-diff-value/transferFunds.proof.out.diff
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,37 @@ | ||
| version: 13 | ||
| hook: MAP.concat Lbl'Unds'Map'Unds'{} () | ||
| arg: kore[Lbl'Stop'Map{}()] | ||
| arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))] | ||
| hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))] | ||
| function: LblinitGeneratedTopCell{} () | ||
| rule: 231 1 | ||
| VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))] | ||
| function: LblinitKCell{} (0) | ||
| rule: 232 1 | ||
| VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))] | ||
| hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0) | ||
| arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))] | ||
| arg: kore[\dv{SortKConfigVar{}}("$PGM")] | ||
| hook result: kore[Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1")))] | ||
| function: Lblproject'Coln'Ops{} (0:0) | ||
| rule: 313 1 | ||
| VarK = kore[Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1")))] | ||
| function: LblinitAccountsCell{} (1) | ||
| rule: 227 0 | ||
| function: LblinitGeneratedCounterCell{} (2) | ||
| rule: 230 0 | ||
| config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))),dotk{}())),Lbl'-LT-'accounts'-GT-'{}(Lbl'Stop'AccountCellMap{}()),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))] | ||
| rule: 191 4 | ||
| Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))] | ||
| VarACCT = kore[\dv{SortInt{}}("0")] | ||
| VarO = kore[Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))] | ||
| VarVALUE = kore[\dv{SortInt{}}("5")] | ||
| side condition entry: 188 2 | ||
| VarORIGFROM = kore[\dv{SortInt{}}("5")] | ||
| VarVALUE = kore[\dv{SortInt{}}("1")] | ||
| hook: INT.le Lbl'Unds-LT-Eqls'Int'Unds'{} () | ||
| arg: kore[\dv{SortInt{}}("1")] | ||
| arg: kore[\dv{SortInt{}}("5")] | ||
| hook result: kore[\dv{SortBool{}}("true")] | ||
| side condition exit: 188 true | ||
| config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1")),dotk{}())),Lbl'-LT-'accounts'-GT-'{}(LblAccountCellMapItem{}(Lbl'-LT-'acctID'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'account'-GT-'{}(Lbl'-LT-'acctID'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'balance'-GT-'{}(\dv{SortInt{}}("5"))))),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,64 @@ | ||
| module SAME-NAME-DIFF-VALUE | ||
| imports INT | ||
| imports K-EQUAL | ||
| imports BOOL | ||
|
|
||
| configuration <k> $PGM:Ops </k> | ||
| <accounts> | ||
| <account multiplicity="*" type="Map"> | ||
| <acctID> 0 </acctID> | ||
| <balance> 0 </balance> | ||
| </account> | ||
| </accounts> | ||
|
|
||
| syntax Ops ::= Op ";" Ops [symbol(seq)] | ||
| | Op | ||
|
|
||
| syntax Op ::= "#transferFunds" Int Int Int | ||
| | "#init" Int Int | ||
|
|
||
| syntax NoOp ::= "#finish" | ||
|
|
||
|
|
||
| rule <k> #init ACCT VALUE ; O:Op => O </k> | ||
| <accounts> | ||
| ( .Bag | ||
| => | ||
| <account> | ||
| <acctID> ACCT </acctID> | ||
| <balance> VALUE </balance> | ||
| </account> | ||
| ) | ||
| </accounts> | ||
|
|
||
| rule <k> #transferFunds ACCT ACCT VALUE => .K ... </k> | ||
| <account> | ||
| <acctID> ACCT </acctID> | ||
| <balance> ORIGFROM </balance> | ||
| </account> | ||
| requires VALUE <=Int ORIGFROM | ||
|
|
||
|
|
||
| rule <k> #transferFunds ACCTFROM ACCTTO VALUE => .K ... </k> | ||
| <account> | ||
| <acctID> ACCTFROM </acctID> | ||
| <balance> ORIGFROM => ORIGFROM -Int VALUE </balance> | ||
| ... | ||
| </account> | ||
| <account> | ||
| <acctID> ACCTTO </acctID> | ||
| <balance> ORIGTO => ORIGTO +Int VALUE </balance> | ||
| ... | ||
| </account> | ||
| requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM | ||
| [preserves-definedness] | ||
|
|
||
| rule <k> #transferFunds ACCTFROM _ACCTTO VALUE => .K ... </k> | ||
| <account> | ||
| <acctID> ACCTFROM </acctID> | ||
| <balance> ORIGFROM </balance> | ||
| ... | ||
| </account> | ||
| requires VALUE >Int ORIGFROM | ||
|
|
||
| endmodule |
Oops, something went wrong.