Test to detect incorrect relabelling of properties after slicing

Author: peterschrammel

regression/cbmc/full_slice2/main.c

@@ -0,0 +1,53 @@
+#include <assert.h>
+
+typedef enum {
+  A,
+  B,
+  C
+} node_t;
+
+void doit(node_t *node);
+
+static inline void foo(node_t *node) { }
+static inline void bar(node_t *node) { }
+
+void doit(node_t *node) 
+{
+  switch (*node)
+  {
+  case A:
+    foo(node);
+    *node=B;
+    bar(node);
+    return;
+  case C:
+    *node=B;
+    bar(node);
+    return;
+  }
+}
+
+int main() 
+{
+  node_t node=A;
+
+  assert(&node);
+  
+  char count=0;  
+  while(count++<10)
+  {
+    char c;    
+
+    doit(&node);
+
+    static char q=0;      
+    q=0;
+    
+    if(c==0) 
+    {
+      assert(node==A);
+    }
+  }
+
+  return 0;
+}

regression/cbmc/full_slice2/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--full-slice --property main.assertion.2 --unwind 1
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED
+--
+^warning: ignoring
+--
+Tests whether properties are not relabelled after slicing.