Merge pull request #998 from peterschrammel/label-properties-before-full-slice

Label properties before using property slicer

Author: kroening

regression/cbmc/full_slice1/main.c

@@ -0,0 +1,51 @@
+#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;
+  
+  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_slice1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice --property main.assertion.1 --unwind 1
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED
+--
+^warning: ignoring

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.

src/cbmc/cbmc_parse_options.cpp

@@ -456,8 +456,6 @@ int cbmc_parse_optionst::doit()
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
 
-  label_properties(goto_functions);
-
   if(cmdline.isset("show-claims") || // will go away
      cmdline.isset("show-properties")) // use this one
   {
@@ -801,13 +799,6 @@ bool cbmc_parse_optionst::process_goto_program(
     status() << "Generic Property Instrumentation" << eom;
     goto_check(ns, options, goto_functions);
 
-    // full slice?
-    if(cmdline.isset("full-slice"))
-    {
-      status() << "Performing a full slice" << eom;
-      full_slicer(goto_functions, ns);
-    }
-
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_functions, ns);
 
@@ -857,6 +848,23 @@ bool cbmc_parse_optionst::process_goto_program(
         return true;
     }
 
+    // label the assertions
+    // This must be done after adding assertions and
+    // before using the argument of the "property" option.
+    // Do not re-label after using the property slicer because
+    // this would cause the property identifiers to change.
+    label_properties(goto_functions);
+
+    // full slice?
+    if(cmdline.isset("full-slice"))
+    {
+      status() << "Performing a full slice" << eom;
+      if(cmdline.isset("property"))
+        property_slicer(goto_functions, ns, cmdline.get_values("property"));
+      else
+        full_slicer(goto_functions, ns);
+    }
+
     // remove skips
     remove_skip(goto_functions);
     goto_functions.update();

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1417,9 +1417,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       full_slicer(goto_functions, ns);
   }
 
-  // label the assertions
-  label_properties(goto_functions);
-
   // recalculate numbers, etc.
   goto_functions.update();
 }