diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-01-30 12:43:15 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-01-30 12:43:15 -0800 |
| commit | 06055fdd22eeb9015d215e71996e4714c183ef19 (patch) | |
| tree | bdd9aa1ee6667426903f7721abc8d84f1873da83 /Test/og/bar.bpl | |
| parent | b2ed78d44c2b79dd0ed070012ee0d310fb7a4ad0 (diff) | |
handling old() in stable assertions
bug fix in linear
Diffstat (limited to 'Test/og/bar.bpl')
| -rw-r--r-- | Test/og/bar.bpl | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl new file mode 100644 index 00000000..cddc5338 --- /dev/null +++ b/Test/og/bar.bpl @@ -0,0 +1,29 @@ +var g:int;
+
+procedure PB()
+{
+ g := g + 1;
+}
+
+procedure PC()
+ ensures g == old(g);
+{
+ assert{:yield} g == old(g);
+}
+
+procedure PD()
+{
+ g := 3;
+ call PC();
+ assert g == 3;
+}
+
+procedure{:entrypoint} Main2()
+{
+ while (true)
+ {
+ call{:async} PB();
+ call{:async} PC();
+ call{:async} PD();
+ }
+}
|