Throwing error when encountering #pragmas

ftsrg · Nov 22, 2023 · 7f5c7d2 · 7f5c7d2
1 parent d492a1f
commit 7f5c7d2
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git 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
@@ -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<String>) {
                             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
                         }
-Original file line number
+Diff line change
@@ Expand Up / @@ -933,7 +933,6 @@ LineDirective @@
     PragmaDirective
         :   '#' Whitespace? 'pragma' Whitespace ~[\r\n]*
-            -> skip
         ;
     Whitespace
@@ Expand Down @@