From e53952f1055566876edb5cfa37a732cf9acf32e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Fri, 17 Jan 2025 12:30:00 +0100
Subject: [PATCH] add better config options

---
 src/main/scala/viper/gobra/frontend/Config.scala | 5 +++--
 src/test/scala/viper/gobra/GobraTests.scala      | 5 +++++
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala
index b98a2aafc..566986001 100644
--- 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
index 9de0ce90d..dbbbbdc3b 100644
--- 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 = {