Merge pull request #6514 from tautschnig/swap-labels

Swapping goto_programt::instructiont must preserve labels

Author: tautschnig

regression/goto-instrument/labels1/main.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int foo()
+{
+  return 1;
+}
+
+typedef int (*fptr_t)(void);
+
+int main()
+{
+label_zero:
+  assert(1);
+  int x;
+  int *p;
+  goto label_two;
+label_one:
+  assert(x < 0 || x >= 0);
+label_two:
+  p = malloc(sizeof(int));
+label_three:
+  if(foo())
+    x = 42;
+label_four:
+  assert(foo() == 1);
+label_five:
+  fptr_t fp = foo;
+  assert(fp() == 1);
+label_six:
+  return *p;
+}

regression/goto-instrument/labels1/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+
+Labels: label_zero$
+Labels: label_one$
+Labels: label_two$
+Labels: label_three$
+Labels: label_four$
+Labels: label_five$
+Labels: label_six$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test ensures that label names specified in the source code are preserved.

src/goto-programs/goto_program.h

@@ -527,6 +527,7 @@ class goto_programt
       swap(instruction._type, _type);
       swap(instruction.guard, guard);
       swap(instruction.targets, targets);
+      swap(instruction.labels, labels);
     }
 
     /// Uniquely identify an invalid target or location