diff options
| author |  qadeer <unknown> | 2013-07-15 01:05:25 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2013-07-15 01:05:25 -0700 |
| commit | ad34aee0bb9e9090418fd1cb2e2fced7ddb625d8 (patch) | |
| tree | 08b240d51e7aee5b70d2690827d3d69d3f6906d9 | |
| parent | 100518bf2d57bd48d5dd24c7a7bf0ee86daeb424 (diff) | |
added another regression
| -rw-r--r-- | Test/og/Answer | 9 | ||||
| -rw-r--r-- | Test/og/async.bpl | 16 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 2 |
3 files changed, 26 insertions, 1 deletions
diff --git a/Test/og/Answer b/Test/og/Answer index c29d38dc..d663de9a 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -98,3 +98,12 @@ Boogie program verifier finished with 2 verified, 0 errors -------------------- perm.bpl --------------------
Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- async.bpl --------------------
+async.bpl(13,1): Error BP5001: This assertion might not hold.
+Execution trace:
+ async.bpl(6,3): anon0
+ async.bpl(6,3): anon0$1
+ (0,0): inline$Proc_YieldChecker_P$1$L0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/og/async.bpl b/Test/og/async.bpl new file mode 100644 index 00000000..15f89bae --- /dev/null +++ b/Test/og/async.bpl @@ -0,0 +1,16 @@ +var x: int;
+var y: int;
+
+procedure {:entrypoint} foo()
+{
+ assume x == y;
+ x := x + 1;
+ async call P();
+ y := y + 1;
+}
+
+procedure P()
+requires x != y;
+{
+ assert x != y;
+}
\ No newline at end of file diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index dd07b4a4..5915a206 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 parallel5.bpl parallel6.bpl parallel7.bpl akash.bpl t1.bpl new1.bpl perm.bpl) do (
+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 (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
|