From e8272220e94c52a8425cba727bebb5f7050405ab Mon Sep 17 00:00:00 2001
From: stefanheule <unknown>
Date: Mon, 18 Jul 2011 10:44:12 +0200
Subject: Chalice: Fix a problem with permission expressions. Prevsiously,
 exhaling "acc(o.f,100-rd) && acc(o.f,rd)" resulted in a contradiction. This
 is now solved by using a two-step exhale (loosely speaking, read permissions
 and functional properties are exhaled first, and only afterwards all other
 permissions). Extended testcases appropriately.

---
 .../permission-model/permission_arithmetic.chalice | 38 ++++++++++++++++++++++
 .../permission_arithmetic.output.txt               | 21 ++++++------
 2 files changed, 49 insertions(+), 10 deletions(-)

(limited to 'Chalice/tests/permission-model')

diff --git a/Chalice/tests/permission-model/permission_arithmetic.chalice b/Chalice/tests/permission-model/permission_arithmetic.chalice
index 94cf30a3..fa457981 100644
--- a/Chalice/tests/permission-model/permission_arithmetic.chalice
+++ b/Chalice/tests/permission-model/permission_arithmetic.chalice
@@ -2,6 +2,8 @@ class Cell {
   var x: int;
   var i: int;
   var y: Cell;
+  var f: int;
+  var g: int;
   
   invariant rd(x);
   
@@ -189,5 +191,41 @@ class Cell {
     fold valid
   }
   
+  method a27()
+    requires acc(f,100-rd) && acc(f,rd)
+  {
+    assert acc(f) // ok, we have full access
+  }
+  
+  method a28()
+    requires acc(f)
+  {
+    call a27();
+    var x: int
+    x := f // ERROR: no permission left
+  }
+  
+  method a29()
+    requires acc(f, 100-rd) && acc(g, rd)
+  {  }
+
+  method a30()
+    requires acc(f, 100) && acc(g, rd)
+  {
+    call a29();
+    var tmp: int := this.g;
+  }
+  
+  method a31(c: Cell)
+    requires acc(f, 100-rd) && acc(c.f, rd)
+  {  }
+
+  method a32(c: Cell)
+    requires acc(f, 100) && acc(c.f, rd)
+  {
+    call a31(c);
+    var tmp: int := this.f;
+  }
+  
   method void() requires rd(x); ensures rd(x); {}
 }
diff --git a/Chalice/tests/permission-model/permission_arithmetic.output.txt b/Chalice/tests/permission-model/permission_arithmetic.output.txt
index 0b2b5335..f4859de5 100644
--- a/Chalice/tests/permission-model/permission_arithmetic.output.txt
+++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt
@@ -1,13 +1,14 @@
 Verification of permission_arithmetic.chalice using parameters="" 
 
-  24.5: Assertion might not hold. The permission at 24.12 might not be positive.
-  40.5: The precondition at 33.14 might not hold. The permission at 33.14 might not be positive.
-  73.3: The postcondition at 75.13 might not hold. Insufficient fraction at 75.13 for Cell.x.
-  86.3: The postcondition at 88.13 might not hold. Insufficient epsilons at 88.22  for Cell.x.
-  103.20: Location might not be readable.
-  109.20: Location might not be readable.
-  145.5: Monitor invariant might not hold. Insufficient fraction at 6.13 for Cell.x.
-  162.3: The postcondition at 164.13 might not hold. The permission at 164.13 might not be positive.
-  174.3: The postcondition at 176.13 might not hold. Insufficient fraction at 176.13 for Cell.x.
+  26.5: Assertion might not hold. The permission at 26.12 might not be positive.
+  42.5: The precondition at 35.14 might not hold. The permission at 35.14 might not be positive.
+  75.3: The postcondition at 77.13 might not hold. Insufficient fraction at 77.13 for Cell.x.
+  88.3: The postcondition at 90.13 might not hold. Insufficient epsilons at 90.22  for Cell.x.
+  105.20: Location might not be readable.
+  111.20: Location might not be readable.
+  147.5: Monitor invariant might not hold. Insufficient fraction at 8.13 for Cell.x.
+  164.3: The postcondition at 166.13 might not hold. The permission at 166.13 might not be positive.
+  176.3: The postcondition at 178.13 might not hold. Insufficient fraction at 178.13 for Cell.x.
+  205.10: Location might not be readable.
 
-Boogie program verifier finished with 47 verified, 9 errors
+Boogie program verifier finished with 58 verified, 10 errors
-- 
cgit v1.2.3