diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-02-12 11:17:29 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-02-12 11:17:29 -0800 |
| commit | bbe5109c4ed1b1d1f48b8208e1bcb4fda0513c59 (patch) | |
| tree | d534b4a4a0f74fc3a890281dfca4dfa549a7eede /Test/og/Answer | |
| parent | 0c73a681516818cfdaa65fb1bb3ab081930a79a6 (diff) | |
fixed another bug reported by ChrisHaw
Added an answer file
Diffstat (limited to 'Test/og/Answer')
| -rw-r--r-- | Test/og/Answer | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/Test/og/Answer b/Test/og/Answer new file mode 100644 index 00000000..712ebfd8 --- /dev/null +++ b/Test/og/Answer @@ -0,0 +1,40 @@ +
+-------------------- foo.bpl --------------------
+OwickiGriesDesugared.bpl(179,4): Error BP5001: This assertion might not hold.
+Execution trace:
+ OwickiGriesDesugared.bpl(17,0): anon0
+ OwickiGriesDesugared.bpl(177,0): inline$YieldChecker_PC$0$L1
+
+Boogie program verifier finished with 3 verified, 1 error
+
+-------------------- bar.bpl --------------------
+OwickiGriesDesugared.bpl(171,4): Error BP5001: This assertion might not hold.
+Execution trace:
+ OwickiGriesDesugared.bpl(17,0): anon0
+ OwickiGriesDesugared.bpl(169,0): inline$YieldChecker_PC$0$L1
+OwickiGriesDesugared.bpl(171,4): Error BP5001: This assertion might not hold.
+Execution trace:
+ OwickiGriesDesugared.bpl(68,0): anon0
+ OwickiGriesDesugared.bpl(169,0): inline$YieldChecker_PC$0$L1
+
+Boogie program verifier finished with 2 verified, 2 errors
+
+-------------------- one.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- linear-set.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- linear-set2.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- FlanaganQadeer.bpl --------------------
+
+Boogie program verifier finished with 3 verified, 0 errors
+
+-------------------- DeviceCacheSimplified.bpl --------------------
+
+Boogie program verifier finished with 5 verified, 0 errors
|