Merge pull request #679 from viperproject/meilers_reenable_tests

Reenabling tests for some examples
viperproject · Apr 20, 2023 · 747ded6 · 747ded6
2 parents 47c42ac + 6364d76
commit 747ded6
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 8 deletions.
diff --git a/src/test/resources/examples/longest-common-prefix/longest-common-prefix.vpr b/src/test/resources/examples/longest-common-prefix/longest-common-prefix.vpr
@@ -5,7 +5,6 @@
  * VerifyThis@FM2012: http://fm2012.verifythis.org/challenges
  */
 
-//:: IgnoreFile(/silicon/issue/398/)
 
 define access(a) forall k: Int :: 0 <= k && k < len(a) ==> acc(loc(a, k).val)
 define untouched(a) forall k: Int :: 0 <= k && k < len(a) ==> loc(a, k).val == old(loc(a, k).val)

diff --git a/src/test/resources/examples/tree-delete-min/tree_delete_min.vpr b/src/test/resources/examples/tree-delete-min/tree_delete_min.vpr
@@ -1,7 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-//:: IgnoreFile(/carbon/issue/280/)
 
 /* This example shows how magic wands can be used to specify the
  * imperative version of challenge 3 from the VerifyThis@FM2012

diff --git a/src/test/resources/examples/vmcai2016/encoding-adts.vpr b/src/test/resources/examples/vmcai2016/encoding-adts.vpr
@@ -10,8 +10,6 @@
  * properties of functions over such a data type can proved.
  */
 
-//:: IgnoreFile(/carbon/issue/280/)
-
 domain list {
 
   /* Constructors */

diff --git a/src/test/resources/examples/vmcai2016/linked-list-predicates-with-wands.vpr b/src/test/resources/examples/vmcai2016/linked-list-predicates-with-wands.vpr
@@ -2,7 +2,6 @@
 // http://creativecommons.org/publicdomain/zero/1.0/
 
 //:: IgnoreFile(/carbon/issue/102/)
-//:: IgnoreFile(/silicon/issue/208/)
 
 /*****************************************************************
  * List Nodes
@@ -21,7 +20,7 @@ predicate lseg(this: Ref, end: Ref)
 function contentNodes(this: Ref, end: Ref): Seq[Int]
   requires acc(lseg(this, end))
   ensures  this == end ==> result == Seq[Int]()
-  ensures  this != end ==> result[0] == unfolding acc(lseg(this, end)) in this.data
+  ensures  this != end ==> |result| > 0 && result[0] == unfolding acc(lseg(this, end)) in this.data
   ensures  forall i: Int, j: Int :: 0 <= i && i < j && j < |result| ==> result[i] <= result[j]
 {
   this == end ? Seq[Int]() :
@@ -138,6 +137,8 @@ method insert(this: Ref, elem: Int) returns (index: Int)
       invariant ptr.next != null ==> ptr.data <= unfolding acc(lseg(ptr.next, null)) in ptr.next.data
       invariant A --* B
     {
+
+      assert A --* B
       var prev: Ref := ptr
 
       unfold acc(lseg(ptr.next, null))
@@ -146,7 +147,8 @@ method insert(this: Ref, elem: Int) returns (index: Int)
 
       package (A) --* B {
           fold acc(lseg(prev, null))
-          apply acc(lseg(prev, null)) && contentNodes(prev, null)[0] == old(content(this))[index-1] --* B
+          apply acc(lseg(prev, null)) && contentNodes(prev, null)[0] == old(content(this))[index-2] --*
+                (acc(lseg(hd, null)) && contentNodes(hd, null) == old(content(this))[0..index-2] ++ old[lhs](contentNodes(prev, null)))
       }
     }
 
@@ -194,7 +196,7 @@ field held: Int
 field changed: Bool
 
 method test(lock: Ref)
-  ensures [true, forperm[held] r :: false]
+  ensures [true, forperm r: Ref [r.held] :: false]
 {
   /* Acquire lock (without deadlock checking) */
   inhale acc(List(lock)) && acc(lock.held) && acc(lock.changed)