Checking only read permissions when asserting function preconditions

src/main/scala/viper/carbon/CarbonVerifier.scala

@@ -94,6 +94,12 @@ case class CarbonVerifier(override val reporter: Reporter,
   }
   else false
 
+  def respectFunctionPrecPermAmounts: Boolean = if (config != null) config.respectFunctionPrePermAmounts.toOption match {
+    case Some(b) => b
+    case None => false
+  }
+  else false
+
   override def usePolyMapsInEncoding =
     if (config != null) {
       config.desugarPolymorphicMaps.toOption match {

src/main/scala/viper/carbon/modules/PermModule.scala

@@ -159,4 +159,8 @@ trait PermModule extends Module with CarbonStateComponent {
   // removes permission to w#ft (footprint of the magic wand) (See Heap module for w#ft description)
   def exhaleWandFt(w: sil.MagicWand): Stmt
 
+  def setCheckReadPermissionOnlyState(readOnly: Boolean): Boolean
+
+  def assumePermUpperBounds: Stmt
+
 }

src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala

@@ -79,6 +79,7 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
       case sil.Unfolding(_, exp) =>
         translateExp(exp)
       case sil.Applying(_, exp) => translateExp(exp)
+      case sil.Asserting(_, exp) => translateExp(exp)
       case sil.Old(exp) =>
         val prevState = stateModule.state
         stateModule.replaceState(stateModule.oldState)
@@ -378,6 +379,13 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
         checkDefinednessImpl(e1, error, makeChecks = makeChecks, definednessStateOpt) :: // short-circuiting evaluation:
           If(UnExp(Not, translateExp(e1)), checkDefinednessImpl(e2, error, makeChecks = makeChecks, definednessStateOpt), Statements.EmptyStmt) ::
           Nil
+      case sil.Asserting(assertion, e) =>
+        val checkAssDefined = checkDefinedness(assertion, error, makeChecks = makeChecks)
+        val (stateStmt, state) = stateModule.freshTempState("asserting")
+        val checkAssHolds = MaybeComment("Exhale assertion of asserting", exhale(Seq((assertion, error, Some(error)))))
+        stateModule.replaceState(state)
+        val checkEDefined = checkDefinedness(e, error, makeChecks = makeChecks)
+        checkAssDefined :: stateStmt :: checkAssHolds :: checkEDefined :: Nil
       case w@sil.MagicWand(_, _) =>
         checkDefinednessWand(w, error, makeChecks = makeChecks)
       case sil.Let(v, e, body) =>

src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala

@@ -190,6 +190,8 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     override def translateFunction(f: sil.Function, names: Option[mutable.Map[String, String]]): Seq[Decl] = {
     env = Environment(verifier, f)
     ErrorMemberMapping.currentMember = f
+
+    val oldPermOnlyState = permModule.setCheckReadPermissionOnlyState(!verifier.respectFunctionPrecPermAmounts)
     val res = MaybeCommentedDecl(s"Translation of function ${f.name}",
       MaybeCommentedDecl("Uninterpreted function definitions", functionDefinitions(f), size = 1) ++
         (if (f.isAbstract) Nil else
@@ -207,6 +209,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
       names.get ++= usedNames
     }
 
+    permModule.setCheckReadPermissionOnlyState(oldPermOnlyState)
     env = null
     ErrorMemberMapping.currentMember = null
     res
@@ -665,7 +668,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
 
     val args = p.formalArgs map translateLocalVarDecl
     val init : Stmt = MaybeCommentBlock("Initializing the state",
-      stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ (p.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true)))
+      stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ permModule.assumePermUpperBounds ++ (p.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true)))
     )
 
     val predicateBody = p.body.get
@@ -871,12 +874,17 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
                     * contain permission introspection.
                     */
                   val curState = stateModule.state
+                  val oldReadState = permModule.setCheckReadPermissionOnlyState(true)
                   defState.setDefState()
                   val res = executeExhale()
+                  permModule.setCheckReadPermissionOnlyState(oldReadState)
                   stateModule.replaceState(curState)
                   res
                 case None =>
-                  executeExhale()
+                  val oldReadState = permModule.setCheckReadPermissionOnlyState(true)
+                  val res = executeExhale()
+                  permModule.setCheckReadPermissionOnlyState(oldReadState)
+                  res
               }
             }
           ) ++
@@ -961,7 +969,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
             wandModule.translatingStmtsInWandInit()
           }
           (checkDefinedness(acc, errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++
-            checkDefinedness(perm, errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++
+            checkDefinedness(perm.getOrElse(sil.FullPerm()()), errors.FoldFailed(fold), insidePackageStmt = insidePackageStmt) ++
             foldFirst, foldLast)
         }
       }
@@ -998,7 +1006,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     unfold match {
       case sil.Unfold(acc@sil.PredicateAccessPredicate(pa@sil.PredicateAccess(_, _), perm)) =>
         checkDefinedness(acc, errors.UnfoldFailed(unfold), insidePackageStmt = insidePackageStmt) ++
-          checkDefinedness(perm, errors.UnfoldFailed(unfold)) ++
+          checkDefinedness(perm.getOrElse(sil.FullPerm()()), errors.UnfoldFailed(unfold)) ++
           unfoldPredicate(acc, errors.UnfoldFailed(unfold), false, statesStackForPackageStmt, insidePackageStmt)
     }
   }

src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala

@@ -137,7 +137,7 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles
             val initOldStateComment = "Initializing of old state"
             val ins: Seq[LocalVarDecl] = formalArgs map translateLocalVarDecl
             val outs: Seq[LocalVarDecl] = formalReturns map translateLocalVarDecl
-            val init = MaybeCommentBlock("Initializing the state", stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ stmtModule.initStmt(method.bodyOrAssumeFalse))
+            val init = MaybeCommentBlock("Initializing the state", stateModule.initBoogieState ++ assumeAllFunctionDefinitions ++ permModule.assumePermUpperBounds ++ stmtModule.initStmt(method.bodyOrAssumeFalse))
             val initOld = MaybeCommentBlock("Initializing the old state", stateModule.initOldState)
             val paramAssumptions = mWithLoopInfo.formalArgs map (a => allAssumptionsAboutValue(a.typ, translateLocalVarDecl(a), true))
             val inhalePre = translateMethodDeclPre(pres)
@@ -269,9 +269,9 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles
     val resourceCurPerm =
       q.exp match {
         case r : sil.FieldAccess =>
-          sil.FieldAccessPredicate(r, curPermVar)()
+          sil.FieldAccessPredicate(r, Some(curPermVar))()
         case r: sil.PredicateAccess =>
-          sil.PredicateAccessPredicate(r, curPermVar)()
+          sil.PredicateAccessPredicate(r, Some(curPermVar))()
         case _ => sys.error("Not supported resource in quasihavoc")
       }