diff options
| author |  qadeer <unknown> | 2014-07-12 15:31:40 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-07-12 15:31:40 -0700 |
| commit | 85a60be8a0a7ef1438908364b7997dddc4524ed1 (patch) | |
| tree | 356d1801d0338ae1ec91d22909b88ea589cbad11 /Test/og/Program2.bpl | |
| parent | 5ef33fad3a4d6438d7e3c38388639eff7f08533d (diff) | |
added tests
Diffstat (limited to 'Test/og/Program2.bpl')
| -rw-r--r-- | Test/og/Program2.bpl | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/Test/og/Program2.bpl b/Test/og/Program2.bpl new file mode 100644 index 00000000..7713a5d2 --- /dev/null +++ b/Test/og/Program2.bpl @@ -0,0 +1,34 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:phase 1} x:int;
+
+procedure {:yields} {:phase 1} p()
+requires {:phase 1} x >= 5;
+ensures {:phase 1} x >= 8;
+{
+ call yield_x(5);
+ call Incr(1);
+ call yield_x(6);
+ call Incr(1);
+ call yield_x(7);
+ call Incr(1);
+}
+
+procedure {:yields} {:phase 1} q()
+{
+ call Incr(3);
+}
+
+procedure {:yields} {:phase 0,1} Incr(val: int);
+ensures {:atomic}
+|{A:
+ x := x + val; return true;
+}|;
+
+procedure {:yields} {:phase 1} yield_x(n: int)
+requires {:phase 1} x >= n;
+ensures {:phase 1} x >= n;
+{
+ yield;
+ assert {:phase 1} x >= n;
+}
\ No newline at end of file |