diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
commit | d652155ae013f36a1ee17653a8e458baad2d9c2c (patch) | |
tree | 067d600fe3cd1723afc11682935f0123a1eab653 /Test/linear/f1.bpl | |
parent | d7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff) |
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Test/linear/f1.bpl')
-rw-r--r-- | Test/linear/f1.bpl | 96 |
1 files changed, 48 insertions, 48 deletions
diff --git a/Test/linear/f1.bpl b/Test/linear/f1.bpl index 0d255149..cf786143 100644 --- a/Test/linear/f1.bpl +++ b/Test/linear/f1.bpl @@ -1,48 +1,48 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
-const {:existential true} b0: bool;
-const {:existential true} b1: bool;
-const {:existential true} b2: bool;
-const {:existential true} b3: bool;
-const {:existential true} b4: bool;
-const {:existential true} b5: bool;
-const {:existential true} b6: bool;
-const {:existential true} b7: bool;
-const {:existential true} b8: bool;
-
-axiom(b0);
-axiom(b1);
-axiom(b2);
-axiom(b3);
-axiom(b4);
-axiom(b5);
-axiom(!b6);
-axiom(!b7);
-axiom(b8);
-
-procedure main({:linear_in "1"} x_in: [int]bool)
- requires b0 ==> x_in == mapconstbool(true);
- requires b1 ==> x_in != mapconstbool(false);
-{
- var {:linear "1"} x: [int] bool;
- x := x_in;
-
- call foo(x);
-
- assert b6 ==> x == mapconstbool(true);
- assert b7 ==> x != mapconstbool(false);
- assert b8 ==> x == mapconstbool(false);
-}
-
-procedure foo({:linear_in "1"} x_in: [int]bool)
- requires b2 ==> x_in == mapconstbool(true);
- requires b3 ==> x_in != mapconstbool(false);
-{
- var {:linear "1"} x: [int] bool;
- x := x_in;
-
- assert b4 ==> x == mapconstbool(true);
- assert b5 ==> x != mapconstbool(false);
-
-}
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:builtin "MapConst"} mapconstbool(bool) : [int]bool; +const {:existential true} b0: bool; +const {:existential true} b1: bool; +const {:existential true} b2: bool; +const {:existential true} b3: bool; +const {:existential true} b4: bool; +const {:existential true} b5: bool; +const {:existential true} b6: bool; +const {:existential true} b7: bool; +const {:existential true} b8: bool; + +axiom(b0); +axiom(b1); +axiom(b2); +axiom(b3); +axiom(b4); +axiom(b5); +axiom(!b6); +axiom(!b7); +axiom(b8); + +procedure main({:linear_in "1"} x_in: [int]bool) + requires b0 ==> x_in == mapconstbool(true); + requires b1 ==> x_in != mapconstbool(false); +{ + var {:linear "1"} x: [int] bool; + x := x_in; + + call foo(x); + + assert b6 ==> x == mapconstbool(true); + assert b7 ==> x != mapconstbool(false); + assert b8 ==> x == mapconstbool(false); +} + +procedure foo({:linear_in "1"} x_in: [int]bool) + requires b2 ==> x_in == mapconstbool(true); + requires b3 ==> x_in != mapconstbool(false); +{ + var {:linear "1"} x: [int] bool; + x := x_in; + + assert b4 ==> x == mapconstbool(true); + assert b5 ==> x != mapconstbool(false); + +} |