From fbdf29a9420eae70ff7c66dc3462d61e21e2c6b9 Mon Sep 17 00:00:00 2001 From: reuk Date: Thu, 16 Mar 2017 13:48:29 +0000 Subject: [PATCH 1/3] Remove DEBUG ifdefs which broke the debug build --- .travis.yml | 2 ++ src/analyses/constant_propagator.cpp | 2 -- src/analyses/natural_loops.cpp | 2 -- src/analyses/natural_loops.h | 6 ---- src/cpp/parse.cpp | 29 ------------------- src/goto-instrument/accelerate/accelerate.cpp | 2 -- .../accelerate/acceleration_utils.cpp | 2 -- .../accelerate/all_paths_enumerator.cpp | 2 -- .../accelerate/cone_of_influence.cpp | 2 -- .../disjunctive_polynomial_acceleration.cpp | 3 -- .../enumerating_loop_acceleration.cpp | 2 -- .../accelerate/overflow_instrumenter.cpp | 2 -- .../accelerate/polynomial_accelerator.cpp | 3 -- .../accelerate/sat_path_enumerator.cpp | 2 -- .../accelerate/scratch_program.cpp | 11 ------- .../accelerate/trace_automaton.cpp | 16 ---------- src/goto-programs/goto_inline_class.cpp | 2 -- src/linking/linking.cpp | 10 ------- src/path-symex/path_symex.cpp | 2 -- src/path-symex/path_symex_state.cpp | 2 -- src/path-symex/path_symex_state_read.cpp | 2 -- src/path-symex/var_map.cpp | 2 -- src/pointer-analysis/dereference.cpp | 2 -- .../value_set_dereference.cpp | 2 -- src/solvers/flattening/arrays.cpp | 2 -- src/solvers/flattening/boolbv.cpp | 9 ------ src/solvers/flattening/boolbv_get.cpp | 2 -- src/solvers/flattening/boolbv_map.cpp | 2 -- src/solvers/flattening/equality.cpp | 7 ----- src/solvers/flattening/functions.cpp | 2 -- src/solvers/prop/prop_conv.cpp | 2 -- src/solvers/sat/satcheck_limmat.cpp | 2 -- src/solvers/sat/satcheck_zchaff.cpp | 2 -- 33 files changed, 2 insertions(+), 140 deletions(-) diff --git a/.travis.yml b/.travis.yml index d74ec93f7e3..3fc29224575 100644 --- a/.travis.yml +++ b/.travis.yml @@ -68,6 +68,8 @@ matrix: script: - if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ; + COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O0 -ggdb3 -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DDEBUG\" -j2" && + eval ${PRE_COMMAND} ${COMMAND} && COMMAND="make -C src minisat2-download" && eval ${PRE_COMMAND} ${COMMAND} && COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare\" -j2" && diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 1fe89a7b8f6..189048994b8 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -6,8 +6,6 @@ Author: Peter Schrammel \*******************************************************************/ -// #define DEBUG - #ifdef DEBUG #include #endif diff --git a/src/analyses/natural_loops.cpp b/src/analyses/natural_loops.cpp index 16985daa5e9..593fc78006d 100644 --- a/src/analyses/natural_loops.cpp +++ b/src/analyses/natural_loops.cpp @@ -10,8 +10,6 @@ Author: Georg Weissenbacher, georg@weissenbacher.name #include "natural_loops.h" -// #define DEBUG - /*******************************************************************\ Function: show_natural_loops diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h index 327ebbdf112..3408aba68db 100644 --- a/src/analyses/natural_loops.h +++ b/src/analyses/natural_loops.h @@ -81,8 +81,6 @@ Function: natural_loops_templatet::compute \*******************************************************************/ -// #define DEBUG - #ifdef DEBUG #include #endif @@ -92,10 +90,6 @@ void natural_loops_templatet::compute(P &program) { cfg_dominators(program); -#ifdef DEBUG - cfg_dominators.output(std::cout); -#endif - // find back-edges m->n for(T m_it=program.instructions.begin(); m_it!=program.instructions.end(); diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 5a7d2095a58..b15b486c248 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -21,8 +21,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_member_spec.h" #include "cpp_enum_type.h" -// #define DEBUG - #ifdef DEBUG #include @@ -639,12 +637,6 @@ bool Parser::rDefinition(cpp_itemt &item) { int t=lex.LookAhead(0); - #ifdef DEBUG - indenter _i; - std::cout << std::string(__indent, ' ') << "Parser::rDefinition 1 " << t - << "\n"; - #endif - if(t==';') return rNullDeclaration(item.make_declaration()); else if(t==TOK_TYPEDEF) @@ -1237,12 +1229,6 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl) switch(kind) { case tdk_decl: - #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "BODY: " << body << std::endl; - std::cout << std::string(__indent, ' ') << "TEMPLATE_TYPE: " - << template_type << std::endl; - #endif - body.add(ID_template_type).swap(template_type); body.set(ID_is_template, true); decl.swap(body); @@ -1909,12 +1895,6 @@ bool Parser::rIntegralDeclaration( if(lex.LookAhead(0)==';') { - #ifdef DEBUG - std::cout << std::string(__indent, ' ') - << "Parser::rIntegralDeclaration 8 " - << declaration << "\n"; - #endif - lex.get_token(tk); return true; } @@ -5119,11 +5099,6 @@ bool Parser::rClassBody(exprt &body) return true; // error recovery } - #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "Parser::rClassBody " << member - << std::endl; - #endif - members.move_to_operands( static_cast(static_cast(member))); } @@ -9244,10 +9219,6 @@ bool Parser::rExprStatement(codet &statement) if(rDeclarationStatement(statement)) { - #ifdef DEBUG - std::cout << std::string(__indent, ' ') << "rDe: " << statement - << std::endl; - #endif return true; } else diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index 93d0ca0dfd7..bb86d5a4d75 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -27,8 +27,6 @@ Author: Matt Lewis #include "overflow_instrumenter.h" #include "util.h" -#define DEBUG - goto_programt::targett acceleratet::find_back_jump( goto_programt::targett loop_header) { diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index d90357d2246..1d42ebf1945 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -42,8 +42,6 @@ Author: Matt Lewis #include "cone_of_influence.h" #include "overflow_instrumenter.h" -#define DEBUG - void acceleration_utilst::gather_rvalues( const exprt &expr, expr_sett &rvalues) diff --git a/src/goto-instrument/accelerate/all_paths_enumerator.cpp b/src/goto-instrument/accelerate/all_paths_enumerator.cpp index cfc1c3ae2ed..8b1038d426d 100644 --- a/src/goto-instrument/accelerate/all_paths_enumerator.cpp +++ b/src/goto-instrument/accelerate/all_paths_enumerator.cpp @@ -10,8 +10,6 @@ Author: Matt Lewis #include "all_paths_enumerator.h" -// #define DEBUG - bool all_paths_enumeratort::next(patht &path) { if(last_path.empty()) diff --git a/src/goto-instrument/accelerate/cone_of_influence.cpp b/src/goto-instrument/accelerate/cone_of_influence.cpp index a1914756698..0f0b969e342 100644 --- a/src/goto-instrument/accelerate/cone_of_influence.cpp +++ b/src/goto-instrument/accelerate/cone_of_influence.cpp @@ -12,8 +12,6 @@ Author: Matt Lewis #include "cone_of_influence.h" -// #define DEBUG - void cone_of_influencet::cone_of_influence( const expr_sett &targets, expr_sett &cone) diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index 6f91824a8e7..29d5ac0f81b 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp @@ -43,9 +43,6 @@ Author: Matt Lewis #include "cone_of_influence.h" #include "overflow_instrumenter.h" -#define DEBUG - - bool disjunctive_polynomial_accelerationt::accelerate( path_acceleratort &accelerator) { diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp b/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp index 1590eb6c127..d47c0c6287a 100644 --- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp +++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp @@ -10,8 +10,6 @@ Author: Matt Lewis #include "enumerating_loop_acceleration.h" -// #define DEBUG - bool enumerating_loop_accelerationt::accelerate( path_acceleratort &accelerator) { diff --git a/src/goto-instrument/accelerate/overflow_instrumenter.cpp b/src/goto-instrument/accelerate/overflow_instrumenter.cpp index 2bad8d1283b..6e126aeb581 100644 --- a/src/goto-instrument/accelerate/overflow_instrumenter.cpp +++ b/src/goto-instrument/accelerate/overflow_instrumenter.cpp @@ -18,8 +18,6 @@ Author: Matt Lewis #include "overflow_instrumenter.h" #include "util.h" -// #define DEBUG - /* * This code is copied wholesale from analyses/goto_check.cpp. */ diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index a9dbb2ff58f..ccf24d6e475 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -39,9 +39,6 @@ Author: Matt Lewis #include "cone_of_influence.h" #include "overflow_instrumenter.h" -#define DEBUG - - bool polynomial_acceleratort::accelerate( patht &loop, path_acceleratort &accelerator) diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp index 17bc94ecce0..d8067ec3640 100644 --- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp +++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp @@ -42,8 +42,6 @@ Author: Matt Lewis #include "util.h" #include "overflow_instrumenter.h" -#define DEBUG - bool sat_path_enumeratort::next(patht &path) { scratch_programt program(symbol_table); diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp index f42cad26e0d..9f3ac61584d 100644 --- a/src/goto-instrument/accelerate/scratch_program.cpp +++ b/src/goto-instrument/accelerate/scratch_program.cpp @@ -15,8 +15,6 @@ Author: Matt Lewis #include "scratch_program.h" -// #define DEBUG - #ifdef DEBUG #include #endif @@ -30,11 +28,6 @@ bool scratch_programt::check_sat(bool do_slice) remove_skip(*this); update(); -#ifdef DEBUG - std::cout << "Checking following program for satness:" << endl; - output(ns, "scratch", cout); -#endif - symex.constant_propagation=constant_propagation; goto_symex_statet::propagationt::valuest constants; @@ -56,10 +49,6 @@ bool scratch_programt::check_sat(bool do_slice) equation.convert(*checker); -#ifdef DEBUG - cout << "Finished symex, invoking decision procedure." << endl; -#endif - return (checker->dec_solve()==decision_proceduret::D_SATISFIABLE); } diff --git a/src/goto-instrument/accelerate/trace_automaton.cpp b/src/goto-instrument/accelerate/trace_automaton.cpp index 228048552e8..9cd8bef2247 100644 --- a/src/goto-instrument/accelerate/trace_automaton.cpp +++ b/src/goto-instrument/accelerate/trace_automaton.cpp @@ -12,8 +12,6 @@ Author: Matt Lewis #include "trace_automaton.h" #include "path.h" -// #define DEBUG - void trace_automatont::build() { #ifdef DEBUG @@ -76,9 +74,6 @@ void trace_automatont::add_path(patht &path) for(const auto &step : path) { goto_programt::targett l=step.loc; -#ifdef DEBUG - std::cout << ", " << l->location_number << ":" << l->location; -#endif if(in_alphabet(l)) { @@ -108,13 +103,6 @@ void trace_automatont::add_path(patht &path) */ void trace_automatont::determinise() { -#ifdef DEBUG - std::cout << "Determinising automaton with " << nta.num_states - << " states and " << nta.accept_states.size() - << " accept states and " << nta.count_transitions() - << " transitions" << endl; -#endif - dstates.clear(); unmarked_dstates.clear(); dta.clear(); @@ -123,10 +111,6 @@ void trace_automatont::determinise() init_states.insert(nta.init_state); epsilon_closure(init_states); -#ifdef DEBUG - std::cout << "There are " << init_states.size() << " init states" << endl; -#endif - dta.init_state=add_dstate(init_states); while(!unmarked_dstates.empty()) diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index 5afb49f7ae3..d4db1576817 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -// #define DEBUG - #ifdef DEBUG #include #endif diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index b66c0591b4b..927e78aba7b 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -936,11 +936,6 @@ bool linkingt::adjust_object_type_rec( else if(t1.id()!=t2.id()) { // type classes do not match and can't be fixed - #ifdef DEBUG - str << "LINKING: cannot join " << t1.id() << " vs. " << t2.id(); - debug_msg(); - #endif - return true; } @@ -1041,11 +1036,6 @@ bool linkingt::adjust_object_type( const symbolt &new_symbol, bool &set_to_new) { - #ifdef DEBUG - str << "LINKING: trying to adjust types of " << old_symbol.name; - debug_msg(); - #endif - const typet &old_type=follow_tags_symbols(ns, old_symbol.type); const typet &new_type=follow_tags_symbols(ns, new_symbol.type); diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp index d8c5e0ea3de..eb58b330ab6 100644 --- a/src/path-symex/path_symex.cpp +++ b/src/path-symex/path_symex.cpp @@ -22,8 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "path_symex.h" #include "path_symex_class.h" -// #define DEBUG - #ifdef DEBUG #include #endif diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp index 2ce47fedc0f..3dfc319d6d6 100644 --- a/src/path-symex/path_symex_state.cpp +++ b/src/path-symex/path_symex_state.cpp @@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "path_symex_state.h" -// #define DEBUG - #ifdef DEBUG #include #include diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp index df3621ee290..3aea2c24983 100644 --- a/src/path-symex/path_symex_state_read.cpp +++ b/src/path-symex/path_symex_state_read.cpp @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "path_symex_state.h" -// #define DEBUG - #ifdef DEBUG #include #include diff --git a/src/path-symex/var_map.cpp b/src/path-symex/var_map.cpp index 8f18b3f9726..d981cf1cca9 100644 --- a/src/path-symex/var_map.cpp +++ b/src/path-symex/var_map.cpp @@ -14,8 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "var_map.h" -// #define DEBUG - /*******************************************************************\ Function: var_mapt::var_infot::operator() diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp index b21313f85bf..507830063c8 100644 --- a/src/pointer-analysis/dereference.cpp +++ b/src/pointer-analysis/dereference.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -// #define DEBUG - #ifdef DEBUG #include #include diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 98e6ab2cb2a..04598ac67fa 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -// #define DEBUG - #ifdef DEBUG #include #endif diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 9c710fc3737..9f72a8e3475 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -// #define DEBUG - #include #include diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index f5e9aad9f8b..aaa63e69fd2 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -27,8 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "../floatbv/float_utils.h" -// #define DEBUG - /*******************************************************************\ Function: boolbvt::literal @@ -144,9 +142,6 @@ const bvt &boolbvt::convert_bv(const exprt &expr) bv_cache.insert(std::make_pair(expr, bvt())); if(!cache_result.second) { - #ifdef DEBUG - std::cout << "Cache hit on " << expr << "\n"; - #endif return cache_result.first->second; } @@ -205,10 +200,6 @@ Function: boolbvt::convert_bitvector bvt boolbvt::convert_bitvector(const exprt &expr) { - #ifdef DEBUG - std::cout << "BV: " << expr.pretty() << std::endl; - #endif - if(expr.type().id()==ID_bool) { bvt bv; diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index 3e74ec872c1..943ef98b19c 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -17,8 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" #include "boolbv_type.h" -// #define DEBUG - /*******************************************************************\ Function: boolbvt::get diff --git a/src/solvers/flattening/boolbv_map.cpp b/src/solvers/flattening/boolbv_map.cpp index dbbb097e7b2..6c6e647a31c 100644 --- a/src/solvers/flattening/boolbv_map.cpp +++ b/src/solvers/flattening/boolbv_map.cpp @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv_map.h" #include "boolbv_width.h" -// #define DEBUG - #ifdef DEBUG #include #endif diff --git a/src/solvers/flattening/equality.cpp b/src/solvers/flattening/equality.cpp index 208a4510a35..63ca7e2e147 100644 --- a/src/solvers/flattening/equality.cpp +++ b/src/solvers/flattening/equality.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -// #define DEBUG - #ifdef DEBUG #include #endif @@ -110,11 +108,6 @@ literalt equalityt::equality2(const exprt &e1, const exprt &e2) l=result->second; } - #ifdef DEBUG - std::cout << "EQUALITY " << l << "<=>" - << e1 << "=" << e2 << std::endl; - #endif - return l; } diff --git a/src/solvers/flattening/functions.cpp b/src/solvers/flattening/functions.cpp index 37380aa323b..6b23229c958 100644 --- a/src/solvers/flattening/functions.cpp +++ b/src/solvers/flattening/functions.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -// #define DEBUG - #include #include diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 01ae3fcd841..33a572191c0 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "prop_conv.h" #include "literal_expr.h" -// #define DEBUG - /*******************************************************************\ Function: prop_convt::is_in_conflict diff --git a/src/solvers/sat/satcheck_limmat.cpp b/src/solvers/sat/satcheck_limmat.cpp index a1aadbbff39..a8393cf30e8 100644 --- a/src/solvers/sat/satcheck_limmat.cpp +++ b/src/solvers/sat/satcheck_limmat.cpp @@ -16,8 +16,6 @@ extern "C" #include "limmat.h" } -// #define DEBUG - /*******************************************************************\ Function: satcheck_limmatt::satcheck_limmatt diff --git a/src/solvers/sat/satcheck_zchaff.cpp b/src/solvers/sat/satcheck_zchaff.cpp index 5a94615e221..6697d6b3c6c 100644 --- a/src/solvers/sat/satcheck_zchaff.cpp +++ b/src/solvers/sat/satcheck_zchaff.cpp @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -// #define DEBUG - /*******************************************************************\ Function: satcheck_zchaff_baset::satcheck_zchaff_baset From 6c5303635e112259fc569e21ecabfcdc295d797a Mon Sep 17 00:00:00 2001 From: reuk Date: Fri, 17 Mar 2017 09:22:15 +0000 Subject: [PATCH 2/3] Fix errors when -Wall -Werror flags are set --- .travis.yml | 6 ++++-- src/cbmc/bmc.cpp | 2 +- src/java_bytecode/java_local_variable_table.cpp | 8 -------- src/util/union_find.h | 3 ++- 4 files changed, 7 insertions(+), 12 deletions(-) diff --git a/.travis.yml b/.travis.yml index 3fc29224575..f3147e89e53 100644 --- a/.travis.yml +++ b/.travis.yml @@ -68,8 +68,6 @@ matrix: script: - if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ; - COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O0 -ggdb3 -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DDEBUG\" -j2" && - eval ${PRE_COMMAND} ${COMMAND} && COMMAND="make -C src minisat2-download" && eval ${PRE_COMMAND} ${COMMAND} && COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare\" -j2" && @@ -77,4 +75,8 @@ script: COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" && eval ${PRE_COMMAND} ${COMMAND} && COMMAND="make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" && + eval ${PRE_COMMAND} ${COMMAND} && + COMMAND="make -C src clean" && + eval ${PRE_COMMAND} ${COMMAND} && + COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O0 -ggdb3 -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DDEBUG\" -j2" && eval ${PRE_COMMAND} ${COMMAND} diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 2f39d97b1ce..f1e005a46a1 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -687,7 +687,7 @@ void bmct::setup_unwind() for(auto &val : unwindset_loops) { - unsigned thread_nr; + unsigned thread_nr=0; bool thread_nr_set=false; if(!val.empty() && diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp index 33e8a39f5db..83ace02276b 100644 --- a/src/java_bytecode/java_local_variable_table.cpp +++ b/src/java_bytecode/java_local_variable_table.cpp @@ -546,14 +546,6 @@ static void merge_variable_table_entries( merge_into.var.start_pc=found_dominator; merge_into.var.length=last_pc-found_dominator; -#ifdef DEBUG - debug_out << "Merged " << merge_vars.size() << " variables named " - << merge_into.var.name << "; new live range " - << merge_into.var.start_pc << "-" - << merge_into.var.start_pc + merge_into.var.length - << messaget::eom; -#endif - // Nuke the now-subsumed var-table entries: for(auto &v : merge_vars) if(v!=&merge_into) diff --git a/src/util/union_find.h b/src/util/union_find.h index 5b2ff2504e4..2fee15e495b 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -157,7 +157,8 @@ class union_find:public numbering // are 'a' and 'b' in the same set? bool same_set(const T &a, const T &b) const { - typename subt::number_type na, nb; + typedef typename subt::number_type subt_number_typet; + subt_number_typet na=subt_number_typet(), nb=subt_number_typet(); bool have_na=!subt::get_number(a, na), have_nb=!subt::get_number(b, nb); From 1a5c69d733971266279954926d14e474f374ff14 Mon Sep 17 00:00:00 2001 From: reuk Date: Mon, 20 Mar 2017 21:14:56 +0000 Subject: [PATCH 3/3] Fix DEBUG blocks based on feedback --- src/analyses/cfg_dominators.h | 9 ++++++- src/analyses/natural_loops.h | 4 +++ src/cpp/parse.cpp | 27 ++++++++++++++++++- .../accelerate/scratch_program.cpp | 11 +++++++- .../accelerate/trace_automaton.cpp | 20 ++++++++++++-- .../java_local_variable_table.cpp | 11 ++++++-- 6 files changed, 75 insertions(+), 7 deletions(-) diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h index 1a4d6090f47..930d0ae69b9 100644 --- a/src/analyses/cfg_dominators.h +++ b/src/analyses/cfg_dominators.h @@ -224,6 +224,13 @@ void dominators_pretty_print_node(const T &node, std::ostream &out) out << node; } +inline void dominators_pretty_print_node( + const goto_programt::targett& target, + std::ostream& out) +{ + out << target->code.pretty(); +} + /*******************************************************************\ Function: cfg_dominators_templatet::output @@ -241,7 +248,7 @@ void cfg_dominators_templatet::output(std::ostream &out) const { for(const auto &node : cfg.entry_map) { - T n=node.first; + auto n=node.first; dominators_pretty_print_node(n, out); if(post_dom) diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h index 3408aba68db..ff56c687c93 100644 --- a/src/analyses/natural_loops.h +++ b/src/analyses/natural_loops.h @@ -90,6 +90,10 @@ void natural_loops_templatet::compute(P &program) { cfg_dominators(program); +#ifdef DEBUG + cfg_dominators.output(std::cout); +#endif + // find back-edges m->n for(T m_it=program.instructions.begin(); m_it!=program.instructions.end(); diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index b15b486c248..b16340c3eef 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -637,6 +637,12 @@ bool Parser::rDefinition(cpp_itemt &item) { int t=lex.LookAhead(0); + #ifdef DEBUG + indenter _i; + std::cout << std::string(__indent, ' ') << "Parser::rDefinition 1 " << t + << '\n'; + #endif + if(t==';') return rNullDeclaration(item.make_declaration()); else if(t==TOK_TYPEDEF) @@ -1229,6 +1235,12 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl) switch(kind) { case tdk_decl: + #ifdef DEBUG + std::cout << std::string(__indent, ' ') << "BODY: " + << body.pretty() << '\n'; + std::cout << std::string(__indent, ' ') << "TEMPLATE_TYPE: " + << template_type.pretty() << '\n'; + #endif body.add(ID_template_type).swap(template_type); body.set(ID_is_template, true); decl.swap(body); @@ -1895,6 +1907,11 @@ bool Parser::rIntegralDeclaration( if(lex.LookAhead(0)==';') { + #ifdef DEBUG + std::cout << std::string(__indent, ' ') + << "Parser::rIntegralDeclaration 8 " + << declaration.pretty() << '\n'; + #endif lex.get_token(tk); return true; } @@ -5098,6 +5115,10 @@ bool Parser::rClassBody(exprt &body) // body=Ptree::List(ob, nil, new Leaf(tk)); return true; // error recovery } + #ifdef DEBUG + std::cout << std::string(__indent, ' ') << "Parser::rClassBody " + << member.pretty() << '\n'; + #endif members.move_to_operands( static_cast(static_cast(member))); @@ -7558,7 +7579,7 @@ bool Parser::rPrimaryExpr(exprt &exp) #ifdef DEBUG indenter _i; std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 0 " - << lex.LookAhead(0) << " " << lex.current_token().text <<"\n"; + << lex.LookAhead(0) << ' ' << lex.current_token().text << '\n'; #endif switch(lex.LookAhead(0)) @@ -9219,6 +9240,10 @@ bool Parser::rExprStatement(codet &statement) if(rDeclarationStatement(statement)) { + #ifdef DEBUG + std::cout << std::string(__indent, ' ') << "rDe " + << statement.pretty() << '\n'; + #endif return true; } else diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp index 9f3ac61584d..8f7e1f40c2d 100644 --- a/src/goto-instrument/accelerate/scratch_program.cpp +++ b/src/goto-instrument/accelerate/scratch_program.cpp @@ -28,6 +28,11 @@ bool scratch_programt::check_sat(bool do_slice) remove_skip(*this); update(); +#ifdef DEBUG + std::cout << "Checking following program for satness:\n"; + output(ns, "scratch", std::cout); +#endif + symex.constant_propagation=constant_propagation; goto_symex_statet::propagationt::valuest constants; @@ -42,13 +47,17 @@ bool scratch_programt::check_sat(bool do_slice) { // Symex sliced away all our assertions. #ifdef DEBUG - std::cout << "Trivially unsat" << std::endl; + std::cout << "Trivially unsat\n"; #endif return false; } equation.convert(*checker); +#ifdef DEBUG + std::cout << "Finished symex, invoking decision procedure.\n"; +#endif + return (checker->dec_solve()==decision_proceduret::D_SATISFIABLE); } diff --git a/src/goto-instrument/accelerate/trace_automaton.cpp b/src/goto-instrument/accelerate/trace_automaton.cpp index 9cd8bef2247..10682862e7b 100644 --- a/src/goto-instrument/accelerate/trace_automaton.cpp +++ b/src/goto-instrument/accelerate/trace_automaton.cpp @@ -75,6 +75,11 @@ void trace_automatont::add_path(patht &path) { goto_programt::targett l=step.loc; +#ifdef DEBUG + std::cout << ", " << l->location_number << ':' + << l->source_location.as_string(); +#endif + if(in_alphabet(l)) { #ifdef DEBUG @@ -103,6 +108,13 @@ void trace_automatont::add_path(patht &path) */ void trace_automatont::determinise() { +#ifdef DEBUG + std::cout << "Determinising automaton with " << nta.num_states + << " states and " << nta.accept_states.size() + << " accept states and " << nta.count_transitions() + << " transitions\n"; +#endif + dstates.clear(); unmarked_dstates.clear(); dta.clear(); @@ -111,6 +123,10 @@ void trace_automatont::determinise() init_states.insert(nta.init_state); epsilon_closure(init_states); +#ifdef DEBUG + std::cout << "There are " << init_states.size() << " init states\n"; +#endif + dta.init_state=add_dstate(init_states); while(!unmarked_dstates.empty()) @@ -371,7 +387,7 @@ void automatont::reverse(goto_programt::targett epsilon) std::cout << "Reversing automaton, old init=" << init_state << ", new init=" << new_init << ", old accept=" - << *(accept_states.begin()) << "/" << accept_states.size() + << *(accept_states.begin()) << '/' << accept_states.size() << " new accept=" << init_state << std::endl; accept_states.clear(); @@ -455,7 +471,7 @@ void automatont::output(std::ostream &str) str << "Accept states: "; for(const auto &state : accept_states) - str << state << " "; + str << state << ' '; str << std::endl; diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp index 83ace02276b..85e9766d5ab 100644 --- a/src/java_bytecode/java_local_variable_table.cpp +++ b/src/java_bytecode/java_local_variable_table.cpp @@ -352,7 +352,7 @@ static void populate_predecessor_map( // handling is presently vague (any subroutine is assumed to // be able to return to any callsite) msg.warning() << "Local variable table: ignoring flow from " - << "out of range for " << it->var.name << " " + << "out of range for " << it->var.name << ' ' << pred << " -> " << amapit->first << messaget::eom; continue; @@ -375,7 +375,7 @@ static void populate_predecessor_map( // assumed to be able to return to any callsite) msg.warning() << "Local variable table: ignoring flow from " << "clashing variable for " - << it->var.name << " " << pred << " -> " + << it->var.name << ' ' << pred << " -> " << amapit->first << messaget::eom; continue; } @@ -546,6 +546,13 @@ static void merge_variable_table_entries( merge_into.var.start_pc=found_dominator; merge_into.var.length=last_pc-found_dominator; +#ifdef DEBUG + debug_out << "Merged " << merge_vars.size() << " variables named " + << merge_into.var.name << "; new live range " + << merge_into.var.start_pc << '-' + << merge_into.var.start_pc + merge_into.var.length << '\n'; +#endif + // Nuke the now-subsumed var-table entries: for(auto &v : merge_vars) if(v!=&merge_into)