diff options
| author |  qadeer <unknown> | 2014-02-07 22:22:23 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-02-07 22:22:23 -0800 |
| commit | 1f0945b2744ff44091f8574237324506764cfe37 (patch) | |
| tree | abca71419bf02ef5dc6d04b395335fe28f0c02a5 /Test/og | |
| parent | de9be69954d167a71c74ff68dd27e8cc96ba9c12 (diff) | |
added another example and fixed a bug regarding initialization of pc/ok
snapshots per loop header
Diffstat (limited to 'Test/og')
| -rw-r--r-- | Test/og/Answer | 4 | ||||
| -rw-r--r-- | Test/og/lock2.bpl | 59 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 2 |
3 files changed, 64 insertions, 1 deletions
diff --git a/Test/og/Answer b/Test/og/Answer index c9e349e1..511a3ad5 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -108,6 +108,10 @@ Boogie program verifier finished with 28 verified, 0 errors Boogie program verifier finished with 6 verified, 0 errors
+-------------------- lock2.bpl --------------------
+
+Boogie program verifier finished with 6 verified, 0 errors
+
-------------------- multiset.bpl --------------------
Boogie program verifier finished with 102 verified, 0 errors
diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl new file mode 100644 index 00000000..5d532c81 --- /dev/null +++ b/Test/og/lock2.bpl @@ -0,0 +1,59 @@ +var {:qed} b: int;
+
+procedure {:yields} {:entrypoint} main()
+{
+ while (*)
+ {
+ async call Customer();
+ }
+}
+
+procedure {:yields} {:stable} Customer()
+{
+ while (*)
+ {
+ yield;
+
+ call Enter();
+
+ yield;
+
+ call Leave();
+ }
+
+ yield;
+}
+
+procedure {:yields} Enter()
+ensures {:atomic 1} |{ A: assume b == 0; b := 1; return true; }|;
+{
+ var _old, curr: int;
+ L:
+ yield;
+ call _old := CAS(0, 1);
+ yield;
+ if (_old == 0) {
+ return;
+ }
+ while (true) {
+ yield;
+ call curr := Read();
+ yield;
+ if (curr == 0) {
+ goto L;
+ }
+ }
+}
+
+procedure {:yields} Read() returns (val: int);
+ensures {:atomic 0} |{ A: val := b; return true; }|;
+
+procedure {:yields} CAS(prev: int, next: int) returns (_old: int);
+ensures {:atomic 0} |{
+A: _old := b; goto B, C;
+B: assume _old == prev; b := next; return true;
+C: assume _old != prev; return true;
+}|;
+
+procedure {:yields} Leave();
+ensures {:atomic 0} |{ A: b := 0; return true; }|;
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index 30bd66cc..b5802aa5 100644 --- a/Test/og/runtest.bat +++ b/Test/og/runtest.bat @@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl) do ( %BGEXE% %* /nologo /noinfer %%f
)
-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 DeviceCache.bpl ticket.bpl lock.bpl multiset.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 DeviceCache.bpl ticket.bpl lock.bpl lock2.bpl multiset.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f
|