Merge pull request #4360 from peterschrammel/simple-slice-full-trace

Make use of simple-slice more explicit

Author: tautschnig

doc/architectural/folder-walkthrough.md

@@ -14,6 +14,7 @@ containing the code for a different part of the system.
   * \ref linking
 
 - Symbolic Execution
+  * \ref goto-checker
   * \ref goto-symex
 
 - Static Analyses
@@ -36,9 +37,10 @@ containing the code for a different part of the system.
 
   * \ref cbmc
   * \ref goto-analyzer
-  * \ref goto-instrument
-  * \ref goto-diff
   * \ref goto-cc
+  * \ref goto-diff
+  * \ref goto-harness
+  * \ref goto-instrument
   * \ref jbmc
 
 - Utilities

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -108,6 +108,7 @@ void jbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("propagation", true);
   options.set_option("refine-strings", true);
   options.set_option("sat-preprocessor", true);
+  options.set_option("simple-slice", true);
   options.set_option("simplify", true);
   options.set_option("simplify-if", true);
 

src/cbmc/cbmc_parse_options.cpp

@@ -114,6 +114,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("pretty-names", true);
   options.set_option("propagation", true);
   options.set_option("sat-preprocessor", true);
+  options.set_option("simple-slice", true);
   options.set_option("simplify", true);
   options.set_option("simplify-if", true);
 

src/goto-checker/bmc_util.cpp

@@ -233,7 +233,7 @@ void slice(
     }
     else
     {
-      if(options.get_list_option("cover").empty())
+      if(options.get_bool_option("simple-slice"))
       {
         simple_slice(symex_target_equation);
         msg.statistics() << "simple slicing removed "

src/goto-checker/goto_trace_provider.h

@@ -23,6 +23,8 @@ class goto_trace_providert
 {
 public:
   /// Builds and returns the complete trace
+  /// \note If slicing is used then the trace will not be complete.
+  ///   E.g. with simple-slice it will end at the last assertion.
   virtual goto_tracet build_full_trace() const = 0;
 
   /// Builds and returns the trace up to the first failed property

src/goto-instrument/cover.cpp

@@ -165,6 +165,10 @@ parse_coverage_criterion(const std::string &criterion_string)
 void parse_cover_options(const cmdlinet &cmdline, optionst &options)
 {
   options.set_option("cover", cmdline.get_values("cover"));
+
+  // allow retrieving full traces
+  options.set_option("simple-slice", false);
+
   options.set_option(
     "cover-include-pattern", cmdline.get_value("cover-include-pattern"));
   options.set_option("no-trivial-tests", cmdline.isset("no-trivial-tests"));