reduces diff by undoing some unnecessary changes

Author: ArquintL

src/main/scala/viper/gobra/Gobra.scala

@@ -298,7 +298,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     // can be found by the well-formedness checks.
     val startMs = System.currentTimeMillis()
     var transformations: Vector[InternalTransform] = Vector(CGEdgesTerminationTransform, ConstantPropagation)
-    if (config.checkOverflowsOrDefault) {
+    if (config.checkOverflows) {
       transformations :+= OverflowChecksTransform
     }
     val result = transformations.foldLeft(program)((prog, transf) => transf.transform(prog))

src/main/scala/viper/gobra/backend/ViperBackends.scala

@@ -25,7 +25,7 @@ trait ViperBackend extends CliEnumConverter.EnumCase {
     var options: Vector[String] = Vector.empty
 
     options ++= exePaths
-    if (config.assumeInjectivityOnInhaleOrDefault) {
+    if (config.assumeInjectivityOnInhale) {
       options ++= Vector("--assumeInjectivityOnInhale")
     }
     if (config.respectFunctionPrePermAmounts) {
@@ -48,16 +48,16 @@ trait SiliconBasedBackend extends ViperBackend {
     var options: Vector[String] = super.buildOptions(exePaths, config)
     options ++= Vector("--logLevel", "ERROR")
     options ++= Vector("--disableCatchingExceptions")
-    if (config.conditionalizePermissionsOrDefault) {
+    if (config.conditionalizePermissions) {
       options ++= Vector("--conditionalizePermissions")
     }
-    if (config.z3APIModeOrDefault) {
+    if (config.z3APIMode) {
       options ++= Vector(s"--prover=${Z3ProverAPI.name}")
     }
-    if (config.disableNLOrDefault) {
+    if (config.disableNL) {
       options ++= Vector(s"--disableNL")
     }
-    if (config.unsafeWildcardOptimizationOrDefault) {
+    if (config.unsafeWildcardOptimization) {
       options ++= Vector(s"--unsafeWildcardOptimization")
     }
     options ++= Vector(s"--moreJoins=${config.moreJoins.viperValue}")
@@ -70,10 +70,10 @@ trait SiliconBasedBackend extends ViperBackend {
     // Gobra seems to be much slower with the new silicon axiomatization of collections.
     // For now, we stick to the old one.
     options ++= Vector("--useOldAxiomatization")
-    if (config.parallelizeBranchesOrDefault) {
+    if (config.parallelizeBranches) {
       options ++= Vector("--parallelizeBranches")
     }
-    if (config.disableSetAxiomatizationOrDefault) {
+    if (config.disableSetAxiomatization) {
       // Since resources are stored within the .jar archive, we cannot
       // directly pass the axiom file to Silicon.
       val tmpPath = Paths.get("gobra_tmp")

src/main/scala/viper/gobra/frontend/Config.scala

@@ -94,7 +94,7 @@ object PackageResolver {
     for {
       // pkgDir stores the path to the directory that should contain source files belonging to the desired package
       pkgDir <- getLookupPath(importTarget)(config)
-      sourceFiles = getSourceFiles(pkgDir, onlyFilesWithHeader = config.onlyFilesWithHeaderOrDefault)
+      sourceFiles = getSourceFiles(pkgDir, onlyFilesWithHeader = config.onlyFilesWithHeader)
       // check whether all found source files belong to the same package (the name used in the package clause can
       // be absolutely independent of the import path)
       // in case of error, iterate over all resources and close them

src/main/scala/viper/gobra/frontend/PackageResolver.scala

@@ -235,7 +235,7 @@ object Info extends LazyLogging {
       .mkString("")
     val isMainContextKey = if (isMainContext) "1" else "0"
     val configKey = config.typeBounds.hashCode().toString ++
-      (if (config.int32bitOrDefault) "1" else "0")
+      (if (config.int32bit) "1" else "0")
 
     val key = pkgKey ++
       dependentTypeInfoKey ++

src/main/scala/viper/gobra/frontend/info/Info.scala

@@ -55,7 +55,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       // check that the quantifier `body` is either Boolean or an assertion
       assignableToSpec(body) ++
       // check that the user provided triggers when running with --requireTriggers
-      error(n, "found a quantifier without triggers.", config.requireTriggersOrDefault && triggers.isEmpty)
+      error(n, "found a quantifier without triggers.", config.requireTriggers && triggers.isEmpty)
 
     case n@PExists(vars, triggers, body) =>
       val mayInit = isEnclosingMayInit(n)
@@ -64,7 +64,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       // check that the quantifier `body` is Boolean
       assignableToSpec(body) ++ assignableTo.errors(exprType(body), BooleanT, mayInit)(expr) ++
       // check that the user provided triggers when running with --requireTriggers
-      error(n, "found a quantifier without triggers.", config.requireTriggersOrDefault && triggers.isEmpty)
+      error(n, "found a quantifier without triggers.", config.requireTriggers && triggers.isEmpty)
 
     case n: PImplication =>
       val mayInit = isEnclosingMayInit(n)

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala

@@ -36,7 +36,7 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
     }
     val hasMeasureIfNeeded =
       if (spec.isPure || isEnclosingGhost(member))
-        config.disableCheckTerminationPureFnsOrDefault || spec.terminationMeasures.nonEmpty
+        config.disableCheckTerminationPureFns || spec.terminationMeasures.nonEmpty
       else
         true
     val needsMeasureError =

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala

@@ -51,7 +51,7 @@ object Translator {
       case (errs, _) => errs
     }
 
-    if (config.checkConsistencyOrDefault) {
+    if (config.checkConsistency) {
       transformedTask
         .flatMap(task => {
           val consistencyErrs = task.program.checkTransitively

src/main/scala/viper/gobra/translator/Translator.scala

@@ -128,7 +128,7 @@ class DetailedBenchmarkTests extends BenchmarkTests {
       val c = config.get
       assert(c.packageInfoInputMap.size == 1)
       val pkgInfo = c.packageInfoInputMap.keys.head
-      if (c.checkOverflowsOrDefault) {
+      if (c.checkOverflows) {
         val result = OverflowChecksTransform.transform(program)
         c.reporter report AppliedInternalTransformsMessage(c.packageInfoInputMap(pkgInfo).map(_.name), () => result)
         Right(result)

src/test/scala/viper/gobra/DetailedBenchmarkTests.scala

@@ -76,7 +76,7 @@ class GobraPackageTests extends GobraTests {
           reporter = NoopReporter,
           packageInfoInputMap = Map(pkgInfo -> input.files.toVector.map(FromFileSource(_))),
           includeDirs = Vector(currentDir),
-          checkConsistency = Some(true),
+          checkConsistency = true,
           z3Exe = z3Exe
         )