Api -> API

viperproject · Jul 28, 2023 · 8844584 · 8844584
1 parent 45b7df4
commit 8844584
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 13 deletions.
diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala
@@ -28,7 +28,7 @@ object ViperBackends {
       if (config.conditionalizePermissions) {
         options ++= Vector("--conditionalizePermissions")
       }
-      if (config.z3ApiMode) {
+      if (config.z3APIMode) {
         options = options ++ Vector(s"--prover ${Z3ProverAPI.name}")
       }
       val mceSiliconOpt = config.mceMode match {

diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala
@@ -65,7 +65,7 @@ object ConfigDefaults {
   lazy val DefaultAssumeInjectivityOnInhale: Boolean = true
   lazy val DefaultParallelizeBranches: Boolean = false
   lazy val DefaultConditionalizePermissions: Boolean = false
-  lazy val DefaultZ3ApiMode: Boolean = false
+  lazy val DefaultZ3APIMode: Boolean = false
   lazy val DefaultMCEMode: MCE.Mode = MCE.Enabled
   lazy val DefaultEnableLazyImports: Boolean = false
   lazy val DefaultNoVerify: Boolean = false
@@ -128,7 +128,7 @@ case class Config(
                    // branches will be verified in parallel
                    parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches,
                    conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions,
-                   z3ApiMode: Boolean = ConfigDefaults.DefaultZ3ApiMode,
+                   z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode,
                    mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode,
                    enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                    noVerify: Boolean = ConfigDefaults.DefaultNoVerify,
@@ -176,7 +176,7 @@ case class Config(
       assumeInjectivityOnInhale = assumeInjectivityOnInhale || other.assumeInjectivityOnInhale,
       parallelizeBranches = parallelizeBranches,
       conditionalizePermissions = conditionalizePermissions,
-      z3ApiMode = z3ApiMode || other.z3ApiMode,
+      z3APIMode = z3APIMode || other.z3APIMode,
       mceMode = mceMode,
       enableLazyImports = enableLazyImports || other.enableLazyImports,
       noVerify = noVerify || other.noVerify,
@@ -228,7 +228,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       assumeInjectivityOnInhale: Boolean = ConfigDefaults.DefaultAssumeInjectivityOnInhale,
                       parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches,
                       conditionalizePermissions: Boolean = ConfigDefaults.DefaultConditionalizePermissions,
-                      z3ApiMode: Boolean = ConfigDefaults.DefaultZ3ApiMode,
+                      z3APIMode: Boolean = ConfigDefaults.DefaultZ3APIMode,
                       mceMode: MCE.Mode = ConfigDefaults.DefaultMCEMode,
                       enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                       noVerify: Boolean = ConfigDefaults.DefaultNoVerify,
@@ -284,7 +284,7 @@ trait RawConfig {
     assumeInjectivityOnInhale = baseConfig.assumeInjectivityOnInhale,
     parallelizeBranches = baseConfig.parallelizeBranches,
     conditionalizePermissions = baseConfig.conditionalizePermissions,
-    z3ApiMode = baseConfig.z3ApiMode,
+    z3APIMode = baseConfig.z3APIMode,
     mceMode = baseConfig.mceMode,
     enableLazyImports = baseConfig.enableLazyImports,
     noVerify = baseConfig.noVerify,
@@ -633,10 +633,10 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     short = 'c',
   )
 
-  val z3ApiMode: ScallopOption[Boolean] = opt[Boolean](
-    name = "z3ApiMode",
+  val z3APIMode: ScallopOption[Boolean] = opt[Boolean](
+    name = "z3APIMode",
     descr = "When the backend is either SILICON or VSWITHSILICON, silicon will use Z3 via API.",
-    default = Some(ConfigDefaults.DefaultZ3ApiMode),
+    default = Some(ConfigDefaults.DefaultZ3APIMode),
     noshort = true,
   )
 
@@ -739,9 +739,9 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
   }
 
   addValidation {
-    val z3ApiModeOn = z3ApiMode.toOption.contains(true)
-    if (z3ApiModeOn && !isSiliconBasedBackend) {
-      Left("The selected backend does not support --z3ApiMode.")
+    val z3APIModeOn = z3APIMode.toOption.contains(true)
+    if (z3APIModeOn && !isSiliconBasedBackend) {
+      Left("The selected backend does not support --z3APIMode.")
     } else {
       Right(())
     }
@@ -843,7 +843,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     assumeInjectivityOnInhale = assumeInjectivityOnInhale(),
     parallelizeBranches = parallelizeBranches(),
     conditionalizePermissions = conditionalizePermissions(),
-    z3ApiMode = z3ApiMode(),
+    z3APIMode = z3APIMode(),
     mceMode = mceMode(),
     enableLazyImports = enableLazyImports(),
     noVerify = noVerify(),