diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-03-04 11:33:51 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-03-04 11:33:51 -0800 |
| commit | f82dab21f1240fb3f8d67a880f4f93017d85c345 (patch) | |
| tree | cdd03adc32960284e9ec20d8d8640a1709c40556 /Test | |
| parent | 68a39909f93535ad4d091fce647d8a0e8539508f (diff) | |
fixed a bug in og
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/og/Answer | 4 | ||||
| -rw-r--r-- | Test/og/parallel5.bpl | 36 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 2 |
3 files changed, 41 insertions, 1 deletions
diff --git a/Test/og/Answer b/Test/og/Answer index 1b341ee4..154b0193 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -68,3 +68,7 @@ Execution trace: parallel4.bpl(12,3): anon0$2
Boogie program verifier finished with 2 verified, 1 error
+
+-------------------- parallel5.bpl --------------------
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl new file mode 100644 index 00000000..8ee5e436 --- /dev/null +++ b/Test/og/parallel5.bpl @@ -0,0 +1,36 @@ +var a:[int]int;
+
+procedure {:entrypoint} main()
+{
+ var {:linear "tid"} i: int;
+ var {:linear "tid"} j: int;
+ call i := t(i) | j := Yield(j);
+ call i := u(i) | j := u(j);
+}
+
+procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+{
+ assume i == i';
+
+ a[i] := 42;
+ call i := Yield(i);
+ assert a[i] == 42;
+}
+
+procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+{
+ assume i == i';
+
+ a[i] := 42;
+ yield;
+ assert a[i] == 42;
+}
+
+procedure Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+ensures i == i';
+ensures old(a)[i] == a[i];
+{
+ assume i == i';
+ yield;
+ assert old(a)[i] == a[i];
+}
\ No newline at end of file diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index a1cbfba0..64c21618 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 parallel3.bpl) do ( %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
)
-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
|