Remove --debug-level from cbmc and jbmc

This undocumented option no longer has any effect ever since
eb403a6 was merged.

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -213,9 +213,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("depth"))
     options.set_option("depth", cmdline.get_value("depth"));
 
-  if(cmdline.isset("debug-level"))
-    options.set_option("debug-level", cmdline.get_value("debug-level"));
-
   if(cmdline.isset("unwindset"))
     options.set_option("unwindset", cmdline.get_value("unwindset"));
 

jbmc/src/jbmc/jbmc_parse_options.h

@@ -45,7 +45,7 @@ class optionst;
   OPT_FUNCTIONS \
   "(no-simplify)(full-slice)" \
   OPT_REACHABILITY_SLICER \
-  "(debug-level):(no-propagation)(no-simplify-if)" \
+  "(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):" \
   "(object-bits):" \
   "(classpath):(cp):" \

src/cbmc/cbmc_parse_options.cpp

@@ -259,9 +259,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("depth"))
     options.set_option("depth", cmdline.get_value("depth"));
 
-  if(cmdline.isset("debug-level"))
-    options.set_option("debug-level", cmdline.get_value("debug-level"));
-
   if(cmdline.isset("slice-by-trace"))
   {
     log.error() << "--slice-by-trace has been removed" << messaget::eom;

src/cbmc/cbmc_parse_options.h

@@ -44,7 +44,7 @@ class optionst;
   OPT_FUNCTIONS \
   "(no-simplify)(full-slice)" \
   OPT_REACHABILITY_SLICER \
-  "(debug-level):(no-propagation)(no-simplify-if)" \
+  "(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):(test-preprocessor)" \
   "(write-solver-stats-to):"  \
   "(show-array-constraints)"  \

src/goto-symex/symex_config.h

@@ -36,8 +36,6 @@ struct symex_configt final
 
   bool havoc_undefined_functions;
 
-  mp_integer debug_level;
-
   /// \brief Should the additional validation checks be run?
   /// If this flag is set the checks for renaming (both level1 and level2) are
   /// executed in the goto_symex_statet (in the assignment method).

src/goto-symex/symex_main.cpp

@@ -25,7 +25,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/mathematical_expr.h>
 #include <util/replace_symbol.h>
 #include <util/std_expr.h>
-#include <util/string2int.h>
 #include <util/symbol_table.h>
 
 #include "path_storage.h"
@@ -43,7 +42,6 @@ symex_configt::symex_configt(const optionst &options)
     partial_loops(options.get_bool_option("partial-loops")),
     havoc_undefined_functions(
       options.get_bool_option("havoc-undefined-functions")),
-    debug_level(unsafe_string2int(options.get_option("debug-level"))),
     run_validation_checks(options.get_bool_option("validate-ssa-equation")),
     show_symex_steps(options.get_bool_option("show-goto-symex-steps")),
     show_points_to_sets(options.get_bool_option("show-points-to-sets")),