Assert-read-only function preconditions

viperproject · Oct 13, 2024 · f49fee0 · f49fee0
1 parent 53ecf55
commit f49fee0
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 13 deletions.
diff --git a/silver b/silver
diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -1526,27 +1526,21 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                            v: Verifier)
                           : ConsumptionResult = {
 
-    var success = false
     var permsAvailable: Term = NoPerm
     var permsAvailableExp: Option[ast.Exp] = Option.when(withExp)(ast.NoPerm()())
 
-    var tookEnoughCheck: Term = False
 
     for (ch <- candidates) {
-      if (!success) {
-        permsAvailable = PermPlus(permsAvailable, ch.perm)
-        permsAvailableExp = permsAvailableExp.map(pae => ast.PermAdd(pae, permsExp.get)())
-
-        tookEnoughCheck =
-          Forall(codomainQVars, Implies(condition, Implies(Greater(perms, NoPerm), Greater(permsAvailable, NoPerm))), Nil)
-
-        success = v.decider.check(tookEnoughCheck, Verifier.config.splitTimeout())
-      }
+      permsAvailable = PermPlus(permsAvailable, ch.perm)
+      permsAvailableExp = permsAvailableExp.map(pae => ast.PermAdd(pae, permsExp.get)())
     }
 
+    val tookEnoughCheck =
+      Forall(codomainQVars, Implies(condition, Implies(Greater(perms, NoPerm), Greater(permsAvailable, NoPerm))), Nil)
+
     // final check
     val result =
-      if (success || v.decider.check(tookEnoughCheck, Verifier.config.assertTimeout.getOrElse(0)) /* This check is a must-check, i.e. an assert */ )
+      if (v.decider.check(tookEnoughCheck, Verifier.config.assertTimeout.getOrElse(0)) /* This check is a must-check, i.e. an assert */ )
         Complete()
       else
         Incomplete(PermMinus(permsAvailable, perms), permsAvailableExp.map(pa => ast.PermSub(pa, permsExp.get)()))
+300 −0		src/test/resources/all/functions/function_precondition_perms.vpr
+8 −8		src/test/resources/all/issues/carbon/0196.vpr
+1 −1		src/test/resources/all/issues/carbon/0223.vpr
+2 −9		src/test/resources/all/issues/silicon/0030.vpr
+5 −5		src/test/resources/all/issues/silicon/0240.vpr
+1 −0		src/test/resources/all/issues/silicon/0376.vpr