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,