Merge pull request #308 from ftsrg/fix-ref

Fixed variable naming in ReferenceElimination
ftsrg · Nov 3, 2024 · 1e09cf6 · 1e09cf6
2 parents da9aadc + f699d1b
commit 1e09cf6
Show file tree

Hide file tree

Showing 5 changed files with 234 additions and 139 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.6.5"
+    version = "6.6.6"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt
@@ -18,6 +18,7 @@
 package hu.bme.mit.theta.c2xcfa
 
 import com.google.common.base.Preconditions
+import com.google.common.base.Preconditions.checkState
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.core.decl.Decls
 import hu.bme.mit.theta.core.decl.VarDecl
@@ -52,7 +53,6 @@ import hu.bme.mit.theta.xcfa.model.*
 import hu.bme.mit.theta.xcfa.passes.CPasses
 import java.math.BigInteger
 import java.util.stream.Collectors
-import org.abego.treelayout.internal.util.Contract.checkState
 
 class FrontendXcfaBuilder(
   val parseContext: ParseContext,

diff --git a/...cts/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt b/...cts/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToHornChecker.kt
@@ -15,6 +15,7 @@
  */
 package hu.bme.mit.theta.xcfa.cli.checkers
 
+import com.google.common.base.Preconditions.checkState
 import hu.bme.mit.theta.analysis.Trace
 import hu.bme.mit.theta.analysis.algorithm.EmptyProof
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker
@@ -33,7 +34,6 @@ import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig
 import hu.bme.mit.theta.xcfa.cli.utils.getSolver
 import hu.bme.mit.theta.xcfa.model.XCFA
 import hu.bme.mit.theta.xcfa2chc.toCHC
-import org.abego.treelayout.internal.util.Contract.checkState
 
 fun getHornChecker(
   xcfa: XCFA,

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MallocFunctionPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MallocFunctionPass.kt
@@ -15,6 +15,7 @@
  */
 package hu.bme.mit.theta.xcfa.passes
 
+import com.google.common.base.Preconditions.checkState
 import hu.bme.mit.theta.core.decl.Decls.Var
 import hu.bme.mit.theta.core.decl.VarDecl
 import hu.bme.mit.theta.core.stmt.AssignStmt
@@ -27,7 +28,6 @@ import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer
 import hu.bme.mit.theta.xcfa.getFlatLabels
 import hu.bme.mit.theta.xcfa.model.*
-import org.abego.treelayout.internal.util.Contract.checkState
 
 /**
  * Transforms mallocs into address assignments. Requires the ProcedureBuilder be `deterministic`.