Added back atomic_begin,_end, and a pass to remove them afterwards.

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java

@@ -743,6 +743,10 @@ public Expr<?> visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) {
     @Override
     public Expr<?> visitPrimaryExpressionId(CParser.PrimaryExpressionIdContext ctx) {
         final var variable = getVar(ctx.Identifier().getText());
+        if (atomicVars.contains(variable)) {
+            preStatements.add(new CCall("__VERIFIER_atomic_begin", List.of(), parseContext));
+            postStatements.add(new CCall("__VERIFIER_atomic_end", List.of(), parseContext));
+        }
         return variable.getRef();
     }
 
@@ -983,7 +987,7 @@ public Function<Expr<?>, Expr<?>> visitPostfixExpressionIncrement(
                 cexpr = new CExpr(expr, parseContext);
                 // no need to truncate here, as left and right side types are the same
                 CAssignment cAssignment = new CAssignment(primary, cexpr, "=", parseContext);
-                postStatements.add(cAssignment);
+                postStatements.add(0, cAssignment);
                 functionVisitor.recordMetadata(ctx, cAssignment);
                 functionVisitor.recordMetadata(ctx, cexpr);
                 return primary;
@@ -1004,7 +1008,7 @@ public Function<Expr<?>, Expr<?>> visitPostfixExpressionDecrement(
                 cexpr = new CExpr(expr, parseContext);
                 // no need to truncate here, as left and right side types are the same
                 CAssignment cAssignment = new CAssignment(primary, cexpr, "=", parseContext);
-                postStatements.add(cAssignment);
+                postStatements.add(0, cAssignment);
                 functionVisitor.recordMetadata(ctx, cAssignment);
                 functionVisitor.recordMetadata(ctx, cexpr);
                 return expr;

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt

@@ -70,6 +70,7 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningL
       UnusedLocRemovalPass(),
     ),
     listOf(FetchExecuteWriteback(parseContext)),
+    listOf(RemoveAtomics()),
   )
 
 class ChcPasses(parseContext: ParseContext, uniqueWarningLogger: Logger) :

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt

@@ -0,0 +1,51 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.xcfa.passes
+
+import hu.bme.mit.theta.xcfa.getFlatLabels
+import hu.bme.mit.theta.xcfa.model.FenceLabel
+import hu.bme.mit.theta.xcfa.model.SequenceLabel
+import hu.bme.mit.theta.xcfa.model.XcfaProcedureBuilder
+
+class RemoveAtomics : ProcedurePass {
+
+  override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder {
+    for (xcfaEdge in LinkedHashSet(builder.getEdges())) {
+      val labels = xcfaEdge.getFlatLabels()
+      val (beginIndex, beginLabel) =
+        labels
+          .mapIndexed { i1, i2 -> Pair(i1, i2) }
+          .firstOrNull {
+            it.second is FenceLabel && (it.second as FenceLabel).labels.contains("ATOMIC_BEGIN")
+          } ?: continue
+      val (endIndex, endLabel) =
+        labels
+          .mapIndexed { i1, i2 -> Pair(i1, i2) }
+          .lastOrNull {
+            it.second is FenceLabel && (it.second as FenceLabel).labels.contains("ATOMIC_END")
+          } ?: continue
+      val newLabels =
+        labels.subList(0, beginIndex) +
+          labels.subList(beginIndex + 1, endIndex).filter {
+            it !is FenceLabel || !it.labels.contains("ATOMIC_")
+          } +
+          labels.subList(endIndex + 1, labels.size)
+      builder.removeEdge(xcfaEdge)
+      builder.addEdge(xcfaEdge.withLabel(SequenceLabel(newLabels)))
+    }
+    return builder
+  }
+}