Add trace_configuration struct to global config

polgreen · polgreen · commit 235bb0190bb0 · 2017-10-20T16:49:52.000+02:00
Introduces trace_configurationt

Adds cmd line options to help file and to cbmc_parse_optionst

Note that this is only implemented for CBMC, I am working in a repository that doesn't contain symex.
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -105,6 +105,47 @@ void cbmc_parse_optionst::eval_verbosity()
   ui_message_handler.set_verbosity(v);
 }
 
+void cbmc_parse_optionst::configure_trace_output()
+{
+
+  if(cmdline.isset("trace-hex"))
+    config.trace_config.numeric_representation =
+        configt::numeric_representationt::HEX;
+  else
+    config.trace_config.numeric_representation =
+        configt::numeric_representationt::BINARY;
+
+  if(cmdline.isset("trace-show-source-code"))
+    config.trace_config.show_source_code=true;
+  else
+    config.trace_config.show_source_code=false;
+
+  if(cmdline.isset("trace-hide-assignments"))
+    config.trace_config.show_value_assignments=false;
+  else
+    config.trace_config.show_value_assignments=true;
+
+  if(cmdline.isset("trace-hide-inputs"))
+    config.trace_config.show_inputs=false;
+  else
+    config.trace_config.show_inputs=true;
+
+  if(cmdline.isset("trace-hide-outputs"))
+    config.trace_config.show_outputs=false;
+  else
+    config.trace_config.show_outputs=true;
+
+  if(cmdline.isset("trace-show-function-calls"))
+    config.trace_config.show_function_calls=true;
+  else
+    config.trace_config.show_function_calls=false;
+
+  if(cmdline.isset("html-trace"))
+    config.trace_config.trace_format = configt::trace_formatt::HTML;
+  else
+    config.trace_config.trace_format = configt::trace_formatt::STANDARD;
+}
+
 void cbmc_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -159,14 +200,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
      cmdline.isset("stop-on-fail"))
   {
     options.set_option("trace", true);
-    if(cmdline.isset("hex"))
-      options.set_option("hex", true);
-
-    if(cmdline.isset("trace-verbosity"))
-      options.set_option("trace-verbosity",
-          cmdline.get_value("trace-verbosity"));
-    else
-      options.set_option("trace-verbosity", 1);
+    configure_trace_output();
   }
 
   if(cmdline.isset("localize-faults"))
@@ -1096,5 +1130,14 @@ void cbmc_parse_optionst::help()
     " --xml-interface              bi-directional XML interface\n"
     " --json-ui                    use JSON-formatted output\n"
     " --verbosity #                verbosity level\n"
+    "\n"
+    "Trace formatting options\n"
+    "--trace-show-function-calls  show functions calls and returns in trace (default is to hide)\n" // NOLINT(*)
+    "--trace-hide-assignments     show all assignments in trace (default is to show)\n" // NOLINT(*)
+    "--trace-hide-inputs          show all inputs in trace (default is to show)\n" // NOLINT(*)
+    "--trace-hide-outputs         show all outputs in trace (default is to show)\n" // NOLINT(*)
+    "--trace-show-source-code     show lines of source code (default is to hide)\n" // NOLINT(*)
+    "--trace-hex                  outputs assignments to variables in hex (default is binary)\n" // NOLINT(*)
+    "--html-trace                 outputs trace in html format\n"
     "\n";
 }
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
@@ -57,8 +57,9 @@ class optionst;
   "(drop-unused-functions)" \
   "(havoc-undefined-functions)" \
   "(property):(stop-on-fail)(trace)" \
-  "(hex)" \
-  "(trace-verbosity):" \
+  "(trace-hex)(trace-show-source-code)(trace-hide-assignments)"\
+  "(trace-show-function-calls)(html-trace)(trace-hide-inputs)" \
+  "(trace-hide-outputs)" \
   "(error-label):(verbosity):(no-library)" \
   "(nondet-static)" \
   "(version)" \
@@ -97,6 +98,7 @@ class cbmc_parse_optionst:
   void eval_verbosity();
   void register_languages();
   void get_command_line_options(optionst &);
+  void configure_trace_output();
   void preprocessing();
   int get_goto_program(const optionst &);
   bool process_goto_program(const optionst &);
diff --git a/src/util/config.h b/src/util/config.h
@@ -24,6 +24,20 @@ class namespacet;
 class configt
 {
 public:
+  typedef enum { STANDARD, HTML } trace_formatt;
+  typedef enum { HEX, BINARY } numeric_representationt;
+
+  struct trace_configurationt
+  {
+    bool show_function_calls;
+    bool show_source_code;
+    bool show_inputs;
+    bool show_outputs;
+    bool show_value_assignments;
+    numeric_representationt numeric_representation;
+    trace_formatt trace_format;
+  } trace_config;
+
   struct ansi_ct
   {
     // for ANSI-C
