diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-06 20:21:12 -0700 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-06 20:21:12 -0700 |
| commit | c411d1bd49cfd9952359339779a08feff11ee776 (patch) | |
| tree | aa252a921a153b8d9f8857911a9ca4b3b5b7541c /Test | |
| parent | b35c3daef15cdaea422bf408c4cff62242a9fb04 (diff) | |
fixed bug (reported by Akash) in treatment of linear parameters to calls
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/linear/Answer | 11 | ||||
| -rw-r--r-- | Test/linear/f1.bpl | 48 | ||||
| -rw-r--r-- | Test/linear/f2.bpl | 19 | ||||
| -rw-r--r-- | Test/linear/runtest.bat | 2 |
4 files changed, 79 insertions, 1 deletions
diff --git a/Test/linear/Answer b/Test/linear/Answer index 680f9895..662e6670 100644 --- a/Test/linear/Answer +++ b/Test/linear/Answer @@ -27,3 +27,14 @@ Execution trace: allocator.bpl(6,3): anon0
Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- f1.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- f2.bpl --------------------
+f2.bpl(18,4): Error BP5001: This assertion might not hold.
+Execution trace:
+ f2.bpl(14,4): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/linear/f1.bpl b/Test/linear/f1.bpl new file mode 100644 index 00000000..0d9189ab --- /dev/null +++ b/Test/linear/f1.bpl @@ -0,0 +1,48 @@ +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 {:entrypoint} main({:linear "1"} x_in: [int]bool)
+ requires b0 ==> x_in == mapconstbool(true);
+ requires b1 ==> x_in != mapconstbool(false);
+{
+ var {:linear "1"} x: [int] bool;
+ assume x == x_in;
+
+ assume x == mapconstbool(true);
+
+ call foo(x);
+
+ assert b6 ==> x == mapconstbool(true);
+ assert b7 ==> x != mapconstbool(false);
+ assert b8 ==> x == mapconstbool(false);
+}
+
+procedure foo({:linear "1"} x_in: [int]bool)
+ requires b2 ==> x_in == mapconstbool(true);
+ requires b3 ==> x_in != mapconstbool(false);
+{
+ var {:linear "1"} x: [int] bool;
+ assume x == x_in;
+
+ assert b4 ==> x == mapconstbool(true);
+ assert b5 ==> x != mapconstbool(false);
+
+}
diff --git a/Test/linear/f2.bpl b/Test/linear/f2.bpl new file mode 100644 index 00000000..4e4bfbcf --- /dev/null +++ b/Test/linear/f2.bpl @@ -0,0 +1,19 @@ +function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
+function {:builtin "MapOr"} mapunion([int]bool, [int]bool) : [int]bool;
+
+procedure Split({:linear "1"} xls: [int]bool) returns ({:linear "1"} xls1: [int]bool, {:linear "1"} xls2: [int]bool);
+ensures xls == mapunion(xls1, xls2) && xls1 != mapconstbool(false) && xls2 != mapconstbool(false);
+
+
+procedure {:entrypoint} main()
+{
+ var {:linear "1"} x: [int] bool;
+ var {:linear "1"} x1: [int] bool;
+ var {:linear "1"} x2: [int] bool;
+
+ havoc x;
+ assume x == mapconstbool(true);
+
+ call x1, x2 := Split(x);
+ assert false;
+}
diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat index 5681784a..3ccd660c 100644 --- a/Test/linear/runtest.bat +++ b/Test/linear/runtest.bat @@ -9,7 +9,7 @@ for %%f in (typecheck.bpl) do ( %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f
)
-for %%f in (list.bpl allocator.bpl) do (
+for %%f in (list.bpl allocator.bpl f1.bpl f2.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f
|