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/perm.bpl | |
| parent | 89b20adf23750478098578895fef9ca3b9170927 (diff) | |
reworked the linear and og implementation based on available variables theory
Diffstat (limited to 'Test/og/perm.bpl')
| -rw-r--r-- | Test/og/perm.bpl | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl new file mode 100644 index 00000000..78889868 --- /dev/null +++ b/Test/og/perm.bpl @@ -0,0 +1,50 @@ +var x: int;
+function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;
+
+function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool;
+
+procedure Split({:linear "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1: [int]bool, {:linear "Perm"} xls2: [int]bool);
+ ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);
+
+
+procedure {:entrypoint} mainE({:linear "Perm"} permVar_in: [int]bool)
+ free requires permVar_in == ch_mapconstbool(true);
+ free requires permVar_in[0];
+ modifies x;
+{
+ var {:linear "Perm"} permVar_out: [int]bool;
+ var {:linear "Perm"} permVarOut2: [int]bool;
+
+ permVar_out := permVar_in;
+
+ assume x == 0;
+
+ yield;
+ assert x == 0;
+ assert permVar_out[0];
+ assert permVar_out == ch_mapconstbool(true);
+
+ call permVar_out, permVarOut2 := Split(permVar_out);
+ async call foo(permVarOut2);
+}
+
+procedure foo({:linear "Perm"} permVar_in: [int]bool)
+ free requires permVar_in != ch_mapconstbool(false);
+ free requires permVar_in[1];
+ requires x == 0;
+ modifies x;
+{
+ var {:linear "Perm"} permVar_out: [int]bool;
+ permVar_out := permVar_in;
+
+ yield;
+ assert permVar_out[1];
+ assert x == 0;
+
+ x := x + 1;
+
+ yield;
+ assert permVar_out[1];
+ assert x == 1;
+}
+
|