Ensure atomic blocks in CHandler::makeAssignment

ultimate-pa · Oct 21, 2024 · 52f4372 · 52f4372
1 parent 5cfe192
commit 52f4372
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/...src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java b/...src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java
@@ -130,6 +130,7 @@
 import de.uni_freiburg.informatik.ultimate.boogie.annotation.LTLPropertyCheck.CheckableExpression;
 import de.uni_freiburg.informatik.ultimate.boogie.ast.ASTType;
 import de.uni_freiburg.informatik.ultimate.boogie.ast.AssignmentStatement;
+import de.uni_freiburg.informatik.ultimate.boogie.ast.AtomicStatement;
 import de.uni_freiburg.informatik.ultimate.boogie.ast.Attribute;
 import de.uni_freiburg.informatik.ultimate.boogie.ast.Axiom;
 import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression;
@@ -2850,7 +2851,11 @@ public ExpressionResult makeAssignment(final ILocation loc, final LRValue leftHa
 		final AssignmentStatement assignStmt = StatementFactory.constructAssignmentStatement(loc,
 				new LeftHandSide[] { lValue.getLhs() }, new Expression[] { rhsWithBitfieldTreatment });
 
-		builder.addStatement(assignStmt);
+		if (leftHandSide.getCType().isAtomic()) {
+			builder.addStatement(new AtomicStatement(loc, new Statement[] { assignStmt }));
+		} else {
+			builder.addStatement(assignStmt);
+		}
 
 		for (final Overapprox oa : rhsConverted.getOverapprs()) {
 			new OverapproxVariable(oa.getOverapproximatedLocations()).annotate(assignStmt);