fix instrumentation of location invariants at labels

trunk/examples/witness-checking/regression/sequential/correctness/many-labels.c

@@ -0,0 +1,32 @@
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+extern int __VERIFIER_nondet_int();
+void reach_error() { __assert_fail("0", "many-labels.c", 3, "reach_error"); }
+
+int main() {
+  int x = __VERIFIER_nondet_int();
+  if (x < 0) {
+    return;
+  }
+
+  if (x == -8) {
+    goto LABEL_A;
+  }
+  if (x == -16) {
+    goto LABEL_B;
+  }
+  if (x == -32) {
+    goto LABEL_C;
+  }
+  if (x == -64) {
+    goto LABEL_D;
+  }
+  return (0);
+
+  LABEL_A:
+  LABEL_B:
+  LABEL_C:
+  LABEL_D: {reach_error();abort();}
+  return (-1);
+}
+

trunk/examples/witness-checking/regression/sequential/correctness/many-labels.c-witness_v01.yaml

@@ -0,0 +1,25 @@
+- entry_type: location_invariant
+  metadata:
+    format_version: '0.1'
+    uuid: 386b0121-a302-415f-af28-bf0db7c36d11
+    creation_time: '2024-09-07T13:26:54+01:00'
+    producer:
+      name: UNUSED
+      version: 0.2.4-dev-25b2402-m
+    task:
+      input_files:
+      - C:\ultimate\trunk\examples\witness-checking\regression\correctness\many-labels.c
+      input_file_hashes:
+        C:\ultimate\trunk\examples\witness-checking\regression\correctness\many-labels.c: UNUSED
+      specification: UNUSED
+      data_model: UNUSED
+      language: C
+  location:
+    file_name: C:\ultimate\trunk\examples\witness-checking\regression\correctness\many-labels.c
+    file_hash: UNUSED
+    line: 29
+    function: main
+  location_invariant:
+    string: '0'
+    type: assertion
+    format: C

trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/ExtractedLocationInvariant.java

@@ -28,10 +28,12 @@
 package de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.witness;
 
 import java.util.List;
+import java.util.stream.Collectors;
 
 import org.eclipse.cdt.core.dom.ast.IASTNode;
 
 import de.uni_freiburg.informatik.ultimate.boogie.ast.AtomicStatement;
+import de.uni_freiburg.informatik.ultimate.boogie.ast.Label;
 import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement;
 import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.IDispatcher;
 import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.ExpressionResult;
@@ -60,15 +62,23 @@ public boolean isBefore() {
 	public ExpressionResult transform(final ILocation loc, final IDispatcher dispatcher,
 			final ExpressionResult expressionResult) {
 		final ExpressionResult invariantExprResult = instrument(loc, dispatcher);
+		final ExpressionResultBuilder erb =
+				new ExpressionResultBuilder(expressionResult).addAllExceptLrValueAndStatements(invariantExprResult);
+
 		// Make sure that the location invariant (incl. all auxiliary statements) is executed atomically.
 		final Statement invariant =
 				new AtomicStatement(loc, invariantExprResult.getStatements().toArray(Statement[]::new));
+
+		// Insert the location invariant at the appropriate location.
 		if (mIsBefore) {
-			return new ExpressionResultBuilder(invariantExprResult).resetStatements(List.of(invariant))
-					.addAllIncludingLrValue(expressionResult).build();
+			// Push location invariants after leading labels, if there are any.
+			final var statements = expressionResult.getStatements();
+			final List<Statement> labels =
+					statements.stream().takeWhile(Label.class::isInstance).collect(Collectors.toList());
+			final List<Statement> remainder = statements.subList(labels.size(), statements.size());
+			return erb.resetStatements(labels).addStatement(invariant).addStatements(remainder).build();
 		}
-		return new ExpressionResultBuilder(expressionResult).addAllExceptLrValueAndStatements(invariantExprResult)
-				.addStatement(invariant).build();
+		return erb.addStatement(invariant).build();
 	}
 
 	@Override