From bb8c1582a8a885194d4b97c158f094a2b5a3cf8c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 8 Dec 2021 00:21:38 +0000 Subject: [PATCH] Remove --debug-level from cbmc and jbmc This undocumented option no longer has any effect ever since eb403a60174a was merged. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 3 --- jbmc/src/jbmc/jbmc_parse_options.h | 2 +- src/cbmc/cbmc_parse_options.cpp | 3 --- src/cbmc/cbmc_parse_options.h | 2 +- src/goto-symex/symex_config.h | 2 -- src/goto-symex/symex_main.cpp | 2 -- 6 files changed, 2 insertions(+), 12 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index f4e40d5812a..f6cce764e8b 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -205,9 +205,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")); diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 2e05f5cca5a..ad95ecc60a8 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_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)" \ "(object-bits):" \ "(classpath):(cp):" \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b9a4d5edaae..3a34ad521a6 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -258,9 +258,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; diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 7d5c544533d..b1a7abd9f27 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -38,7 +38,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)(test-preprocessor)" \ "(show-array-constraints)" \ OPT_CONFIG_C_CPP \ diff --git a/src/goto-symex/symex_config.h b/src/goto-symex/symex_config.h index 70650744356..9f292e7f014 100644 --- a/src/goto-symex/symex_config.h +++ b/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). diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 697779db366..7df69db080d 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -25,7 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #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")),