diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
commit | 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d (patch) | |
tree | 27d5f9b0d130c6c1a6758bc0b7456b0aa51e34e0 /Test/inline/test5.bpl | |
parent | e11d65009d0b4ba1327f5f5dd6b26367330611f0 (diff) |
Normalise line endings using a .gitattributes file. Unfortunately
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
Diffstat (limited to 'Test/inline/test5.bpl')
-rw-r--r-- | Test/inline/test5.bpl | 162 |
1 files changed, 81 insertions, 81 deletions
diff --git a/Test/inline/test5.bpl b/Test/inline/test5.bpl index d7a80737..a0a25faf 100644 --- a/Test/inline/test5.bpl +++ b/Test/inline/test5.bpl @@ -1,81 +1,81 @@ -// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// test a case, where the inlined proc comes before the caller
-
-procedure {:inline 2} foo()
- modifies x;
-{
- x := x + 1;
-}
-
-var x:int;
-
-procedure bar()
- modifies x;
-{
- x := 3;
- call foo();
- assert x == 4;
- call foo();
- assert x == 5;
-}
-
-// -------------------------------------------------
-
-var Mem : [int]int;
-
-procedure {:inline 1} P(x:int)
- modifies Mem;
-{
- Mem[x] := 1;
-}
-
-procedure mainA()
- modifies Mem;
-{
- Mem[1] := 0;
- call P(0);
- call P(1);
- assert Mem[1] == 0; // error
-}
-
-procedure mainB()
- modifies Mem;
-{
- Mem[1] := 0;
- call P(0);
- call P(1);
- assert Mem[1] == 1; // good
-}
-
-procedure mainC()
- modifies Mem;
-{
- Mem[1] := 0;
- call P(0);
- call P(1);
- assert Mem[1] == 1; // good
-}
-
-// -------------------------------------------------
-
-type ref;
-var xyz: ref;
-
-procedure xyzA();
- modifies xyz;
- ensures old(xyz) == xyz;
-
-procedure {:inline 1} xyzB()
- modifies xyz;
-{
- call xyzA();
-}
-
-procedure xyzMain()
- modifies xyz;
-{
- call xyzA();
- assert old(xyz) == xyz;
- call xyzB();
-}
+// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// test a case, where the inlined proc comes before the caller + +procedure {:inline 2} foo() + modifies x; +{ + x := x + 1; +} + +var x:int; + +procedure bar() + modifies x; +{ + x := 3; + call foo(); + assert x == 4; + call foo(); + assert x == 5; +} + +// ------------------------------------------------- + +var Mem : [int]int; + +procedure {:inline 1} P(x:int) + modifies Mem; +{ + Mem[x] := 1; +} + +procedure mainA() + modifies Mem; +{ + Mem[1] := 0; + call P(0); + call P(1); + assert Mem[1] == 0; // error +} + +procedure mainB() + modifies Mem; +{ + Mem[1] := 0; + call P(0); + call P(1); + assert Mem[1] == 1; // good +} + +procedure mainC() + modifies Mem; +{ + Mem[1] := 0; + call P(0); + call P(1); + assert Mem[1] == 1; // good +} + +// ------------------------------------------------- + +type ref; +var xyz: ref; + +procedure xyzA(); + modifies xyz; + ensures old(xyz) == xyz; + +procedure {:inline 1} xyzB() + modifies xyz; +{ + call xyzA(); +} + +procedure xyzMain() + modifies xyz; +{ + call xyzA(); + assert old(xyz) == xyz; + call xyzB(); +} |