Merge pull request #6681 from tautschnig/cleanup/option-pretty-names

CBMC/JBMC: do not attempt to parse unused option pretty-names

Author: NlightNFotis

doc/man/cbmc.1

@@ -149,8 +149,6 @@ Show the verification conditions
 Remove assignments unrelated to property
 .IP --no-unwinding-assertions
 Do not generate unwinding assertions
-.IP --no-pretty-names
-Do not simplify identifiers
 .SS "BACKEND OPTIONS (cbmc)"
 .IP --dimacs
 Generate CNF in DIMACS format for use by external SAT solvers

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -95,7 +95,6 @@ void jbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("assumptions", true);
   options.set_option("built-in-assertions", true);
   options.set_option("lazy-methods", true);
-  options.set_option("pretty-names", true);
   options.set_option("propagation", true);
   options.set_option("refine-strings", true);
   options.set_option("simple-slice", true);
@@ -278,10 +277,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
       "--max-nondet-string-length");
   }
 
-  options.set_option(
-    "pretty-names",
-    !cmdline.isset("no-pretty-names"));
-
   if(cmdline.isset("graphml-witness"))
   {
     options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));

src/cbmc/cbmc_parse_options.cpp

@@ -104,7 +104,6 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
 {
   // Default true
   options.set_option("built-in-assertions", true);
-  options.set_option("pretty-names", true);
   options.set_option("propagation", true);
   options.set_option("simple-slice", true);
   options.set_option("simplify", true);
@@ -330,9 +329,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     }
   }
 
-  if(cmdline.isset("no-pretty-names"))
-    options.set_option("pretty-names", false);
-
   if(cmdline.isset("graphml-witness"))
   {
     options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));

src/goto-checker/bmc_util.h

@@ -180,7 +180,6 @@ void run_property_decider(
   "(slice-formula)" \
   "(unwinding-assertions)" \
   "(no-unwinding-assertions)" \
-  "(no-pretty-names)" \
   "(no-self-loops-to-assumptions)" \
   "(partial-loops)" \
   "(paths):" \
@@ -238,7 +237,6 @@ void run_property_decider(
   " --partial-loops              permit paths with partial loops\n" \
   " --no-self-loops-to-assumptions\n" \
   "                              do not simplify while(1){} to assume(0)\n" \
-  " --no-pretty-names            do not simplify identifiers\n" \
   " --symex-complexity-limit N   how complex (N) a path can become before\n" \
   "                              symex abandons it. Currently uses guard\n" \
   "                              size to calculate complexity. \n" \