diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-01-30 12:43:15 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-01-30 12:43:15 -0800 |
| commit | 06055fdd22eeb9015d215e71996e4714c183ef19 (patch) | |
| tree | bdd9aa1ee6667426903f7721abc8d84f1873da83 /Test/linear | |
| parent | b2ed78d44c2b79dd0ed070012ee0d310fb7a4ad0 (diff) | |
handling old() in stable assertions
bug fix in linear
Diffstat (limited to 'Test/linear')
| -rw-r--r-- | Test/linear/Maps.bpl | 24 | ||||
| -rw-r--r-- | Test/linear/list.bpl | 39 | ||||
| -rw-r--r-- | Test/linear/runtest.bat | 11 |
3 files changed, 74 insertions, 0 deletions
diff --git a/Test/linear/Maps.bpl b/Test/linear/Maps.bpl new file mode 100644 index 00000000..5f302034 --- /dev/null +++ b/Test/linear/Maps.bpl @@ -0,0 +1,24 @@ +type X;
+
+function {:builtin "MapAdd"} MapAdd([X]int, [X]int) : [X]int;
+function {:builtin "MapSub"} MapSub([X]int, [X]int) : [X]int;
+function {:builtin "MapMul"} MapMul([X]int, [X]int) : [X]int;
+function {:builtin "MapDiv"} MapDiv([X]int, [X]int) : [X]int;
+function {:builtin "MapMod"} MapMod([X]int, [X]int) : [X]int;
+function {:builtin "MapConst"} MapConstInt(int) : [X]int;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:builtin "MapAnd"} MapAnd([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapNot"} MapNot([X]bool) : [X]bool;
+function {:builtin "MapIte"} MapIteInt([X]bool, [X]int, [X]int) : [X]int;
+function {:builtin "MapIte"} MapIteBool([X]bool, [X]bool, [X]bool) : [X]bool;
+function {:builtin "MapLe"} MapLe([X]int, [X]int) : [X]bool;
+function {:builtin "MapLt"} MapLt([X]int, [X]int) : [X]bool;
+function {:builtin "MapGe"} MapGe([X]int, [X]int) : [X]bool;
+function {:builtin "MapGt"} MapGt([X]int, [X]int) : [X]bool;
+function {:builtin "MapEq"} MapEq([X]int, [X]int) : [X]bool;
+function {:builtin "MapIff"} MapIff([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapImp"} MapImp([X]bool, [X]bool) : [X]bool;
+
+
+
diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl new file mode 100644 index 00000000..9a333351 --- /dev/null +++ b/Test/linear/list.bpl @@ -0,0 +1,39 @@ +var head: X;
+var tail: X;
+var {:linear "Mem"} D: [X]bool;
+var Next:[X]X;
+const nil: X;
+
+procedure malloc() returns (x: X, {:linear "Mem"} M: [X]bool);
+ensures M == MapConstBool(false)[x := true];
+
+procedure Join({:linear "Mem"} A: [X]bool);
+modifies D;
+ensures MapOr(old(D), A) == D;
+
+procedure one()
+requires D[head] && D[tail];
+requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
+ensures D[head] && D[tail];
+ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
+ensures head != tail;
+{
+ var x: X;
+ var {:linear "Mem"} M: [X]bool;
+
+ call x, M := malloc();
+ call Join(M);
+ Next[tail] := x;
+ tail := x;
+ Next[tail] := nil;
+}
+
+procedure two()
+requires head != tail;
+requires D[head] && D[tail];
+requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
+ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
+ensures D[head] && D[tail];
+{
+ head := Next[head];
+}
diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat new file mode 100644 index 00000000..28c91996 --- /dev/null +++ b/Test/linear/runtest.bat @@ -0,0 +1,11 @@ +@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+
+for %%f in (list.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f Maps.bpl
+)
+
|