diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-03-01 22:05:19 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-03-01 22:05:19 -0800 |
| commit | abdbd2a717efd1e6184bf1113ed2cce63da0d0ea (patch) | |
| tree | 192a5dac7dfcf28cc8278964f4dff4cb2a4273c3 /Test/og/parallel1.bpl | |
| parent | c5c2c9465a53e4b35a20ad5efe73882dc6a5af34 (diff) | |
added parallel calls
Diffstat (limited to 'Test/og/parallel1.bpl')
| -rw-r--r-- | Test/og/parallel1.bpl | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl new file mode 100644 index 00000000..cb3502b4 --- /dev/null +++ b/Test/og/parallel1.bpl @@ -0,0 +1,29 @@ +var g:int;
+
+procedure PB()
+{
+ g := g + 1;
+}
+
+procedure PC()
+ ensures g == 3;
+{
+ g := 3;
+ yield;
+ assert g == 3;
+}
+
+procedure PD()
+{
+ call PC();
+ assert g == 3;
+ yield;
+}
+
+procedure{:entrypoint} Main()
+{
+ while (true)
+ {
+ call PB() | PC() | PD();
+ }
+}
|