Fixing lint errors in files touched by PR #338

Corrected lint errors in some files as they were touched by #338.

There are some outstanding errors that I wasn't sure how to fix:

- The formatting of the CBMC help message

Author: thk123

src/ansi-c/ansi_c_entry_point.cpp

@@ -109,15 +109,12 @@ void record_function_outputs(
   code_blockt &init_code,
   symbol_tablet &symbol_table)
 {
-  //const code_typet::parameterst &parameters=
-  //  to_code_type(function.type).parameters();
-
   bool has_return_value=
     to_code_type(function.type).return_type()!=empty_typet();
 
   if(has_return_value)
   {
-    //record return value
+    // record return value
     codet output(ID_output);
     output.operands().resize(2);
 
@@ -194,7 +191,8 @@ bool ansi_c_entry_point(
     forall_symbol_base_map(it, symbol_table.symbol_base_map, config.main)
     {
       // look it up
-      symbol_tablet::symbolst::const_iterator s_it=symbol_table.symbols.find(it->second);
+      symbol_tablet::symbolst::const_iterator s_it=
+        symbol_table.symbols.find(it->second);
 
       if(s_it==symbol_table.symbols.end()) continue;
 
@@ -456,7 +454,9 @@ bool ansi_c_entry_point(
           const exprt &arg1=parameters[1];
 
           exprt index_expr(ID_index, arg1.type().subtype());
-          index_expr.copy_to_operands(argv_symbol.symbol_expr(), gen_zero(index_type()));
+          index_expr.copy_to_operands(
+            argv_symbol.symbol_expr(),
+            gen_zero(index_type()));
 
           // disable bounds check on that one
           index_expr.set("bounds_check", false);

src/ansi-c/ansi_c_language.cpp

@@ -169,8 +169,14 @@ bool ansi_c_languaget::typecheck(
 {
   symbol_tablet new_symbol_table;
 
-  if(ansi_c_typecheck(parse_tree, new_symbol_table, module, get_message_handler()))
+  if(ansi_c_typecheck(
+    parse_tree,
+    new_symbol_table,
+    module,
+    get_message_handler()))
+  {
     return true;
+  }
 
   remove_internal_symbols(new_symbol_table);
 

src/cbmc/cbmc_parse_options.cpp

@@ -117,7 +117,8 @@ void cbmc_parse_optionst::eval_verbosity()
   if(cmdline.isset("verbosity"))
   {
     v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v>10) v=10;
+    if(v>10)
+      v=10;
   }
 
   ui_message_handler.set_verbosity(v);
@@ -192,8 +193,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("localize-faults"))
     options.set_option("localize-faults", true);
   if(cmdline.isset("localize-faults-method"))
-    options.set_option("localize-faults-method",
-                       cmdline.get_value("localize-faults-method"));
+  {
+    options.set_option(
+      "localize-faults-method",
+      cmdline.get_value("localize-faults-method"));
+  }
 
   if(cmdline.isset("unwind"))
     options.set_option("unwind", cmdline.get_value("unwind"));
@@ -239,23 +243,29 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("cover"))
     options.set_option("unwinding-assertions", false);
   else
-    options.set_option("unwinding-assertions",
+  {
+    options.set_option(
+      "unwinding-assertions",
       cmdline.isset("unwinding-assertions"));
+  }
 
   // generate unwinding assumptions otherwise
-  options.set_option("partial-loops",
-   cmdline.isset("partial-loops"));
+  options.set_option(
+    "partial-loops",
+    cmdline.isset("partial-loops"));
 
   if(options.get_bool_option("partial-loops") &&
      options.get_bool_option("unwinding-assertions"))
   {
-    error() << "--partial-loops and --unwinding-assertions must not be given together" << eom;
+    error() << "--partial-loops and --unwinding-assertions "
+            << "must not be given together" << eom;
     exit(1); // should contemplate EX_USAGE from sysexits.h
   }
 
   // remove unused equations
-  options.set_option("slice-formula",
-       cmdline.isset("slice-formula"));
+  options.set_option(
+    "slice-formula",
+    cmdline.isset("slice-formula"));
 
   // simplify if conditions and branches
   if(cmdline.isset("no-simplify-if"))
@@ -293,105 +303,108 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   }
 
   if(cmdline.isset("max-node-refinement"))
-    options.set_option("max-node-refinement", cmdline.get_value("max-node-refinement"));
+    options.set_option(
+      "max-node-refinement",
+      cmdline.get_value("max-node-refinement"));
 
   if(cmdline.isset("aig"))
     options.set_option("aig", true);
 
   // SMT Options
-  bool version_set = false;
+  bool version_set=false;
 
   if(cmdline.isset("smt1"))
   {
     options.set_option("smt1", true);
     options.set_option("smt2", false);
-    version_set = true;
+    version_set=true;
   }
 
   if(cmdline.isset("smt2"))
   {
-    options.set_option("smt1", false);// If both are given, smt2 takes precedence
+    // If both are given, smt2 takes precedence
+    options.set_option("smt1", false);
     options.set_option("smt2", true);
-    version_set = true;
+    version_set=true;
   }
 
   if(cmdline.isset("fpa"))
     options.set_option("fpa", true);
 
 
-  bool solver_set = false;
+  bool solver_set=false;
 
   if(cmdline.isset("boolector"))
   {
-    options.set_option("boolector", true), solver_set = true;
+    options.set_option("boolector", true), solver_set=true;
     if(!version_set)
-      options.set_option("smt2", true), version_set = true;
+      options.set_option("smt2", true), version_set=true;
   }
 
   if(cmdline.isset("mathsat"))
   {
-    options.set_option("mathsat", true), solver_set = true;
+    options.set_option("mathsat", true), solver_set=true;
     if(!version_set)
-      options.set_option("smt2", true), version_set = true;
+      options.set_option("smt2", true), version_set=true;
   }
 
   if(cmdline.isset("cvc3"))
   {
-    options.set_option("cvc3", true), solver_set = true;
+    options.set_option("cvc3", true), solver_set=true;
     if(!version_set)
-      options.set_option("smt1", true), version_set = true;
+      options.set_option("smt1", true), version_set=true;
   }
 
   if(cmdline.isset("cvc4"))
   {
-    options.set_option("cvc4", true), solver_set = true;
+    options.set_option("cvc4", true), solver_set=true;
     if(!version_set)
-      options.set_option("smt2", true), version_set = true;
+      options.set_option("smt2", true), version_set=true;
   }
 
   if(cmdline.isset("yices"))
   {
-    options.set_option("yices", true), solver_set = true;
+    options.set_option("yices", true), solver_set=true;
     if(!version_set)
-      options.set_option("smt2", true), version_set = true;
+      options.set_option("smt2", true), version_set=true;
   }
 
   if(cmdline.isset("z3"))
   {
-    options.set_option("z3", true), solver_set = true;
+    options.set_option("z3", true), solver_set=true;
     if(!version_set)
-      options.set_option("smt2", true), version_set = true;
+      options.set_option("smt2", true), version_set=true;
   }
 
   if(cmdline.isset("opensmt"))
   {
-    options.set_option("opensmt", true), solver_set = true;
+    options.set_option("opensmt", true), solver_set=true;
     if(!version_set)
-      options.set_option("smt1", true), version_set = true;
+      options.set_option("smt1", true), version_set=true;
   }
 
   if(version_set && !solver_set)
   {
     if(cmdline.isset("outfile"))
     {
       // outfile and no solver should give standard compliant SMT-LIB
-      options.set_option("generic", true), solver_set = true;
+      options.set_option("generic", true), solver_set=true;
     }
     else
     {
       if(options.get_bool_option("smt1"))
       {
-        options.set_option("boolector", true), solver_set = true;
+        options.set_option("boolector", true), solver_set=true;
       }
       else
       {
         assert(options.get_bool_option("smt2"));
-        options.set_option("z3", true), solver_set = true;
+        options.set_option("z3", true), solver_set=true;
       }
     }
   }
   // Either have solver and standard version set, or neither.
-  assert(version_set == solver_set);
+  assert(version_set==solver_set);
 
   if(cmdline.isset("beautify"))
     options.set_option("beautify", true);
@@ -401,8 +414,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   else
     options.set_option("sat-preprocessor", true);
 
-  options.set_option("pretty-names",
-                     !cmdline.isset("no-pretty-names"));
+  options.set_option(
+    "pretty-names",
+    !cmdline.isset("no-pretty-names"));
 
   if(cmdline.isset("outfile"))
     options.set_option("outfile", cmdline.get_value("outfile"));
@@ -457,7 +471,6 @@ int cbmc_parse_optionst::doit()
 
   if(cmdline.isset("module") ||
      cmdline.isset("gen-interface"))
-
   {
     error() << "This version of CBMC has no support for "
                " hardware modules. Please use hw-cbmc." << eom;
@@ -514,7 +527,8 @@ int cbmc_parse_optionst::doit()
     return 0; // should contemplate EX_OK from sysexits.h
   }
 
-  if(cmdline.isset("show-reachable-properties")) // may replace --show-properties
+  // may replace --show-properties
+  if(cmdline.isset("show-reachable-properties"))
   {
     const namespacet ns(symbol_table);
 
@@ -668,11 +682,15 @@ int cbmc_parse_optionst::get_goto_program(
 
     if(!cmdline.args.empty())
     {
-      if(parse()) return 6;
-      if(typecheck()) return 6;
+      if(parse())
+        return 6;
+      if(typecheck())
+        return 6;
       int get_modules_ret=get_modules(bmc);
-      if(get_modules_ret!=-1) return get_modules_ret;
-      if(binaries.empty() && final()) return 6;
+      if(get_modules_ret!=-1)
+        return get_modules_ret;
+      if(binaries.empty() && final())
+        return 6;
 
       // we no longer need any parse trees or language files
       clear_parse();
@@ -685,9 +703,14 @@ int cbmc_parse_optionst::get_goto_program(
     {
       status() << "Reading GOTO program from file " << eom;
 
-      if(read_object_and_link(*it, symbol_table, goto_functions,
-                              get_message_handler()))
+      if(read_object_and_link(
+        *it,
+        symbol_table,
+        goto_functions,
+        get_message_handler()))
+      {
         return 6;
+      }
     }
 
     if(!binaries.empty())
@@ -851,7 +874,9 @@ bool cbmc_parse_optionst::process_goto_program(
 
     // remove function pointers
     status() << "Removal of function pointers and virtual functions" << eom;
-    remove_function_pointers(symbol_table, goto_functions,
+    remove_function_pointers(
+      symbol_table,
+      goto_functions,
       cmdline.isset("pointer-check"));
     remove_virtual_functions(symbol_table, goto_functions);
 
@@ -887,8 +912,10 @@ bool cbmc_parse_optionst::process_goto_program(
     if(cmdline.isset("string-abstraction"))
     {
       status() << "String Abstraction" << eom;
-      string_abstraction(symbol_table,
-        get_message_handler(), goto_functions);
+      string_abstraction(
+        symbol_table,
+        get_message_handler(),
+        goto_functions);
     }
 
     // add failed symbols

src/java_bytecode/java_entry_point.cpp

@@ -21,7 +21,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/namespace.h>
 #include <util/pointer_offset_size.h>
 #include <util/i2string.h>
-#include <util/prefix.h>
 #include <ansi-c/c_types.h>
 #include <ansi-c/string_constant.h>
 
@@ -30,8 +29,6 @@ Author: Daniel Kroening, [email protected]
 #include "java_entry_point.h"
 #include "java_object_factory.h"
 
-//#include "zero_initializer.h"
-
 #define INITIALIZE CPROVER_PREFIX "initialize"
 
 /*******************************************************************\
@@ -46,8 +43,7 @@ Function: create_initialize
 
 \*******************************************************************/
 
-namespace {
-void create_initialize(symbol_tablet &symbol_table)
+static void create_initialize(symbol_tablet &symbol_table)
 {
   symbolt initialize;
   initialize.name=INITIALIZE;
@@ -72,7 +68,7 @@ void create_initialize(symbol_tablet &symbol_table)
   if(symbol_table.add(initialize))
     throw "failed to add "+std::string(INITIALIZE);
 }
-}
+
 
 /*******************************************************************\
 
@@ -217,7 +213,7 @@ void java_record_outputs(
 
   if(has_return_value)
   {
-    //record return value
+    // record return value
     codet output(ID_output);
     output.operands().resize(2);