add option to show code in CBMC trace

Author: polgreen

regression/cbmc/trace_show_code/main.c

@@ -0,0 +1,23 @@
+int function_to_call(int a)
+{
+	int local = 1;
+	return a+local;
+}
+
+
+int main()
+{
+	int a, c;
+	unsigned int b;
+	a = 0;
+	c = -100;
+	a = function_to_call(a) + function_to_call(c);
+	if(a < 0)
+	  b = function_to_call(b);
+
+	if(c < 0)
+	  b = -function_to_call(b);
+
+	__CPROVER_assert(0,"");
+
+}

regression/cbmc/trace_show_code/test.desc

@@ -0,0 +1,20 @@
+CORE
+main.c
+--trace --trace-show-code
+^EXIT=10$
+^SIGNAL=0$
+
+local = 1
+int a
+int c
+unsigned int b
+a = 0;
+c = -100;
+function_to_call\(a\)
+function_to_call\(c\)
+a = return_value_function_to_call \+ return_value_function_to_call
+function_to_call\(\(signed int\)b\)
+b = \(unsigned int\)return_value_function_to_call
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/goto-programs/goto_trace.cpp

@@ -247,20 +247,30 @@ void trace_value(
 
 void show_state_header(
   std::ostream &out,
+  const namespacet &ns,
   const goto_trace_stept &state,
   const source_locationt &source_location,
-  unsigned step_nr)
+  unsigned step_nr,
+  const trace_optionst &options)
 {
   out << "\n";
 
-  if(step_nr==0)
+  if(step_nr == 0)
     out << "Initial State";
   else
     out << "State " << step_nr;
 
-  out << " " << source_location
-      << " thread " << state.thread_nr << "\n";
-  out << "----------------------------------------------------" << "\n";
+  out << " " << source_location << " thread " << state.thread_nr << "\n";
+  out << "----------------------------------------------------"
+      << "\n";
+
+  if(options.show_code)
+  {
+    out << as_string(ns, *state.pc)
+        << "\n";
+    out << "----------------------------------------------------"
+        << "\n";
+  }
 }
 
 bool is_index_member_symbol(const exprt &src)
@@ -342,7 +352,8 @@ void show_goto_trace(
         {
           first_step=false;
           prev_step_nr=step.step_nr;
-          show_state_header(out, step, step.pc->source_location, step.step_nr);
+          show_state_header(
+            out, ns, step, step.pc->source_location, step.step_nr, options);
         }
 
         // see if the full lhs is something clean
@@ -370,7 +381,8 @@ void show_goto_trace(
       {
         first_step=false;
         prev_step_nr=step.step_nr;
-        show_state_header(out, step, step.pc->source_location, step.step_nr);
+        show_state_header(
+          out, ns, step, step.pc->source_location, step.step_nr, options);
       }
 
       trace_value(
@@ -387,7 +399,8 @@ void show_goto_trace(
       }
       else
       {
-        show_state_header(out, step, step.pc->source_location, step.step_nr);
+        show_state_header(
+          out, ns, step, step.pc->source_location, step.step_nr, options);
         out << "  OUTPUT " << step.io_id << ":";
 
         for(std::list<exprt>::const_iterator
@@ -408,7 +421,8 @@ void show_goto_trace(
       break;
 
     case goto_trace_stept::typet::INPUT:
-      show_state_header(out, step, step.pc->source_location, step.step_nr);
+      show_state_header(
+        out, ns, step, step.pc->source_location, step.step_nr, options);
       out << "  INPUT " << step.io_id << ":";
 
       for(std::list<exprt>::const_iterator

src/goto-programs/goto_trace.h

@@ -201,6 +201,7 @@ struct trace_optionst
   bool hex_representation;
   bool base_prefix;
   bool show_function_calls;
+  bool show_code;
 
   static const trace_optionst default_options;
 
@@ -210,6 +211,7 @@ struct trace_optionst
     hex_representation = options.get_bool_option("trace-hex");
     base_prefix = hex_representation;
     show_function_calls = options.get_bool_option("trace-show-function-calls");
+    show_code = options.get_bool_option("trace-show-code");
   };
 
 private:
@@ -219,6 +221,7 @@ struct trace_optionst
     hex_representation = false;
     base_prefix = false;
     show_function_calls = false;
+    show_code = false;
   };
 };
 
@@ -243,18 +246,22 @@ void trace_value(
 
 #define OPT_GOTO_TRACE "(trace-json-extended)" \
                        "(trace-show-function-calls)" \
+                       "(trace-show-code)" \
                        "(trace-hex)"
 
 #define HELP_GOTO_TRACE                                                        \
   " --trace-json-extended        add rawLhs property to trace\n"               \
   " --trace-show-function-calls  show function calls in plain trace\n"         \
+  " --trace-show-code            show original code in plain trace\n"          \
   " --trace-hex                  represent plain trace values in hex\n"
 
 #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)                             \
   if(cmdline.isset("trace-json-extended"))                                     \
     options.set_option("trace-json-extended", true);                           \
   if(cmdline.isset("trace-show-function-calls"))                               \
     options.set_option("trace-show-function-calls", true);                     \
+  if(cmdline.isset("trace-show-code"))                                       \
+      options.set_option("trace-show-code", true);                             \
   if(cmdline.isset("trace-hex"))                                               \
     options.set_option("trace-hex", true);