From 7f5c7d2c4cb53bdbdaaea0939a87dfd82dd975ea Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Wed, 22 Nov 2023 22:24:10 +0100 Subject: [PATCH] Throwing error when encountering #pragmas --- subprojects/frontends/c-frontend/src/main/antlr/C.g4 | 1 - .../src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 5 ++++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/subprojects/frontends/c-frontend/src/main/antlr/C.g4 b/subprojects/frontends/c-frontend/src/main/antlr/C.g4 index e8cb557d48..3f0eac318b 100644 --- a/subprojects/frontends/c-frontend/src/main/antlr/C.g4 +++ b/subprojects/frontends/c-frontend/src/main/antlr/C.g4 @@ -933,7 +933,6 @@ LineDirective PragmaDirective : '#' Whitespace? 'pragma' Whitespace ~[\r\n]* - -> skip ; Whitespace diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt index c142862f49..8491a1346e 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt @@ -45,6 +45,7 @@ import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.frontend.chc.ChcFrontend import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.ArithmeticType +import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.ArithmeticTrait import hu.bme.mit.theta.llvm2xcfa.XcfaUtils.fromFile import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager import hu.bme.mit.theta.xcfa.analysis.ErrorDetection @@ -471,8 +472,10 @@ class XcfaCli(private val args: Array) { parseContext.arithmetic = ArchitectureConfig.ArithmeticType.bitvector logger.write(Logger.Level.INFO, "Retrying parsing with bitvector arithmetic...\n") val stream = FileInputStream(input!!) - getXcfaFromC(stream, parseContext, false, + val xcfa = getXcfaFromC(stream, parseContext, false, explicitProperty == ErrorDetection.OVERFLOW, uniqueWarningLogger).first + parseContext.arithmeticTraits.add(ArithmeticTrait.BITWISE) + xcfa } else { throw e }