Merge pull request viperproject#526 from viperproject/meilers_adapt_t…

…oString_val Adapting to Silver change
viper-admin · Sep 1, 2024 · ebbdf60 · ebbdf60
2 parents 759f3c1 + 70011aa
commit ebbdf60
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 10 deletions.
diff --git a/silver b/silver
diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala
@@ -601,7 +601,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
 
           val triggers = if (locationAccess.exists(lvds.toSet)) Seq(Trigger(Seq(locationAccess1,locationAccess2))) else Seq() // TODO: we could (also in general) raise an error/warning if the tools fail to find triggers
 
-          val res = CommentedDecl("Function used for framing of quantified permission " + qp.toString() +  " in " + originalName,
+          val res = CommentedDecl("Function used for framing of quantified permission " + qp.toString +  " in " + originalName,
             condFunc ++
             Axiom(
               Forall(heap1 ++ heap2 ++ origArgs, Seq(Trigger(Seq(funApp1, funApp2, heapModule.successorHeapState(heap1,heap2)))),

diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala
@@ -328,13 +328,13 @@ DefaultWandModule(val verifier: Verifier) extends WandModule with StmtComponent
         UNIONState = OPS
         val StateSetup(usedState, initStmt) = createAndSetState(None)
         tempCurState = usedState
-        Comment("Translating exec of non-ghost operation" + e.toString()) ++
+        Comment("Translating exec of non-ghost operation" + e.toString) ++
         initStmt ++  exhaleExt(ops :: states, usedState,e,ops.boolVar&&allStateAssms, RHS = true, mainError)
     }
   }
 
 override def exhaleExt(statesObj: List[Any], usedObj:Any, e: sil.Exp, allStateAssms: Exp, RHS: Boolean = false, error: PartialVerificationError, havocHeap: Boolean):Stmt = {
-  Comment("exhale_ext of " + e.toString())
+  Comment("exhale_ext of " + e.toString)
   val states = statesObj.asInstanceOf[List[StateRep]]
   val used = usedObj.asInstanceOf[StateRep]
   e match {
@@ -391,7 +391,7 @@ def transferMain(states: List[StateRep], used:StateRep, e: sil.Exp, allStateAssm
 
   val unionStmt = updateUnion()
 
-  MaybeCommentBlock("Transfer of " + e.toString(), stmt ++ unionStmt)
+  MaybeCommentBlock("Transfer of " + e.toString, stmt ++ unionStmt)
 
 }
 

diff --git a/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala b/src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala
@@ -611,9 +611,9 @@ class QuantifiedPermModule(val verifier: Verifier)
               MaybeComment("wild card assumptions", stmts ++
               wildcardAssms) ++
               CommentBlock("check that the permission amount is positive", permPositive) ++
-              CommentBlock("check if receiver " + recv.toString() + " is injective",injectiveAssertion) ++
+              CommentBlock("check if receiver " + recv.toString + " is injective",injectiveAssertion) ++
               CommentBlock("check if sufficient permission is held", enoughPerm) ++
-              CommentBlock("assumptions for inverse of receiver " + recv.toString(), Assume(invAssm1)++ Assume(invAssm2)) ++
+              CommentBlock("assumptions for inverse of receiver " + recv.toString, Assume(invAssm1)++ Assume(invAssm2)) ++
               CommentBlock("assume permission updates for field " + f.name, Assume(Forall(obj,triggersForPermissionUpdateAxiom, condTrueLocations && condFalseLocations ))) ++
               CommentBlock("assume permission updates for independent locations", independentLocations) ++
               (mask := qpMask)
@@ -803,9 +803,9 @@ class QuantifiedPermModule(val verifier: Verifier)
               MaybeComment("wildcard assumptions", stmts ++
               wildcardAssms) ++
               CommentBlock("check that the permission amount is positive", permPositive) ++
-              CommentBlock("check if receiver " + accPred.toString() + " is injective",injectiveAssertion) ++
+              CommentBlock("check if receiver " + accPred.toString + " is injective",injectiveAssertion) ++
               CommentBlock("check if sufficient permission is held", enoughPerm) ++
-              CommentBlock("assumptions for inverse of receiver " + accPred.toString(), Assume(invAssm1)++ Assume(invAssm2)) ++
+              CommentBlock("assumptions for inverse of receiver " + accPred.toString, Assume(invAssm1)++ Assume(invAssm2)) ++
               CommentBlock("assume permission updates", permissionsMap ++
               independentResource) ++
               CommentBlock("assume permission updates for independent locations ", independentLocations) ++
@@ -1349,7 +1349,7 @@ class QuantifiedPermModule(val verifier: Verifier)
 
            val res1 = Havoc(qpMask) ++
              stmts ++
-             (if (!verifier.assumeInjectivityOnInhale) CommentBlock("check if receiver " + accPred.toString() + " is injective",injectiveAssertion)
+             (if (!verifier.assumeInjectivityOnInhale) CommentBlock("check if receiver " + accPred.toString + " is injective",injectiveAssertion)
              else Nil) ++
              CommentBlock("Define Inverse Function", Assume(invAssm1) ++
                Assume(invAssm2)) ++