diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-18 21:15:20 -0700 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-18 21:15:20 -0700 |
| commit | 64d8963508ce048d00db3766f4ca597b792c1b95 (patch) | |
| tree | 67801fe71cd2ceb7eb851833dd489751baa21ce2 /Test/og/new1.bpl | |
| parent | 89b20adf23750478098578895fef9ca3b9170927 (diff) | |
reworked the linear and og implementation based on available variables theory
Diffstat (limited to 'Test/og/new1.bpl')
| -rw-r--r-- | Test/og/new1.bpl | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl new file mode 100644 index 00000000..472e64c6 --- /dev/null +++ b/Test/og/new1.bpl @@ -0,0 +1,38 @@ +function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;
+
+var g:int;
+
+var {:linear "Perm"} Permissions: [int]bool;
+
+procedure Allocate_Perm() returns ({:linear "Perm"} xls: [int]bool);
+modifies Permissions;
+requires Permissions == mapconstbool(true);
+ensures xls == mapconstbool(true) && Permissions == mapconstbool(false);
+
+procedure PB({:linear "Perm"} permVar_in:[int]bool)
+requires permVar_in[0] && g == 0;
+{
+ var {:linear "Perm"} permVar_out: [int]bool;
+ permVar_out := permVar_in;
+
+ yield;
+ assert permVar_out[0];
+ assert g == 0;
+
+ g := g + 1;
+
+ yield;
+ assert permVar_out[0];
+ assert g == 1;
+}
+
+procedure{:entrypoint} Main()
+requires Permissions == mapconstbool(true);
+{
+ var {:linear "Perm"} permVar_out: [int]bool;
+
+ call permVar_out := Allocate_Perm();
+
+ g := 0;
+ async call PB(permVar_out);
+}
|