noDataRaceWhenPtr

ftsrg · Nov 12, 2024 · cd102e8 · cd102e8
1 parent 0d4e531
commit cd102e8
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/...ts/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt b/...ts/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt
@@ -40,6 +40,7 @@ import hu.bme.mit.theta.xcfa.analysis.*
 import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts
 import hu.bme.mit.theta.xcfa.cli.params.*
 import hu.bme.mit.theta.xcfa.cli.utils.getSolver
+import hu.bme.mit.theta.xcfa.dereferences
 import hu.bme.mit.theta.xcfa.model.XCFA
 
 fun getCegarChecker(
@@ -53,6 +54,12 @@ fun getCegarChecker(
   XcfaPrec<*>,
 > {
   val cegarConfig = config.backendConfig.specConfig as CegarConfig
+  if (
+    config.inputConfig.property == ErrorDetection.DATA_RACE &&
+      xcfa.procedures.any { it.edges.any { it.label.dereferences.isNotEmpty() } }
+  ) {
+    throw RuntimeException("DATA_RACE cannot be checked when pointers exist in the file.")
+  }
   val abstractionSolverFactory: SolverFactory =
     getSolver(
       cegarConfig.abstractorConfig.abstractionSolver,