From cd102e8763a92610d3daf39560c1a3abb5674b22 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Tue, 12 Nov 2024 12:26:05 +0100
Subject: [PATCH] noDataRaceWhenPtr

---
 .../mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt    | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt
index 25a81fdb2e..c8768cb67c 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt
+++ b/subprojects/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,