sequences: fix and add tests

src/main/scala/decider/Decider.scala

@@ -212,7 +212,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
         }
         case None => {
           pathConditions.setCurrentBranchCondition(t, None)
-          assume(t, new DebugExp("current branch condition"))
+          assume(t, new DebugExp("unknown branch condition"))
         } // TODO ake
       }
     }

src/main/scala/resources/PropertyInterpreter.scala

@@ -117,7 +117,7 @@ abstract class PropertyInterpreter {
       case _ =>
         val leftCond = buildPathCondition(left, info)
         val rightCond =  buildPathCondition(right, info)
-        new Pair(terms.Equals(leftCond.getFirst,rightCond.getFirst), ast.EqCmp(leftCond.getSecond, rightCond.getSecond)())
+        new Pair(terms.Equals(leftCond.getFirst, rightCond.getFirst), ast.EqCmp(leftCond.getSecond, rightCond.getSecond)())
     }
   }
 

src/main/scala/rules/Evaluator.scala

@@ -173,7 +173,7 @@ object evaluator extends EvaluationRules {
 
       case _: ast.WildcardPerm =>
         val (tVar, tConstraints) = v.decider.freshARP()
-        v.decider.assume(tConstraints, new DebugExp("Fresh ARP"))
+        v.decider.assume(tConstraints, new DebugExp(s"WildcardPerm Access: ${tConstraints.toString}"))
         /* TODO: Only record wildcards in State.constrainableARPs that are used in exhale
          *       position. Currently, wildcards used in inhale position (only) may not be removed
          *       from State.constrainableARPs (potentially inefficient, but should be sound).
@@ -940,12 +940,13 @@ object evaluator extends EvaluationRules {
                       } else failure2}
             } else failure1}}})
 
-      case ast.ExplicitSeq(es) =>
+      case seq@ast.ExplicitSeq(es) =>
         evals2(s, es, Nil, _ => pve, v)((s1, tEs, v1) => {
           val tSeq =
             tEs.tail.foldLeft[SeqTerm](SeqSingleton(tEs.head))((tSeq, te) =>
               SeqAppend(tSeq, SeqSingleton(te)))
-          v1.decider.assume(SeqLength(tSeq) === IntLiteral(es.size), new DebugExp("Init sequence length"))
+          val exp = ast.EqCmp(ast.SeqLength(seq)(), ast.IntLit(es.size)())()
+          v1.decider.assume(SeqLength(tSeq) === IntLiteral(es.size), new DebugExp(exp, s1.substituteVarsInExp(exp)))
           Q(s1, tSeq, v1)})
 
       /* Sets and multisets */

src/main/scala/state/State.scala

@@ -127,7 +127,10 @@ final case class State(g: Store = Store(),
 
   def substituteVarsInExp(e : ast.Exp): ast.Exp = {
     val varMapping = g.values.map { case (localVar, term) => {
-      val newName = term.toString.replaceAll("@.. ", " ")
+      val newName = term match {
+        case Var(n, _) => n.name.substring(0, n.name.lastIndexOf("@"))
+        case _ => term.toString.replaceAll("@.. ", " ")
+      }
       localVar.name -> LocalVar(newName, localVar.typ)(localVar.pos, localVar.info, localVar.errT)
     } }
     Sanitizer.replaceFreeVariablesInExpression(e, varMapping, Set())

src/test/resources/viperDebugger/globalAssumptions.vpr

@@ -0,0 +1,22 @@
+field f: Int
+
+predicate P(x: Ref) { acc(x.f, wildcard) }
+
+method test40(x: Ref, y: Ref)
+  requires acc(x.f, 1/2) && acc(y.f, 1/2)
+{
+  fold P(x)
+  exhale acc(x.f, perm(x.f))
+  exhale acc(y.f, perm(y.f))
+  unfold P(x)
+  if (y == x) {
+    assert y.f == old(y.f)
+  }
+}
+
+method test50(x: Ref, y: Ref)
+{
+  inhale acc(P(x), 1/2) && acc(P(y), 1/2)
+  //:: ExpectedOutput(exhale.failed:insufficient.permission)
+  exhale acc(P(x), wildcard) && acc(P(y), 1/2)
+}

src/test/resources/viperDebugger/predicateUnfoldingWithRef.vpr

@@ -0,0 +1,14 @@
+field val : Int
+
+
+predicate greater0(n : Ref, p : Perm)
+{
+    none < p && p <= write && acc(n.val, p) && n.val >= 0
+}
+
+method my_unfold(n : Ref)
+    requires acc(n.val, 1/2) && greater0(n, 1/2)
+    ensures acc(n.val, 1/2) && n.val >= 0
+{
+    assert unfolding greater0(n, 1/2) in n.val >= 0
+}

src/test/resources/viperDebugger/sequences.vpr

@@ -0,0 +1,18 @@
+
+
+method test_sequence()
+{
+    var s : Seq[Int]
+    s := Seq(1,3,3)
+    var z : Int
+    z := s[1] + s[2]
+    assert z == 6
+}
+
+method test_sequence_append(s1 : Seq[Int], s2: Seq[Int])
+    requires |s1| > 0 && |s2| > 0
+{
+    var s : Seq[Int]
+    s := s1 ++ s2
+    assert |s| > 1
+}