summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/og/Answer12
-rw-r--r--Test/og/DeviceCache.bpl19
-rw-r--r--Test/og/DeviceCacheWithBuffer.bpl23
-rw-r--r--Test/og/lock.bpl2
-rw-r--r--Test/og/runtest.bat4
-rw-r--r--Test/og/ticket.bpl35
6 files changed, 34 insertions, 61 deletions
diff --git a/Test/og/Answer b/Test/og/Answer
index d4111927..8397d051 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -35,10 +35,6 @@ Execution trace:
Boogie program verifier finished with 3 verified, 2 errors
--------------------- parallel3.bpl --------------------
-
-Boogie program verifier finished with 3 verified, 0 errors
-
-------------------- linear-set.bpl --------------------
Boogie program verifier finished with 2 verified, 0 errors
@@ -71,14 +67,6 @@ Boogie program verifier finished with 2 verified, 1 error
Boogie program verifier finished with 4 verified, 0 errors
--------------------- parallel6.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- parallel7.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
-------------------- akash.bpl --------------------
Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index ede0a31e..c93d5d21 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -1,10 +1,10 @@
type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
-var ghostLock: X;
-var lock: X;
-var currsize: int;
-var newsize: int;
+var {:qed} ghostLock: X;
+var {:qed} lock: X;
+var {:qed} currsize: int;
+var {:qed} newsize: int;
function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
{
@@ -87,7 +87,7 @@ ensures 0 <= bytesRead && bytesRead <= size;
}
READ_DEVICE:
- par Skip() | tid := YieldToWriteCache(tid);
+ par tid := YieldToWriteCache(tid);
call tid := WriteCache(tid, start + size);
call tid := acquire(tid);
call tid, tmp := ReadNewsize(tid);
@@ -95,7 +95,7 @@ READ_DEVICE:
call tid := release(tid);
COPY_TO_BUFFER:
- par Skip() | YieldToReadCache();
+ par YieldToReadCache();
call ReadCache(start, bytesRead);
}
@@ -107,7 +107,7 @@ ensures {:right 1} |{ A: assert ghostLock == tid' && tid' != nil; tid := tid'; r
call tid, j := ReadCurrsize(tid);
while (j < index)
- invariant ghostLock == tid && currsize <= j && tid == tid';
+ invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid';
{
call tid := WriteCacheEntry(tid, j);
j := j + 1;
@@ -155,8 +155,3 @@ ensures {:right 0} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lo
procedure {:yields} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);
ensures {:left 0} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;
-
-procedure {:yields} {:stable} Skip()
-ensures {:both 0} |{ A: return true; }|;
-{
-} \ No newline at end of file
diff --git a/Test/og/DeviceCacheWithBuffer.bpl b/Test/og/DeviceCacheWithBuffer.bpl
index fa2cc611..f1da0ecf 100644
--- a/Test/og/DeviceCacheWithBuffer.bpl
+++ b/Test/og/DeviceCacheWithBuffer.bpl
@@ -1,13 +1,13 @@
type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
-var ghostLock: X;
-var lock: X;
-var currsize: int;
-var newsize: int;
+var {:qed} ghostLock: X;
+var {:qed} lock: X;
+var {:qed} currsize: int;
+var {:qed} newsize: int;
const device: [int]int;
-var cache: [int]int;
+var {:qed} cache: [int]int;
function {:inline} Inv(ghostLock: X, currsize: int, newsize: int, cache: [int]int) : (bool)
{
@@ -93,7 +93,7 @@ ensures (forall i: int :: 0 <= i && i < bytesRead ==> buffer[i] == device[start+
}
READ_DEVICE:
- par Skip() | tid := YieldToWriteCache(tid);
+ par tid := YieldToWriteCache(tid);
call tid := WriteCache(tid, start + size);
call tid := acquire(tid);
call tid, tmp := ReadNewsize(tid);
@@ -101,7 +101,7 @@ READ_DEVICE:
call tid := release(tid);
COPY_TO_BUFFER:
- par Skip() | YieldToReadCache();
+ par YieldToReadCache();
call buffer := ReadCache(start, bytesRead);
}
@@ -113,8 +113,8 @@ ensures {:right 1} |{ A: assert ghostLock == tid' && tid' != nil; tid := tid'; c
call tid, j := ReadCurrsize(tid);
while (j < index)
- invariant ghostLock == tid && currsize <= j && tid == tid';
- invariant cache == (lambda i: int :: if (currsize <= i && i < j) then device[i] else old(cache)[i]);
+ invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid';
+ invariant {:phase 1} cache == (lambda i: int :: if (currsize <= i && i < j) then device[i] else old(cache)[i]);
{
call tid := WriteCacheEntry(tid, j);
j := j + 1;
@@ -168,8 +168,3 @@ ensures {:right 0} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lo
procedure {:yields} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);
ensures {:left 0} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;
-
-procedure {:yields} {:stable} Skip()
-ensures {:both 0} |{ A: return true; }|;
-{
-}
diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 4e4e6dec..c00560fe 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -1,4 +1,4 @@
-var b: bool;
+var {:qed} b: bool;
procedure {:yields} {:entrypoint} main()
{
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index 1325e476..068f361f 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -3,13 +3,13 @@ setlocal
set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl parallel3.bpl) do (
+for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer %%f
)
-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index d620abf3..9f467229 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -4,10 +4,10 @@ function RightClosed(n: int) : [int]bool;
type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
-var t: int;
-var s: int;
-var cs: X;
-var T: [int]bool;
+var {:qed} t: int;
+var {:qed} s: int;
+var {:qed} cs: X;
+var {:qed} T: [int]bool;
procedure Allocate({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
ensures xl != nil;
@@ -50,11 +50,11 @@ requires {:phase 2} tid' != nil && Inv2(T, s, cs);
invariant {:phase 1} Inv1(T, t);
invariant {:phase 2} tid != nil && Inv2(T, s, cs);
{
- par Skip() | Yield0() | Yield1() | Yield2();
+ par Yield1() | Yield2() | Yield();
call tid := Enter(tid);
- par Skip() | Yield0() | Yield1();
+ par Yield1() | Yield2();
call tid := Leave(tid);
- par Skip() | Yield0() | Yield1() | Yield2();
+ par Yield1() | Yield2() | Yield();
}
}
@@ -68,11 +68,11 @@ ensures {:right 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil
var m: int;
tid := tid';
- par Skip() | Yield0() | Yield1();
+ par Yield1() | Yield2();
call tid, m := GetTicketAbstract(tid);
- par Skip() | Yield0();
+ par Yield1();
call tid := WaitAndEnter(tid, m);
- par Skip() | Yield0() | Yield1();
+ par Yield1() | Yield2();
}
procedure {:yields} GetTicketAbstract({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int)
@@ -82,34 +82,29 @@ ensures {:right 1} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; re
{
tid := tid';
- par Skip() | Yield0();
+ par Yield1();
call tid, m := GetTicket(tid);
- par Skip() | Yield0();
+ par Yield1();
}
-procedure {:yields} {:stable} Yield2()
+procedure {:yields} {:stable} Yield()
{
}
-procedure {:yields} {:stable} Yield1()
+procedure {:yields} {:stable} Yield2()
requires {:phase 2} Inv2(T, s, cs);
ensures {:phase 2} Inv2(T, s, cs);
ensures {:both 2} |{ A: return true; }|;
{
}
-procedure {:yields} {:stable} Yield0()
+procedure {:yields} {:stable} Yield1()
requires {:phase 1} Inv1(T, t);
ensures {:phase 1} Inv1(T,t);
ensures {:both 1} |{ A: return true; }|;
{
}
-procedure {:yields} {:stable} Skip()
-ensures {:both 0} |{ A: return true; }|;
-{
-}
-
procedure {:yields} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);
ensures {:both 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 17:34:26 +0000