From 1b308af248bf49db8ee8fe10ed56c3fc96b08203 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 8 Dec 2016 13:26:13 +0000 Subject: [PATCH 1/3] 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 --- src/ansi-c/ansi_c_entry_point.cpp | 12 +-- src/ansi-c/ansi_c_language.cpp | 8 +- src/cbmc/cbmc_parse_options.cpp | 119 +++++++++++++++---------- src/java_bytecode/java_entry_point.cpp | 10 +-- 4 files changed, 89 insertions(+), 60 deletions(-) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 1acfb7d4459..2b50d6d6212 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/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 ¶meters= - // 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); diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index 6e3b587d248..9323e9dd425 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/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); diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 08955180271..d5cbec6b5da 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/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,81 +303,84 @@ 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) @@ -375,23 +388,23 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) 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 diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 96bbd5764bb..399bfa3c0ec 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -21,7 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -30,8 +29,6 @@ Author: Daniel Kroening, kroening@kroening.com #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); From f98c61a844fc416ad6f0ef06b727490a6de5d6d5 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 21 Dec 2016 14:50:12 +0000 Subject: [PATCH 2/3] Add NOLINT exceptions to lines that fail the linter --- src/cbmc/cbmc_parse_options.cpp | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index d5cbec6b5da..d300712ce29 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -1070,10 +1070,10 @@ void cbmc_parse_optionst::help() " cbmc file.c ... source file names\n" "\n" "Analysis options:\n" - " --show-properties show the properties, but don't run analysis\n" + " --show-properties show the properties, but don't run analysis\n" // NOLINT(*) " --property id only check one specific property\n" - " --stop-on-fail stop analysis once a failed property is detected\n" - " --trace give a counterexample trace for failed properties\n" + " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) + " --trace give a counterexample trace for failed properties\n" //NOLINT(*) "\n" "C/C++ frontend options:\n" " -I path set include path (C/C++)\n" @@ -1096,14 +1096,14 @@ void cbmc_parse_optionst::help() configt::ansi_ct::default_c_standard()== configt::ansi_ct::c_standardt::C99?"c99": configt::ansi_ct::default_c_standard()== - configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" + configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*) " --cpp98/03/11 set C++ language standard (default: " << (configt::cppt::default_cpp_standard()== - configt::cppt::cpp_standardt::CPP98?"cpp98": + configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*) configt::cppt::default_cpp_standard()== - configt::cppt::cpp_standardt::CPP03?"cpp03": + configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*) configt::cppt::default_cpp_standard()== - configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" + configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*) #ifdef _WIN32 " --gcc use GCC as preprocessor\n" #endif @@ -1125,15 +1125,15 @@ void cbmc_parse_optionst::help() " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" " --error-label label check that label is unreachable\n" - " --cover CC create test-suite with coverage criterion CC\n" - " --mm MM memory consistency model for concurrent programs\n" + " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) + " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) "\n" "Java Bytecode frontend options:\n" " --classpath dir/jar set the classpath\n" " --main-class class-name set the name of the main class\n" "\n" "Semantic transformations:\n" - " --nondet-static add nondeterministic initialization of variables with static lifetime\n" + " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*) "\n" "BMC options:\n" " --program-only only show program expression\n" @@ -1147,11 +1147,11 @@ void cbmc_parse_optionst::help() " --unwinding-assertions generate unwinding assertions\n" " --partial-loops permit paths with partial loops\n" " --no-pretty-names do not simplify identifiers\n" - " --graphml-witness filename write the witness in GraphML format to filename\n" + " --graphml-witness filename write the witness in GraphML format to filename\n" // NOLINT(*) "\n" "Backend options:\n" " --dimacs generate CNF in DIMACS format\n" - " --beautify beautify the counterexample (greedy heuristic)\n" + " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*) " --localize-faults localize faults (experimental)\n" " --smt1 use default SMT1 solver (obsolete)\n" " --smt2 use default SMT2 solver (Z3)\n" @@ -1162,8 +1162,8 @@ void cbmc_parse_optionst::help() " --z3 use Z3\n" " --refine use refinement procedure (experimental)\n" " --outfile filename output formula to given file\n" - " --arrays-uf-never never turn arrays into uninterpreted functions\n" - " --arrays-uf-always always turn arrays into uninterpreted functions\n" + " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) + " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*) "\n" "Other options:\n" " --version show version and exit\n" From fc59e0119df2bd0193e538f8f403207c6bcf4608 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 23 Dec 2016 16:19:05 +0100 Subject: [PATCH 3/3] Adjust ansi_c_entry_point.cpp to match coding standards --- src/ansi-c/ansi_c_entry_point.cpp | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 2b50d6d6212..0c6825fd39d 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -51,8 +51,8 @@ exprt::operandst build_function_environment( for(const auto & p : parameters) { - irep_idt base_name=p.get_base_name(); - if(base_name.empty()) base_name="argument#"+i2string(i); + irep_idt base_name=p.get_base_name().empty()? + ("argument#"+i2string(i)):p.get_base_name(); irep_idt identifier=id2string(goto_functionst::entry_point())+ "::"+id2string(base_name); @@ -135,10 +135,12 @@ void record_function_outputs( for(const auto & p : parameters) { + if(p.get_identifier().empty()) + continue; + irep_idt identifier=p.get_identifier(); - if(identifier.empty()) continue; - const symbolt &symbol = symbol_table.lookup(identifier); + const symbolt &symbol=symbol_table.lookup(identifier); if(symbol.type.id()==ID_pointer) { @@ -194,7 +196,8 @@ bool ansi_c_entry_point( symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find(it->second); - if(s_it==symbol_table.symbols.end()) continue; + if(s_it==symbol_table.symbols.end()) + continue; if(s_it->second.type.id()==ID_code) matches.push_back(it->second);