add better config options

viperproject · Jan 17, 2025 · e53952f · e53952f
1 parent ecdfeef
commit e53952f
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala
@@ -775,11 +775,12 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     }
   }
 
-  val respectFunctionPrePermAmounts: ScallopOption[Boolean] = opt[Boolean](
+  val respectFunctionPrePermAmounts: ScallopOption[Boolean] = toggle(
     name = "respectFunctionPrePermAmounts",
-    descr = s"Respects precise permission amounts in function preconditions instead of only checking read access, as done in older versions of Gobra." +
+    descrYes = s"Respects precise permission amounts in pure function preconditions instead of only checking read access, as done in older versions of Gobra." +
       "This option should be used for verifying legacy projects written with the old interpretation of fractional permissions." +
       "New projects are encouraged to not use this flag.",
+    descrNo = s"Use the default interpretation for fractional permissions in pure function preconditions.",
     default = Some(ConfigDefaults.DefaultRespectFunctionPrePermAmounts),
     noshort = true,
   )

diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala
@@ -59,6 +59,11 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
       // termination checks in functions are currently disabled in the tests. This can be enabled in the future,
       // but requires some work to add termination measures all over the test suite.
       disableCheckTerminationPureFns = true,
+      // for the time being, we run the tests against the old semantics for fractional perms in pure function
+      // preconditions, as most tests were still written with the old semantics in mind. Furthermore, it is still
+      // more important to guarantee that there are no regressions in the old behaviour, as our pre-existing verified
+      // codebases use those semantics. In the future, we should deprecate the old semantics and change this to false.
+      respectFunctionPrePermAmounts = true,
     )
 
   override def runTests(testName: Option[String], args: Args): Status = {