add tests

src/main/scala/Utils.scala

@@ -6,17 +6,18 @@
 
 package viper.silicon
 
-import scala.annotation.implicitNotFound
-import scala.collection.immutable.ArraySeq
+import viper.silicon.state.terms.{Sort, Term, True, Var}
+import viper.silicon.verifier.Verifier
 import viper.silver
+import viper.silver.ast.utility.Triggers.TriggerGenerationWithAddAndSubtract
+import viper.silver.ast.utility.rewriter.Traverse
 import viper.silver.components.StatefulComponent
-import viper.silver.verifier.{VerificationError, errors}
 import viper.silver.verifier.errors.Internal
 import viper.silver.verifier.reasons.{FeatureUnsupported, UnexpectedNode}
-import viper.silver.ast.utility.rewriter.Traverse
-import viper.silicon.state.terms.{Sort, Term, Var}
-import viper.silicon.verifier.Verifier
-import viper.silver.ast.utility.Triggers.TriggerGenerationWithAddAndSubtract
+import viper.silver.verifier.{VerificationError, errors}
+
+import scala.annotation.implicitNotFound
+import scala.collection.immutable.ArraySeq
 
 package object utils {
   def freshSnap: (Sort, Verifier) => Var = (sort, v) => v.decider.fresh(sort)
@@ -131,6 +132,10 @@ package object utils {
                     (e0: silver.ast.Exp, e1: silver.ast.Exp) => silver.ast.Or(e0, e1)(e0.pos, e0.info),
                      silver.ast.FalseLit()(emptyPos))
 
+    def removeKnownToBeTrueExp(exps: List[silver.ast.Exp], terms: List[Term]): List[silver.ast.Exp] = {
+      exps.zip(terms).filter(t => t._2 != True).map(e => e._1)
+    }
+
     /** Note: be aware of Silver issue #95!*/
     def rewriteRangeContains(program: silver.ast.Program): silver.ast.Program =
       program.transform({

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -15,6 +15,7 @@ import viper.silicon.state._
 import viper.silicon.state.terms._
 import viper.silicon.state.terms.perms.{IsNonPositive, IsPositive}
 import viper.silicon.supporters.functions.NoopFunctionRecorder
+import viper.silicon.utils.ast.{BigAnd, removeKnownToBeTrueExp}
 import viper.silicon.verifier.Verifier
 import viper.silicon.{MList, MMap}
 import viper.silver.ast
@@ -335,13 +336,12 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
         totalPermSum = PermPlus(totalPermSum, Ite(eq, ch.perm, NoPerm))
         totalPermTaken = PermPlus(totalPermTaken, permTaken)
+        val constraintTerms = List(IsValidPermVar(permTaken), PermAtMost(permTaken, ch.perm), Implies(Not(eq), permTaken === NoPerm))
+        val constraintExp = BigAnd(removeKnownToBeTrueExp(List(ast.TrueLit()(), ast.TrueLit()(), ast.TrueLit()()), constraintTerms)) // TODO ake
 
-        val constraint = And(IsValidPermVar(permTaken),
-          PermAtMost(permTaken, ch.perm),
-          Implies(Not(eq), permTaken === NoPerm)
-        )
+        val constraint = And(constraintTerms)
 
-        v.decider.assume(constraint, new DebugExp("Test"))
+        v.decider.assume(constraint, new DebugExp(constraintExp, s.substituteVarsInExp(constraintExp)))
         newFr = newFr.recordArp(permTaken, constraint)
 
         ch.withPerm(PermMinus(ch.perm, permTaken))

src/test/resources/viperDebugger/predicateFold.vpr

@@ -1,12 +1,12 @@
 
-predicate greater0(i : Int)
+predicate greater0(i : Int, p : Perm)
 {
     i >= 0
 }
 
 method my_fold(n : Int)
     requires n >= 0
-    ensures greater0(n)
+    ensures greater0(n, 1/2)
 {
-    fold greater0(n)
+    fold greater0(n, 1/2)
 }

src/test/resources/viperDebugger/references.vpr

@@ -9,4 +9,17 @@ method test_references(n : Ref)
     i := i + n.val
 
     assert i == n.val
+}
+
+
+method test_references2(n : Ref)
+    requires acc(n.val, 1/2) && n.val >= 0
+{
+    var i : Ref
+    i := new(*)
+
+    i.val := 2
+    i.val := i.val + n.val
+
+    assert i.val == n.val
 }

src/test/resources/viperDebugger/sequences.vpr

@@ -15,4 +15,22 @@ method test_sequence_append(s1 : Seq[Int], s2: Seq[Int])
     var s : Seq[Int]
     s := s1 ++ s2
     assert |s| > 1
+}
+
+method seq_sum(list : Seq[Int])
+{
+    var i : Int
+    var sum : Int
+
+    i := 0
+    sum := 0
+
+    while(i < |list|)
+        invariant 0 <= i && i <= |list|
+    {
+        sum := sum + list[i]
+        i := i + 1
+    }
+
+    assert i == |list|
 }