diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-02-01 21:43:07 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-02-01 21:43:07 -0800 |
| commit | 0ad7d270e9a989919d9291a86a018fe55349022b (patch) | |
| tree | e3896e25ce0c3c8ded1075cffc819e88123c8acc /Test/og/FlanaganQadeer.bpl | |
| parent | 06055fdd22eeb9015d215e71996e4714c183ef19 (diff) | |
fixed bug in OG
added another OG sample illustrating rely-guarantee encoding
Diffstat (limited to 'Test/og/FlanaganQadeer.bpl')
| -rw-r--r-- | Test/og/FlanaganQadeer.bpl | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl new file mode 100644 index 00000000..63a7fc0d --- /dev/null +++ b/Test/og/FlanaganQadeer.bpl @@ -0,0 +1,42 @@ +const nil: X;
+var l: X;
+var x: int;
+
+procedure {:entrypoint} main()
+{
+ var {:linear "tid"} tid: X;
+ var val: int;
+
+ while (*)
+ {
+ havoc tid, val;
+ assume tid != nil;
+ call {:async} foo(tid, val);
+ }
+}
+
+procedure foo({:linear "tid"} tid': X, val: int)
+requires tid' != nil;
+{
+ var {:linear "tid"} tid: X;
+ assume tid == tid';
+
+ assume l == nil;
+ l := tid;
+ call tid := Yield(tid);
+ x := val;
+ call tid := Yield(tid);
+ assert x == val;
+ call tid := Yield(tid);
+ l := nil;
+}
+
+procedure Yield({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)
+requires tid' != nil;
+ensures tid == tid';
+ensures old(l) == tid ==> old(l) == l && old(x) == x;
+{
+ assume tid == tid';
+ assert {:yield} tid != nil;
+ assert (old(l) == tid ==> old(l) == l && old(x) == x);
+}
\ No newline at end of file |