changes testcases that use 'heap', which is now a keyword

viperproject · Feb 28, 2024 · 3da1caf · 3da1caf
1 parent 0c0efd7
commit 3da1caf
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 28 deletions.
diff --git a/src/test/resources/all/basic/many_conjuncts.vpr b/src/test/resources/all/basic/many_conjuncts.vpr
@@ -15,7 +15,7 @@ field acq: Bool
 predicate AcqConjunct(x: Ref, idx: Int)
 
 domain parallelHeaps {
-  function heap(x: Ref) : Int
+  function heap_lookup(x: Ref) : Int
   function is_ghost(x:Ref) : Bool
 }
 
@@ -28,25 +28,25 @@ domain reads {
 
 
 method read(data: Ref, count: Ref, ghost: Ref) returns (v: Int)
-  requires heap(data) == 0 && (heap(count) == 0 && (heap(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard))))))))
-  ensures heap(data) == 0 && (heap(count) == 0 && (heap(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard)))))))) && (data.val == v && [true, perm(data.val) == none])
+  requires heap_lookup(data) == 0 && (heap_lookup(count) == 0 && (heap_lookup(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard))))))))
+  ensures heap_lookup(data) == 0 && (heap_lookup(count) == 0 && (heap_lookup(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard)))))))) && (data.val == v && [true, perm(data.val) == none])
 {
   v := data.val
 }
 
 method read_erroneous(data: Ref, count: Ref, ghost: Ref) returns (v: Int)
-  requires heap(data) == 0 && (heap(count) == 0 && (heap(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard))))))))
+  requires heap_lookup(data) == 0 && (heap_lookup(count) == 0 && (heap_lookup(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard))))))))
   //:: ExpectedOutput(postcondition.violated:assertion.false)
-  ensures heap(data) == 0 && (heap(count) == 0 && (heap(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard)))))))) && (data.val == v && [true, perm(data.val) == none] && false)
+  ensures heap_lookup(data) == 0 && (heap_lookup(count) == 0 && (heap_lookup(ghost) == 0 && (is_ghost(ghost) && (acc(data.val, rd()) && (acc(ghost.val, rd()) && (acc(count.acq, wildcard) && count.acq == false && acc(AcqConjunct(count, 0), wildcard) && (acc(count.rel, wildcard) && count.rel == 0 && acc(count.init, wildcard)))))))) && (data.val == v && [true, perm(data.val) == none] && false)
 {
   v := data.val
 }
 
 method read2(data: Ref, count: Ref, ghost: Ref) returns (v: Int)
   requires
-    heap(data) == 0 &&
-    heap(count) == 0 &&
-    heap(ghost) == 0 &&
+    heap_lookup(data) == 0 &&
+    heap_lookup(count) == 0 &&
+    heap_lookup(ghost) == 0 &&
     is_ghost(ghost) &&
     acc(data.val, rd()) &&
     acc(ghost.val, rd()) &&
@@ -58,9 +58,9 @@ method read2(data: Ref, count: Ref, ghost: Ref) returns (v: Int)
     acc(count.init, wildcard)
 
   ensures
-    heap(data) == 0 &&
-    heap(count) == 0 &&
-    heap(ghost) == 0 &&
+    heap_lookup(data) == 0 &&
+    heap_lookup(count) == 0 &&
+    heap_lookup(ghost) == 0 &&
     is_ghost(ghost) &&
     acc(data.val, rd()) &&
     acc(ghost.val, rd()) &&
@@ -78,9 +78,9 @@ method read2(data: Ref, count: Ref, ghost: Ref) returns (v: Int)
 
 method read2_erroneous(data: Ref, count: Ref, ghost: Ref) returns (v: Int)
   requires
-    heap(data) == 0 &&
-    heap(count) == 0 &&
-    heap(ghost) == 0 &&
+    heap_lookup(data) == 0 &&
+    heap_lookup(count) == 0 &&
+    heap_lookup(ghost) == 0 &&
     is_ghost(ghost) &&
     acc(data.val, rd()) &&
     acc(ghost.val, rd()) &&
@@ -93,9 +93,9 @@ method read2_erroneous(data: Ref, count: Ref, ghost: Ref) returns (v: Int)
 
   ensures
     //:: ExpectedOutput(postcondition.violated:assertion.false)
-    heap(data) == 0 &&
-    heap(count) == 0 &&
-    heap(ghost) == 0 &&
+    heap_lookup(data) == 0 &&
+    heap_lookup(count) == 0 &&
+    heap_lookup(ghost) == 0 &&
     is_ghost(ghost) &&
     acc(data.val, rd()) &&
     acc(ghost.val, rd()) &&

diff --git a/src/test/resources/all/issues/silicon/0365.vpr b/src/test/resources/all/issues/silicon/0365.vpr
@@ -16,15 +16,15 @@ function tokCountRef(r:Ref): Ref
 domain parallelHeaps { 
     function temp(x: Ref): Ref 
     function temp_inv(x: Ref): Ref 
-    function heap(x: Ref): Int 
+    function heap_lookup(x: Ref): Int
     function is_ghost(x: Ref): Bool 
 
     // WARNING: The two axioms can cause a matching loop
     axiom inv_temp {
-        (forall r: Ref :: { temp(r) } temp_inv(temp(r)) == r && (is_ghost(r) ? temp(r) == r : heap(temp(r)) == heap(r) - 3))
+        (forall r: Ref :: { temp(r) } temp_inv(temp(r)) == r && (is_ghost(r) ? temp(r) == r : heap_lookup(temp(r)) == heap_lookup(r) - 3))
     } 
     axiom inv_temp_inv {
-        (forall r: Ref :: { temp_inv(r) } temp(temp_inv(r)) == r && (is_ghost(r) ? temp_inv(r) == r : heap(temp_inv(r)) == heap(r) + 3))
+        (forall r: Ref :: { temp_inv(r) } temp(temp_inv(r)) == r && (is_ghost(r) ? temp_inv(r) == r : heap_lookup(temp_inv(r)) == heap_lookup(r) + 3))
     }
 }
 

diff --git a/src/test/resources/quantifiedpermissions/misc/misc1.vpr b/src/test/resources/quantifiedpermissions/misc/misc1.vpr
@@ -1,6 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field val : Int
 
 domain parallelHeaps {
@@ -12,10 +12,10 @@ domain parallelHeaps {
   function temp(x: Ref) : Ref
   function temp_inv(x: Ref) : Ref
 
-  function heap(x: Ref) : Int
+  function heap_lookup(x: Ref) : Int
   function is_ghost(x:Ref) : Bool
 
-  axiom inv_temp { forall r:Ref :: {temp(r)} temp_inv(temp(r)) == r  && (is_ghost(r) ? temp(r) == r : heap(temp(r)) == -3) }
+  axiom inv_temp { forall r:Ref :: {temp(r)} temp_inv(temp(r)) == r  && (is_ghost(r) ? temp(r) == r : heap_lookup(temp(r)) == -3) }
 }
 
 domain reads {
@@ -31,9 +31,9 @@ domain reads {
 
 
 method clone(data: Ref, count: Ref, ghost: Ref)
-  requires    heap(data) == 0
-           && heap(count) == 0
-           && heap(ghost) == 0
+  requires    heap_lookup(data) == 0
+           && heap_lookup(count) == 0
+           && heap_lookup(ghost) == 0
            && is_ghost(ghost)
            && acc(data.val, rd())
            && acc(ghost.val, rd())