From 40fe0f8691f5ac4820db1abdef89736ada952ebc Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 Aug 2017 16:11:37 +0100 Subject: [PATCH 1/6] simplify API of goto_convert --- src/goto-programs/goto_convert_functions.cpp | 9 --------- src/goto-programs/goto_convert_functions.h | 6 ------ 2 files changed, 15 deletions(-) diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 5a35d5e2ef7..58d03a16cef 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -221,15 +221,6 @@ void goto_convert_functionst::convert_function(const irep_idt &identifier) f.make_hidden(); } -void goto_convert( - symbol_tablet &symbol_table, - goto_modelt &goto_model, - message_handlert &message_handler) -{ - goto_convert(symbol_table, goto_model.goto_functions, message_handler); - goto_model.symbol_table.swap(symbol_table); -} - void goto_convert( goto_modelt &goto_model, message_handlert &message_handler) diff --git a/src/goto-programs/goto_convert_functions.h b/src/goto-programs/goto_convert_functions.h index 85de9a67b97..3162b453d0f 100644 --- a/src/goto-programs/goto_convert_functions.h +++ b/src/goto-programs/goto_convert_functions.h @@ -23,12 +23,6 @@ void goto_convert( goto_functionst &functions, message_handlert &); -// confusing, will go away -void goto_convert( - symbol_tablet &symbol_table, - goto_modelt &dest, - message_handlert &); - // convert it all! void goto_convert( goto_modelt &, From 9469552599fd00d715b1b8b05b8c54e4d449f043 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 25 Aug 2017 15:31:21 +0100 Subject: [PATCH 2/6] use initialize_goto_model in CBMC/goto-analyse/etc --- src/analyses/call_graph.cpp | 4 +- src/analyses/call_graph.h | 4 +- src/analyses/constant_propagator.h | 8 +- src/analyses/custom_bitvector_analysis.cpp | 7 +- src/analyses/custom_bitvector_analysis.h | 3 +- src/analyses/escape_analysis.cpp | 7 +- src/analyses/escape_analysis.h | 4 +- src/analyses/goto_rw.h | 8 +- src/analyses/interval_analysis.cpp | 9 +- src/analyses/interval_analysis.h | 7 +- src/analyses/is_threaded.h | 8 +- src/analyses/natural_loops.cpp | 4 +- src/analyses/natural_loops.h | 5 +- src/cbmc/bmc.h | 3 +- src/cbmc/cbmc_parse_options.cpp | 310 ++++++--------- src/cbmc/cbmc_parse_options.h | 34 +- src/clobber/clobber_parse_options.cpp | 156 +------- src/clobber/clobber_parse_options.h | 10 +- .../goto_analyzer_parse_options.cpp | 2 +- .../goto_analyzer_parse_options.h | 9 +- src/goto-cc/compile.h | 3 +- src/goto-diff/goto_diff_parse_options.cpp | 4 +- src/goto-instrument/accelerate/accelerate.cpp | 7 +- src/goto-instrument/accelerate/accelerate.h | 14 +- src/goto-instrument/branch.cpp | 9 +- src/goto-instrument/branch.h | 7 +- src/goto-instrument/call_sequences.cpp | 22 +- src/goto-instrument/call_sequences.h | 11 +- src/goto-instrument/code_contracts.cpp | 6 +- src/goto-instrument/code_contracts.h | 7 +- src/goto-instrument/concurrency.cpp | 7 +- src/goto-instrument/concurrency.h | 7 +- src/goto-instrument/count_eloc.cpp | 24 +- src/goto-instrument/count_eloc.h | 10 +- src/goto-instrument/document_properties.cpp | 10 +- src/goto-instrument/document_properties.h | 6 +- src/goto-instrument/dot.cpp | 22 +- src/goto-instrument/dot.h | 7 +- src/goto-instrument/function.cpp | 16 +- src/goto-instrument/function.h | 10 +- .../goto_instrument_parse_options.cpp | 369 ++++++++---------- .../goto_instrument_parse_options.h | 7 +- src/goto-instrument/havoc_loops.cpp | 6 +- src/goto-instrument/havoc_loops.h | 4 +- src/goto-instrument/horn_encoding.cpp | 3 +- src/goto-instrument/horn_encoding.h | 5 +- src/goto-instrument/interrupt.cpp | 15 +- src/goto-instrument/interrupt.h | 8 +- src/goto-instrument/k_induction.cpp | 4 +- src/goto-instrument/k_induction.h | 4 +- src/goto-instrument/mmio.cpp | 13 +- src/goto-instrument/mmio.h | 8 +- src/goto-instrument/model_argc_argv.cpp | 39 +- src/goto-instrument/model_argc_argv.h | 8 +- src/goto-instrument/nondet_static.h | 6 - src/goto-instrument/nondet_volatile.cpp | 10 +- src/goto-instrument/nondet_volatile.h | 10 +- src/goto-instrument/points_to.h | 6 +- src/goto-instrument/race_check.cpp | 16 +- src/goto-instrument/race_check.h | 13 +- src/goto-instrument/reachability_slicer.cpp | 8 +- src/goto-instrument/reachability_slicer.h | 9 +- src/goto-instrument/remove_function.cpp | 20 +- src/goto-instrument/remove_function.h | 13 +- src/goto-instrument/rw_set.h | 11 +- src/goto-instrument/show_locations.cpp | 11 +- src/goto-instrument/show_locations.h | 4 +- src/goto-instrument/skip_loops.cpp | 8 +- src/goto-instrument/skip_loops.h | 6 +- src/goto-instrument/stack_depth.cpp | 20 +- src/goto-instrument/stack_depth.h | 6 +- .../thread_instrumentation.cpp | 24 +- src/goto-instrument/thread_instrumentation.h | 7 +- src/goto-instrument/undefined_functions.cpp | 21 +- src/goto-instrument/undefined_functions.h | 10 +- src/goto-instrument/uninitialized.cpp | 15 +- src/goto-instrument/uninitialized.h | 9 +- src/goto-instrument/unwind.h | 25 +- src/goto-instrument/wmm/goto2graph.h | 12 +- .../wmm/instrumenter_pensieve.h | 8 +- src/goto-instrument/wmm/weak_memory.cpp | 29 +- src/goto-instrument/wmm/weak_memory.h | 19 +- src/goto-programs/goto_inline.cpp | 15 +- src/goto-programs/goto_inline.h | 3 +- src/goto-programs/goto_trace.h | 7 +- src/goto-programs/initialize_goto_model.cpp | 4 + src/goto-programs/interpreter.cpp | 24 +- src/goto-programs/interpreter.h | 7 +- src/goto-programs/read_goto_binary.h | 4 +- src/goto-programs/remove_exceptions.cpp | 6 +- src/goto-programs/remove_returns.cpp | 8 +- src/goto-programs/remove_returns.h | 2 + .../remove_static_init_loops.cpp | 8 +- src/goto-programs/remove_static_init_loops.h | 9 +- src/goto-programs/show_goto_functions.h | 6 - src/goto-programs/show_properties.h | 6 - src/goto-programs/slice_global_inits.cpp | 7 +- src/goto-programs/slice_global_inits.h | 7 +- src/goto-programs/write_goto_binary.cpp | 39 +- src/goto-programs/write_goto_binary.h | 17 +- src/goto-symex/precondition.cpp | 3 +- src/musketeer/fence_shared.cpp | 42 +- src/musketeer/fence_shared.h | 24 +- src/musketeer/fencer.cpp | 14 +- src/musketeer/fencer.h | 10 +- src/musketeer/musketeer_parse_options.cpp | 66 ++-- src/musketeer/musketeer_parse_options.h | 8 +- src/musketeer/pensieve.cpp | 15 +- src/musketeer/pensieve.h | 6 +- .../propagate_const_function_pointers.cpp | 21 +- .../propagate_const_function_pointers.h | 8 +- src/musketeer/replace_async.h | 13 +- .../goto_program_dereference.cpp | 10 +- .../goto_program_dereference.h | 33 +- src/pointer-analysis/show_value_sets.cpp | 11 +- src/pointer-analysis/show_value_sets.h | 14 +- src/solvers/refinement/bv_refinement.h | 2 +- src/solvers/refinement/string_refinement.h | 2 +- src/symex/symex_parse_options.cpp | 35 +- src/symex/symex_parse_options.h | 7 +- 120 files changed, 929 insertions(+), 1254 deletions(-) diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp index bed00fd7f06..dd2d5b275fd 100644 --- a/src/analyses/call_graph.cpp +++ b/src/analyses/call_graph.cpp @@ -18,9 +18,9 @@ call_grapht::call_grapht() { } -call_grapht::call_grapht(const goto_functionst &goto_functions) +call_grapht::call_grapht(const goto_modelt &goto_model) { - forall_goto_functions(f_it, goto_functions) + forall_goto_functions(f_it, goto_model.goto_functions) { const goto_programt &body=f_it->second.body; add(f_it->first, body); diff --git a/src/analyses/call_graph.h b/src/analyses/call_graph.h index 79e1c03b1aa..ea4539147fd 100644 --- a/src/analyses/call_graph.h +++ b/src/analyses/call_graph.h @@ -15,13 +15,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include class call_grapht { public: call_grapht(); - explicit call_grapht(const goto_functionst &); + explicit call_grapht(const goto_modelt &); void output_dot(std::ostream &out) const; void output(std::ostream &out) const; diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 0b54c79bdb8..0e2e65383a3 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -110,11 +110,11 @@ class constant_propagator_ait:public ait { public: constant_propagator_ait( - goto_functionst &goto_functions, - const namespacet &ns) + goto_modelt &goto_model) { - operator()(goto_functions, ns); - replace(goto_functions, ns); + const namespacet ns(goto_model.symbol_table); + operator()(goto_model.goto_functions, ns); + replace(goto_model.goto_functions, ns); } constant_propagator_ait( diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index a81a08e6e67..b241150d7ba 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -682,14 +682,13 @@ void custom_bitvector_analysist::instrument(goto_functionst &) } void custom_bitvector_analysist::check( - const namespacet &ns, - const goto_functionst &goto_functions, + const goto_modelt &goto_model, bool use_xml, std::ostream &out) { unsigned pass=0, fail=0, unknown=0; - forall_goto_functions(f_it, goto_functions) + forall_goto_functions(f_it, goto_model.goto_functions) { if(!f_it->second.body.has_assertion()) continue; @@ -715,6 +714,7 @@ void custom_bitvector_analysist::check( continue; exprt tmp=eval(i_it->guard, i_it); + const namespacet ns(goto_model.symbol_table); result=simplify_expr(tmp, ns); description=i_it->source_location.get_comment(); @@ -744,6 +744,7 @@ void custom_bitvector_analysist::check( if(!description.empty()) out << ", " << description; out << ": "; + const namespacet ns(goto_model.symbol_table); out << from_expr(ns, f_it->first, result); out << '\n'; } diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index 5ef03adbaf2..f0c298f84d6 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -128,8 +128,7 @@ class custom_bitvector_analysist:public ait public: void instrument(goto_functionst &); void check( - const namespacet &, - const goto_functionst &, + const goto_modelt &, bool xml, std::ostream &); exprt eval(const exprt &src, locationt loc) diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index a9b7c71db08..b0129dfd0a6 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -436,10 +436,11 @@ void escape_analysist::insert_cleanup( } void escape_analysist::instrument( - goto_functionst &goto_functions, - const namespacet &ns) + goto_modelt &goto_model) { - Forall_goto_functions(f_it, goto_functions) + const namespacet ns(goto_model.symbol_table); + + Forall_goto_functions(f_it, goto_model.goto_functions) { Forall_goto_program_instructions(i_it, f_it->second.body) { diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h index 00f865b45e4..7a4c606e1d4 100644 --- a/src/analyses/escape_analysis.h +++ b/src/analyses/escape_analysis.h @@ -95,9 +95,7 @@ class escape_domaint:public ai_domain_baset class escape_analysist:public ait { public: - void instrument( - goto_functionst &, - const namespacet &); + void instrument(goto_modelt &); protected: virtual void initialize(const goto_functionst &_goto_functions) diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h index 38bc4d2e61a..02f17a7af16 100644 --- a/src/analyses/goto_rw.h +++ b/src/analyses/goto_rw.h @@ -19,7 +19,7 @@ Date: April 2010 #include -#include +#include #define forall_rw_range_set_r_objects(it, rw_set) \ for(rw_range_sett::objectst::const_iterator it=(rw_set).get_r_set().begin(); \ @@ -30,15 +30,15 @@ Date: April 2010 it!=(rw_set).get_w_set().end(); ++it) class rw_range_sett; -class goto_functionst; +class goto_modelt; void goto_rw(goto_programt::const_targett target, rw_range_sett &rw_set); -void goto_rw(const goto_programt &goto_program, +void goto_rw(const goto_programt &, rw_range_sett &rw_set); -void goto_rw(const goto_functionst &goto_functions, +void goto_rw(const goto_functionst &, const irep_idt &function, rw_range_sett &rw_set); diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp index c6d739c8bfd..f3c0247a9bb 100644 --- a/src/analyses/interval_analysis.cpp +++ b/src/analyses/interval_analysis.cpp @@ -76,14 +76,13 @@ void instrument_intervals( } } -void interval_analysis( - const namespacet &ns, - goto_functionst &goto_functions) +void interval_analysis(goto_modelt &goto_model) { ait interval_analysis; - interval_analysis(goto_functions, ns); + const namespacet ns(goto_model.symbol_table); + interval_analysis(goto_model.goto_functions, ns); - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) instrument_intervals(interval_analysis, f_it->second); } diff --git a/src/analyses/interval_analysis.h b/src/analyses/interval_analysis.h index 1c85fc9a193..1b1b7c07e79 100644 --- a/src/analyses/interval_analysis.h +++ b/src/analyses/interval_analysis.h @@ -12,11 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANALYSES_INTERVAL_ANALYSIS_H #define CPROVER_ANALYSES_INTERVAL_ANALYSIS_H -#include -#include +class goto_modelt; -void interval_analysis( - const namespacet &ns, - goto_functionst &goto_functions); +void interval_analysis(goto_modelt &); #endif // CPROVER_ANALYSES_INTERVAL_ANALYSIS_H diff --git a/src/analyses/is_threaded.h b/src/analyses/is_threaded.h index 5a3823b867e..c5cf48a559c 100644 --- a/src/analyses/is_threaded.h +++ b/src/analyses/is_threaded.h @@ -16,7 +16,7 @@ Date: October 2012 #include -#include +#include class is_threadedt { @@ -27,6 +27,12 @@ class is_threadedt compute(goto_functions); } + explicit is_threadedt( + const goto_modelt &goto_model) + { + compute(goto_model.goto_functions); + } + bool operator()(const goto_programt::const_targett t) const { return is_threaded_set.find(t)!=is_threaded_set.end(); diff --git a/src/analyses/natural_loops.cpp b/src/analyses/natural_loops.cpp index 7101613e417..00ece2cf213 100644 --- a/src/analyses/natural_loops.cpp +++ b/src/analyses/natural_loops.cpp @@ -13,9 +13,9 @@ Author: Georg Weissenbacher, georg@weissenbacher.name #include -void show_natural_loops(const goto_functionst &goto_functions) +void show_natural_loops(const goto_modelt &goto_model) { - forall_goto_functions(it, goto_functions) + forall_goto_functions(it, goto_model.goto_functions) { std::cout << "*** " << it->first << '\n'; diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h index 9eb24ccc0ed..8fb41d7e1d2 100644 --- a/src/analyses/natural_loops.h +++ b/src/analyses/natural_loops.h @@ -16,8 +16,7 @@ Author: Georg Weissenbacher, georg@weissenbacher.name #include #include -#include -#include +#include #include "cfg_dominators.h" @@ -70,7 +69,7 @@ class natural_loopst: typedef natural_loops_templatet natural_loops_mutablet; -void show_natural_loops(const goto_functionst &goto_functions); +void show_natural_loops(const goto_modelt &); /// Finds all back-edges and computes the natural loops #ifdef DEBUG diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 4c69fab527c..6c9a5c6bd31 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -23,7 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include + #include #include diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index ed6f3f081a2..a3fbd8c99dc 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -25,7 +25,14 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include +#include #include +#include +#include +#include +#include +#include #include #include #include @@ -35,20 +42,15 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include -#include -#include -#include +#include #include -#include +#include +#include +#include #include #include -#include -#include -#include -#include -#include -#include #include #include @@ -71,7 +73,7 @@ Author: Daniel Kroening, kroening@kroening.com cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv): parse_options_baset(CBMC_OPTIONS, argc, argv), xml_interfacet(cmdline), - language_uit(cmdline, ui_message_handler), + messaget(ui_message_handler), ui_message_handler(cmdline, "CBMC " CBMC_VERSION) { } @@ -82,7 +84,7 @@ ::cbmc_parse_optionst::cbmc_parse_optionst( const std::string &extra_options): parse_options_baset(CBMC_OPTIONS+extra_options, argc, argv), xml_interfacet(cmdline), - language_uit(cmdline, ui_message_handler), + messaget(ui_message_handler), ui_message_handler(cmdline, "CBMC " CBMC_VERSION) { } @@ -470,7 +472,7 @@ int cbmc_parse_optionst::doit() register_languages(); if(cmdline.isset("test-preprocessor")) - return test_c_preprocessor(ui_message_handler)?8:0; + return test_c_preprocessor(get_message_handler())?8:0; if(cmdline.isset("preprocess")) { @@ -478,12 +480,56 @@ int cbmc_parse_optionst::doit() return 0; // should contemplate EX_OK from sysexits.h } - goto_functionst goto_functions; + if(cmdline.isset("show-parse-tree")) + { + if(cmdline.args.size()!=1 || + is_goto_binary(cmdline.args[0])) + { + error() << "Please give exactly one source file" << eom; + return 6; + } + + std::string filename=cmdline.args[0]; + + #ifdef _MSC_VER + std::ifstream infile(widen(filename)); + #else + std::ifstream infile(filename); + #endif + + if(!infile) + { + error() << "failed to open input file `" + << filename << "'" << eom; + return 6; + } + + std::unique_ptr language= + get_language_from_filename(filename); + + if(language==nullptr) + { + error() << "failed to figure out type of file `" + << filename << "'" << eom; + return 6; + } + + language->get_language_options(cmdline); + language->set_message_handler(get_message_handler()); + + status() << "Parsing " << filename << eom; + + if(language->parse(infile, filename)) + { + error() << "PARSING ERROR" << eom; + return 6; + } - expr_listt bmc_constraints; + language->show_parse(std::cout); + return 0; + } - int get_goto_program_ret= - get_goto_program(options, bmc_constraints, goto_functions); + int get_goto_program_ret=get_goto_program(options); if(get_goto_program_ret!=-1) return get_goto_program_ret; @@ -491,26 +537,24 @@ int cbmc_parse_optionst::doit() if(cmdline.isset("show-claims") || // will go away cmdline.isset("show-properties")) // use this one { - const namespacet ns(symbol_table); - show_properties(ns, get_ui(), goto_functions); + show_properties(goto_model, ui_message_handler.get_ui()); return 0; // should contemplate EX_OK from sysexits.h } - if(set_properties(goto_functions)) + if(set_properties()) return 7; // should contemplate EX_USAGE from sysexits.h // unwinds loops to number of enum elements // side effect: add this as explicit unwind to unwind set if(options.get_bool_option("java-unwind-enum-static")) - remove_static_init_loops( - symbol_table, - goto_functions, - options, - ui_message_handler); + remove_static_init_loops(goto_model, options, get_message_handler()); // get solver - cbmc_solverst cbmc_solvers(options, symbol_table, ui_message_handler); - cbmc_solvers.set_ui(get_ui()); + cbmc_solverst cbmc_solvers( + options, + goto_model.symbol_table, + get_message_handler()); + cbmc_solvers.set_ui(ui_message_handler.get_ui()); std::unique_ptr cbmc_solver; @@ -527,21 +571,25 @@ int cbmc_parse_optionst::doit() prop_convt &prop_conv=cbmc_solver->prop_conv(); - bmct bmc(options, symbol_table, ui_message_handler, prop_conv); + bmct bmc( + options, + goto_model.symbol_table, + get_message_handler(), + prop_conv); // do actual BMC - return do_bmc(bmc, goto_functions); + return do_bmc(bmc); } -bool cbmc_parse_optionst::set_properties(goto_functionst &goto_functions) +bool cbmc_parse_optionst::set_properties() { try { if(cmdline.isset("claim")) // will go away - ::set_properties(goto_functions, cmdline.get_values("claim")); + ::set_properties(goto_model, cmdline.get_values("claim")); if(cmdline.isset("property")) // use this one - ::set_properties(goto_functions, cmdline.get_values("property")); + ::set_properties(goto_model, cmdline.get_values("property")); } catch(const char *e) @@ -565,9 +613,7 @@ bool cbmc_parse_optionst::set_properties(goto_functionst &goto_functions) } int cbmc_parse_optionst::get_goto_program( - const optionst &options, - expr_listt &bmc_constraints, // for get_modules - goto_functionst &goto_functions) + const optionst &options) { if(cmdline.args.empty()) { @@ -577,127 +623,29 @@ int cbmc_parse_optionst::get_goto_program( try { - if(cmdline.isset("show-parse-tree")) - { - if(cmdline.args.size()!=1 || - is_goto_binary(cmdline.args[0])) - { - error() << "Please give exactly one source file" << eom; - return 6; - } - - std::string filename=cmdline.args[0]; - - #ifdef _MSC_VER - std::ifstream infile(widen(filename)); - #else - std::ifstream infile(filename); - #endif - - if(!infile) - { - error() << "failed to open input file `" - << filename << "'" << eom; - return 6; - } - - std::unique_ptr language=get_language_from_filename(filename); - language->get_language_options(cmdline); - - if(language==nullptr) - { - error() << "failed to figure out type of file `" - << filename << "'" << eom; - return 6; - } - - language->set_message_handler(get_message_handler()); - - status() << "Parsing " << filename << eom; - - if(language->parse(infile, filename)) - { - error() << "PARSING ERROR" << eom; - return 6; - } - - language->show_parse(std::cout); - return 0; - } - - cmdlinet::argst binaries; - binaries.reserve(cmdline.args.size()); - - for(cmdlinet::argst::iterator - it=cmdline.args.begin(); - it!=cmdline.args.end(); - ) // no ++it - { - if(is_goto_binary(*it)) - { - binaries.push_back(*it); - it=cmdline.args.erase(it); - continue; - } - - ++it; - } - - if(!cmdline.args.empty()) - { - if(parse()) - return 6; - if(typecheck()) - return 6; - int get_modules_ret=get_modules(bmc_constraints); - 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(); - } - - for(const auto &bin : binaries) - { - status() << "Reading GOTO program from file " << eom; - - if(read_object_and_link( - bin, - symbol_table, - goto_functions, - get_message_handler())) - { - return 6; - } - } + if(initialize_goto_model(goto_model, cmdline, get_message_handler())) + return 6; if(cmdline.isset("show-symbol-table")) { - show_symbol_table(); + show_symbol_table(goto_model, ui_message_handler.get_ui()); return 0; } - status() << "Generating GOTO Program" << eom; - - goto_convert(symbol_table, goto_functions, ui_message_handler); - - if(process_goto_program(options, goto_functions)) + if(process_goto_program(options)) return 6; // show it? if(cmdline.isset("show-loops")) { - show_loop_ids(get_ui(), goto_functions); + show_loop_ids(ui_message_handler.get_ui(), goto_model); return 0; } // show it? if(cmdline.isset("show-goto-functions")) { - namespacet ns(symbol_table); - show_goto_functions(ns, get_ui(), goto_functions); + show_goto_functions(goto_model, ui_message_handler.get_ui()); return 0; } @@ -786,49 +734,44 @@ void cbmc_parse_optionst::preprocessing() } bool cbmc_parse_optionst::process_goto_program( - const optionst &options, - goto_functionst &goto_functions) + const optionst &options) { try { - namespacet ns(symbol_table); - // Remove inline assembler; this needs to happen before // adding the library. - remove_asm(symbol_table, goto_functions); + remove_asm(goto_model); // add the library - link_to_library(symbol_table, goto_functions, ui_message_handler); + link_to_library(goto_model, get_message_handler()); if(cmdline.isset("string-abstraction")) - string_instrumentation( - symbol_table, get_message_handler(), goto_functions); + string_instrumentation(goto_model, get_message_handler()); // remove function pointers status() << "Removal of function pointers and virtual functions" << eom; remove_function_pointers( get_message_handler(), - symbol_table, - goto_functions, + goto_model, cmdline.isset("pointer-check")); // Java virtual functions -> explicit dispatch tables: - remove_virtual_functions(symbol_table, goto_functions); + remove_virtual_functions(goto_model); // remove catch and throw (introduces instanceof) - remove_exceptions(symbol_table, goto_functions); + remove_exceptions(goto_model); // Similar removal of RTTI inspection: - remove_instanceof(symbol_table, goto_functions); + remove_instanceof(goto_model); - mm_io(symbol_table, goto_functions); + mm_io(goto_model); // do partial inlining status() << "Partial Inlining" << eom; - goto_partial_inline(goto_functions, ns, ui_message_handler); + goto_partial_inline(goto_model, get_message_handler()); // remove returns, gcc vectors, complex - remove_returns(symbol_table, goto_functions); - remove_vector(symbol_table, goto_functions); - remove_complex(symbol_table, goto_functions); - rewrite_union(goto_functions, ns); + remove_returns(goto_model); + remove_vector(goto_model); + remove_complex(goto_model); + rewrite_union(goto_model); // Similar removal of java nondet statements: // TODO Should really get this from java_bytecode_language somehow, but we @@ -841,20 +784,21 @@ bool cbmc_parse_optionst::process_goto_program( cmdline.isset("java-max-input-tree-depth") ? std::stoul(cmdline.get_value("java-max-input-tree-depth")) : MAX_NONDET_TREE_DEPTH; - replace_java_nondet(goto_functions); + + replace_java_nondet(goto_model); + convert_nondet( - goto_functions, - symbol_table, - ui_message_handler, + goto_model, + get_message_handler(), max_nondet_array_length, max_nondet_tree_depth); // add generic checks status() << "Generic Property Instrumentation" << eom; - goto_check(ns, options, goto_functions); + goto_check(options, goto_model); // checks don't know about adjusted float expressions - adjust_float_expressions(goto_functions, ns); + adjust_float_expressions(goto_model); // ignore default/user-specified initialization // of variables with static lifetime @@ -862,46 +806,44 @@ bool cbmc_parse_optionst::process_goto_program( { status() << "Adding nondeterministic initialization " "of static/global variables" << eom; - nondet_static(ns, goto_functions); + nondet_static(goto_model); } if(cmdline.isset("string-abstraction")) { status() << "String Abstraction" << eom; string_abstraction( - symbol_table, - get_message_handler(), - goto_functions); + goto_model, + get_message_handler()); } // add failed symbols // needs to be done before pointer analysis - add_failed_symbols(symbol_table); + add_failed_symbols(goto_model.symbol_table); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); // add loop ids - goto_functions.compute_loop_numbers(); + goto_model.goto_functions.compute_loop_numbers(); if(cmdline.isset("drop-unused-functions")) { // Entry point will have been set before and function pointers removed status() << "Removing unused functions" << eom; - remove_unused_functions(goto_functions, ui_message_handler); + remove_unused_functions(goto_model, get_message_handler()); } // remove skips such that trivial GOTOs are deleted and not considered // for coverage annotation: - remove_skip(goto_functions); + remove_skip(goto_model); // instrument cover goals if(cmdline.isset("cover")) { if(instrument_cover_goals( cmdline, - symbol_table, - goto_functions, + goto_model, get_message_handler())) return true; } @@ -911,21 +853,21 @@ bool cbmc_parse_optionst::process_goto_program( // before using the argument of the "property" option. // Do not re-label after using the property slicer because // this would cause the property identifiers to change. - label_properties(goto_functions); + label_properties(goto_model); // full slice? if(cmdline.isset("full-slice")) { status() << "Performing a full slice" << eom; if(cmdline.isset("property")) - property_slicer(goto_functions, ns, cmdline.get_values("property")); + property_slicer(goto_model, cmdline.get_values("property")); else - full_slicer(goto_functions, ns); + full_slicer(goto_model); } // remove any skips introduced since coverage instrumentation - remove_skip(goto_functions); - goto_functions.update(); + remove_skip(goto_model); + goto_model.goto_functions.update(); } catch(const char *e) @@ -955,16 +897,14 @@ bool cbmc_parse_optionst::process_goto_program( } /// invoke main modules -int cbmc_parse_optionst::do_bmc( - bmct &bmc, - const goto_functionst &goto_functions) +int cbmc_parse_optionst::do_bmc(bmct &bmc) { - bmc.set_ui(get_ui()); + bmc.set_ui(ui_message_handler.get_ui()); int result=6; // do actual BMC - switch(bmc.run(goto_functions)) + switch(bmc.run(goto_model.goto_functions)) { case safety_checkert::resultt::SAFE: result=0; diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index ef91683ee0e..33c5dca4602 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -74,7 +74,7 @@ class optionst; class cbmc_parse_optionst: public parse_options_baset, public xml_interfacet, - public language_uit + public messaget { public: virtual int doit() override; @@ -87,35 +87,17 @@ class cbmc_parse_optionst: const std::string &extra_options); protected: + goto_modelt goto_model; ui_message_handlert ui_message_handler; - virtual void register_languages(); - - virtual void get_command_line_options(optionst &options); - - virtual int do_bmc( - bmct &bmc, - const goto_functionst &goto_functions); - - virtual int get_goto_program( - const optionst &options, - expr_listt &bmc_constraints, - goto_functionst &goto_functions); - - virtual bool process_goto_program( - const optionst &options, - goto_functionst &goto_functions); - - bool set_properties(goto_functionst &goto_functions); void eval_verbosity(); - - // get any additional stuff before finalizing the goto program - virtual int get_modules(expr_listt &bmc_constraints) - { - return -1; // continue - } - + void register_languages(); + void get_command_line_options(optionst &); void preprocessing(); + int get_goto_program(const optionst &); + bool process_goto_program(const optionst &); + bool set_properties(); + int do_bmc(bmct &); }; #endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index b0859362be9..5a926a71eee 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -24,7 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include #include @@ -120,34 +120,33 @@ int clobber_parse_optionst::doit() eval_verbosity(); - goto_functionst goto_functions; + goto_modelt goto_model; try { - if(get_goto_program(options, goto_functions)) + if(initialize_goto_model(goto_model, cmdline, get_message_handler())) return 6; - label_properties(goto_functions); + label_properties(goto_model); if(cmdline.isset("show-properties")) { - const namespacet ns(symbol_table); - show_properties(ns, get_ui(), goto_functions); + show_properties(goto_model, get_ui()); return 0; } - set_properties(goto_functions); + set_properties(goto_model.goto_functions); // do instrumentation - const namespacet ns(symbol_table); + const namespacet ns(goto_model.symbol_table); std::ofstream out("simulator.c"); if(!out) throw std::string("failed to create file simulator.c"); - dump_c(goto_functions, true, false, false, ns, out); + dump_c(goto_model.goto_functions, true, false, false, ns, out); status() << "instrumentation complete; compile and execute simulator.c" << eom; @@ -189,165 +188,42 @@ bool clobber_parse_optionst::set_properties(goto_functionst &goto_functions) return false; } -bool clobber_parse_optionst::get_goto_program( - const optionst &options, - goto_functionst &goto_functions) -{ - if(cmdline.args.empty()) - { - error() << "Please provide a program to verify" << eom; - return true; - } - - { - if(cmdline.args.size()==1 && - is_goto_binary(cmdline.args[0])) - { - status() << "Reading GOTO program from file" << eom; - - if(read_goto_binary(cmdline.args[0], - symbol_table, goto_functions, get_message_handler())) - return true; - - if(cmdline.isset("show-symbol-table")) - { - show_symbol_table(); - return true; - } - - irep_idt entry_point=goto_functions.entry_point(); - - if(symbol_table.symbols.find(entry_point)==symbol_table.symbols.end()) - { - error() << "The goto binary has no entry point; please complete linking" - << eom; - return true; - } - } - else if(cmdline.isset("show-parse-tree")) - { - if(cmdline.args.size()!=1) - { - error() << "Please give one source file only" << eom; - return true; - } - - std::string filename=cmdline.args[0]; - - #ifdef _MSC_VER - std::ifstream infile(widen(filename)); - #else - std::ifstream infile(filename); - #endif - - if(!infile) - { - error() << "failed to open input file `" << filename << "'" << eom; - return true; - } - - std::unique_ptr language=get_language_from_filename(filename); - language->get_language_options(cmdline); - - if(language==nullptr) - { - error() << "failed to figure out type of file `" << filename << "'" - << eom; - return true; - } - - language->set_message_handler(get_message_handler()); - - status() << "Parsing " << filename << eom; - - if(language->parse(infile, filename)) - { - error() << "PARSING ERROR" << eom; - return true; - } - - language->show_parse(std::cout); - return true; - } - else - { - if(parse() || - typecheck() || - final()) - return true; - - // we no longer need any parse trees or language files - clear_parse(); - - if(cmdline.isset("show-symbol-table")) - { - show_symbol_table(); - return true; - } - - irep_idt entry_point=goto_functions.entry_point(); - - if(symbol_table.symbols.find(entry_point)==symbol_table.symbols.end()) - { - error() << "No entry point; please provide a main function" << eom; - return true; - } - - status() << "Generating GOTO Program" << eom; - - goto_convert(symbol_table, goto_functions, ui_message_handler); - } - - // finally add the library - #if 0 - link_to_library(symbol_table, goto_functions, ui_message_handler); - #endif - - if(process_goto_program(options, goto_functions)) - return true; - } - - return false; -} - bool clobber_parse_optionst::process_goto_program( const optionst &options, - goto_functionst &goto_functions) + goto_modelt &goto_model) { { - namespacet ns(symbol_table); - // do partial inlining status() << "Partial Inlining" << eom; - goto_partial_inline(goto_functions, ns, ui_message_handler); + goto_partial_inline(goto_model, get_message_handler()); // add generic checks status() << "Generic Property Instrumentation" << eom; - goto_check(ns, options, goto_functions); + goto_check(options, goto_model); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); // add loop ids - goto_functions.compute_loop_numbers(); + goto_model.goto_functions.compute_loop_numbers(); // if we aim to cover, replace // all assertions by false to prevent simplification if(cmdline.isset("cover-assertions")) - make_assertions_false(goto_functions); + make_assertions_false(goto_model); // show it? if(cmdline.isset("show-loops")) { - show_loop_ids(get_ui(), goto_functions); + show_loop_ids(get_ui(), goto_model); return true; } // show it? if(cmdline.isset("show-goto-functions")) { - show_goto_functions(ns, get_ui(), goto_functions); + show_goto_functions(goto_model, get_ui()); return true; } } diff --git a/src/clobber/clobber_parse_options.h b/src/clobber/clobber_parse_options.h index 5148bc759af..eb543f60138 100644 --- a/src/clobber/clobber_parse_options.h +++ b/src/clobber/clobber_parse_options.h @@ -54,17 +54,13 @@ class clobber_parse_optionst: protected: ui_message_handlert ui_message_handler; - void get_command_line_options(optionst &options); - - bool get_goto_program( - const optionst &options, - goto_functionst &goto_functions); + void get_command_line_options(optionst &); bool process_goto_program( const optionst &options, - goto_functionst &goto_functions); + goto_modelt &); - bool set_properties(goto_functionst &goto_functions); + bool set_properties(goto_functionst &); void report_success(); void report_failure(); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 66d31053220..b7f0b60a1d0 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -58,7 +58,7 @@ goto_analyzer_parse_optionst::goto_analyzer_parse_optionst( int argc, const char **argv): parse_options_baset(GOTO_ANALYSER_OPTIONS, argc, argv), - language_uit(cmdline, ui_message_handler), + messaget(ui_message_handler), ui_message_handler(cmdline, "GOTO-ANALYZER " CBMC_VERSION) { } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 5d61256b1f2..3fbaab18b1b 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -15,8 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #include #include @@ -52,7 +50,7 @@ class optionst; class goto_analyzer_parse_optionst: public parse_options_baset, - public language_uit + public messaget { public: virtual int doit() override; @@ -72,6 +70,11 @@ class goto_analyzer_parse_optionst: bool set_properties(); void eval_verbosity(); + + ui_message_handlert::uit get_ui() + { + return ui_message_handler.get_ui(); + } }; #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h index b0c61d137a3..4ae2a2eb0e0 100644 --- a/src/goto-cc/compile.h +++ b/src/goto-cc/compile.h @@ -18,7 +18,7 @@ Date: June 2006 #include #include -#include +#include class compilet:public language_uit { @@ -67,6 +67,7 @@ class compilet:public language_uit const std::string &, const symbol_tablet &, goto_functionst &); + bool write_bin_object_file( const std::string &, const symbol_tablet &, diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index c0be3f06694..28a2b017ed1 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -431,14 +431,14 @@ bool goto_diff_parse_optionst::process_goto_program( // show it? if(cmdline.isset("show-loops")) { - show_loop_ids(get_ui(), goto_functions); + show_loop_ids(get_ui(), goto_model); return true; } // show it? if(cmdline.isset("show-goto-functions")) { - show_goto_functions(ns, get_ui(), goto_functions); + show_goto_functions(goto_model, get_ui()); return true; } } diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index cd74e16a9d1..199ea59de21 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -650,14 +650,13 @@ int acceleratet::accelerate_loops() void accelerate_functions( - goto_functionst &functions, - symbol_tablet &symbol_table, + goto_modelt &goto_model, bool use_z3) { - Forall_goto_functions(it, functions) + Forall_goto_functions(it, goto_model.goto_functions) { std::cout << "Accelerating function " << it->first << '\n'; - acceleratet accelerate(it->second.body, functions, symbol_table, use_z3); + acceleratet accelerate(it->second.body, goto_model, use_z3); int num_accelerated=accelerate.accelerate_loops(); diff --git a/src/goto-instrument/accelerate/accelerate.h b/src/goto-instrument/accelerate/accelerate.h index d3aac4ac124..000fec39dbb 100644 --- a/src/goto-instrument/accelerate/accelerate.h +++ b/src/goto-instrument/accelerate/accelerate.h @@ -30,13 +30,12 @@ class acceleratet { public: acceleratet(goto_programt &_program, - goto_functionst &_goto_functions, - symbol_tablet &_symbol_table, - bool _use_z3) : + goto_modelt &_goto_model, + bool _use_z3): program(_program), - goto_functions(_goto_functions), - symbol_table(_symbol_table), - ns(symbol_table), + goto_functions(_goto_model.goto_functions), + symbol_table(_goto_model.symbol_table), + ns(_goto_model.symbol_table), utils(symbol_table, goto_functions), use_z3(_use_z3) { @@ -117,8 +116,7 @@ class acceleratet }; void accelerate_functions( - goto_functionst &functions, - symbol_tablet &ns, + goto_modelt &, bool use_z3); #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H diff --git a/src/goto-instrument/branch.cpp b/src/goto-instrument/branch.cpp index e224a59265e..54abd3ed07e 100644 --- a/src/goto-instrument/branch.cpp +++ b/src/goto-instrument/branch.cpp @@ -17,11 +17,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "function.h" void branch( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &goto_model, const irep_idt &id) { - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) { // don't instrument our internal functions if(has_prefix(id2string(f_it->first), CPROVER_PREFIX)) @@ -53,7 +52,7 @@ void branch( goto_programt::targett t1=body.insert_after(i_it); t1->make_function_call( - function_to_call(symbol_table, id, "taken")); + function_to_call(goto_model.symbol_table, id, "taken")); t1->function=f_it->first; goto_programt::targett t2=body.insert_after(t1); @@ -62,7 +61,7 @@ void branch( goto_programt::targett t3=body.insert_after(t2); t3->make_function_call( - function_to_call(symbol_table, id, "not-taken")); + function_to_call(goto_model.symbol_table, id, "not-taken")); t3->function=f_it->first; i_it->targets.clear(); i_it->targets.push_back(t3); diff --git a/src/goto-instrument/branch.h b/src/goto-instrument/branch.h index 842f3092b7a..dd6f1d2d85d 100644 --- a/src/goto-instrument/branch.h +++ b/src/goto-instrument/branch.h @@ -12,11 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_BRANCH_H #define CPROVER_GOTO_INSTRUMENT_BRANCH_H -#include +#include + +class goto_modelt; void branch( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &, const irep_idt &id); #endif // CPROVER_GOTO_INSTRUMENT_BRANCH_H diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index 7c8ed65a918..29236975364 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -20,6 +20,8 @@ Date: April 2013 #include #include +#include + void show_call_sequences( const irep_idt &function, const goto_programt &goto_program, @@ -97,11 +99,11 @@ void show_call_sequences( std::cout << '\n'; } -void show_call_sequences(const goto_functionst &goto_functions) +void show_call_sequences(const goto_modelt &goto_model) { // do per function - forall_goto_functions(f_it, goto_functions) + forall_goto_functions(f_it, goto_model.goto_functions) show_call_sequences(f_it->first, f_it->second.body); } @@ -109,9 +111,9 @@ class check_call_sequencet { public: explicit check_call_sequencet( - const goto_functionst &_goto_functions, + const goto_modelt &_goto_model, const std::vector &_sequence): - goto_functions(_goto_functions), + goto_functions(_goto_model.goto_functions), sequence(_sequence) { } @@ -281,7 +283,7 @@ void check_call_sequencet::operator()() std::cout << "sequence not feasible\n"; } -void check_call_sequence(const goto_functionst &goto_functions) +void check_call_sequence(const goto_modelt &goto_model) { // read the sequence from stdin @@ -297,7 +299,7 @@ void check_call_sequence(const goto_functionst &goto_functions) sequence.push_back(line); } - check_call_sequencet(goto_functions, sequence)(); + check_call_sequencet(goto_model, sequence)(); } static void list_calls_and_arguments( @@ -346,12 +348,12 @@ static void list_calls_and_arguments( } } -void list_calls_and_arguments( - const namespacet &ns, - const goto_functionst &goto_functions) +void list_calls_and_arguments(const goto_modelt &goto_model) { // do per function - forall_goto_functions(f_it, goto_functions) + const namespacet ns(goto_model.symbol_table); + + forall_goto_functions(f_it, goto_model.goto_functions) list_calls_and_arguments(ns, f_it->first, f_it->second.body); } diff --git a/src/goto-instrument/call_sequences.h b/src/goto-instrument/call_sequences.h index 7d432ddbb4b..55cd164b252 100644 --- a/src/goto-instrument/call_sequences.h +++ b/src/goto-instrument/call_sequences.h @@ -14,13 +14,10 @@ Date: September 2011 #ifndef CPROVER_GOTO_INSTRUMENT_CALL_SEQUENCES_H #define CPROVER_GOTO_INSTRUMENT_CALL_SEQUENCES_H -#include +class goto_modelt; -void show_call_sequences(const goto_functionst &goto_functions); -void check_call_sequence(const goto_functionst &goto_functions); - -void list_calls_and_arguments( - const namespacet &ns, - const goto_functionst &goto_functions); +void show_call_sequences(const goto_modelt &); +void check_call_sequence(const goto_modelt &); +void list_calls_and_arguments(const goto_modelt &); #endif // CPROVER_GOTO_INSTRUMENT_CALL_SEQUENCES_H diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 5b118d36455..a33b0934349 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -400,9 +400,7 @@ void code_contractst::operator()() goto_functions.update(); } -void code_contracts( - symbol_tablet &symbol_table, - goto_functionst &goto_functions) +void code_contracts(goto_modelt &goto_model) { - code_contractst(symbol_table, goto_functions)(); + code_contractst(goto_model.symbol_table, goto_model.goto_functions)(); } diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index 006f4702480..dc02902c142 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -14,11 +14,8 @@ Date: February 2016 #ifndef CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H #define CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H -class goto_functionst; -class symbol_tablet; +class goto_modelt; -void code_contracts( - symbol_tablet &symbol_table, - goto_functionst &goto_functions); +void code_contracts(goto_modelt &); #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H diff --git a/src/goto-instrument/concurrency.cpp b/src/goto-instrument/concurrency.cpp index 579edc36ed8..12f491884a7 100644 --- a/src/goto-instrument/concurrency.cpp +++ b/src/goto-instrument/concurrency.cpp @@ -222,10 +222,9 @@ void concurrency_instrumentationt::instrument( void concurrency( value_setst &value_sets, - class symbol_tablet &symbol_table, - goto_functionst &goto_functions) + goto_modelt &goto_model) { concurrency_instrumentationt concurrency_instrumentation( - value_sets, symbol_table); - concurrency_instrumentation(goto_functions); + value_sets, goto_model.symbol_table); + concurrency_instrumentation(goto_model.goto_functions); } diff --git a/src/goto-instrument/concurrency.h b/src/goto-instrument/concurrency.h index cf09d4da68b..fafe98dcac7 100644 --- a/src/goto-instrument/concurrency.h +++ b/src/goto-instrument/concurrency.h @@ -15,11 +15,8 @@ Date: February 2006 #define CPROVER_GOTO_INSTRUMENT_CONCURRENCY_H #include -#include +#include -void concurrency( - value_setst &value_sets, - class symbol_tablet &symbol_table, - goto_functionst &goto_functions); +void concurrency(value_setst &, goto_modelt &); #endif // CPROVER_GOTO_INSTRUMENT_CONCURRENCY_H diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index fa8cb858da6..ecd9c15ffbb 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -26,10 +26,10 @@ typedef std::unordered_map filest; typedef std::unordered_map working_dirst; static void collect_eloc( - const goto_functionst &goto_functions, + const goto_modelt &goto_model, working_dirst &dest) { - forall_goto_functions(f_it, goto_functions) + forall_goto_functions(f_it, goto_model.goto_functions) { forall_goto_program_instructions(it, f_it->second.body) { @@ -43,12 +43,12 @@ static void collect_eloc( } } -void count_eloc(const goto_functionst &goto_functions) +void count_eloc(const goto_modelt &goto_model) { std::size_t eloc=0; working_dirst eloc_map; - collect_eloc(goto_functions, eloc_map); + collect_eloc(goto_model, eloc_map); for(const std::pair &files : eloc_map) for(const std::pair &lines : files.second) @@ -57,10 +57,10 @@ void count_eloc(const goto_functionst &goto_functions) std::cout << "Effective lines of code: " << eloc << '\n'; } -void list_eloc(const goto_functionst &goto_functions) +void list_eloc(const goto_modelt &goto_model) { working_dirst eloc_map; - collect_eloc(goto_functions, eloc_map); + collect_eloc(goto_model, eloc_map); for(const std::pair &files : eloc_map) for(const std::pair &lines : files.second) @@ -74,13 +74,13 @@ void list_eloc(const goto_functionst &goto_functions) } } -void print_path_lengths(const goto_functionst &goto_functions) +void print_path_lengths(const goto_modelt &goto_model) { - const irep_idt &entry_point=goto_functions.entry_point(); + const irep_idt &entry_point=goto_model.goto_functions.entry_point(); goto_functionst::function_mapt::const_iterator start= - goto_functions.function_map.find(entry_point); + goto_model.goto_functions.function_map.find(entry_point); - if(start==goto_functions.function_map.end() || + if(start==goto_model.goto_functions.function_map.end() || !start->second.body_available()) { std::cout << "No entry point found, path length undefined\n"; @@ -98,7 +98,7 @@ void print_path_lengths(const goto_functionst &goto_functions) typedef cfg_baset cfgt; cfgt cfg; - cfg(goto_functions); + cfg(goto_model.goto_functions); const goto_programt &start_program=start->second.body; @@ -113,7 +113,7 @@ void print_path_lengths(const goto_functionst &goto_functions) << " instructions\n"; std::size_t n_loops=0, loop_ins=0; - forall_goto_functions(gf_it, goto_functions) + forall_goto_functions(gf_it, goto_model.goto_functions) forall_goto_program_instructions(i_it, gf_it->second.body) // loops or recursion if(i_it->is_backwards_goto() || diff --git a/src/goto-instrument/count_eloc.h b/src/goto-instrument/count_eloc.h index 38760038836..9a140eec52b 100644 --- a/src/goto-instrument/count_eloc.h +++ b/src/goto-instrument/count_eloc.h @@ -14,12 +14,10 @@ Date: December 2012 #ifndef CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H #define CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H -#include +#include -void count_eloc(const goto_functionst &goto_functions); - -void list_eloc(const goto_functionst &goto_functions); - -void print_path_lengths(const goto_functionst &goto_functions); +void count_eloc(const goto_modelt &); +void list_eloc(const goto_modelt &); +void print_path_lengths(const goto_modelt &); #endif // CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H diff --git a/src/goto-instrument/document_properties.cpp b/src/goto-instrument/document_properties.cpp index 0a7e656bff0..5140459c025 100644 --- a/src/goto-instrument/document_properties.cpp +++ b/src/goto-instrument/document_properties.cpp @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #define MAXWIDTH 62 class document_propertiest @@ -361,15 +363,15 @@ void document_propertiest::doit() } void document_properties_html( - const goto_functionst &goto_functions, + const goto_modelt &goto_model, std::ostream &out) { - document_propertiest(goto_functions, out).html(); + document_propertiest(goto_model.goto_functions, out).html(); } void document_properties_latex( - const goto_functionst &goto_functions, + const goto_modelt &goto_model, std::ostream &out) { - document_propertiest(goto_functions, out).latex(); + document_propertiest(goto_model.goto_functions, out).latex(); } diff --git a/src/goto-instrument/document_properties.h b/src/goto-instrument/document_properties.h index 35406ae2f30..45f1b147ca7 100644 --- a/src/goto-instrument/document_properties.h +++ b/src/goto-instrument/document_properties.h @@ -14,14 +14,14 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +class goto_modelt; void document_properties_latex( - const goto_functionst &goto_functions, + const goto_modelt &, std::ostream &out); void document_properties_html( - const goto_functionst &goto_functions, + const goto_modelt &, std::ostream &out); #endif // CPROVER_GOTO_INSTRUMENT_DOCUMENT_PROPERTIES_H diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp index bf58fe12cd3..d011c10914a 100644 --- a/src/goto-instrument/dot.cpp +++ b/src/goto-instrument/dot.cpp @@ -25,11 +25,9 @@ Author: Daniel Kroening, kroening@kroening.com class dott { public: - dott( - const goto_functionst &_goto_functions, - const namespacet &_ns): - ns(_ns), - goto_functions(_goto_functions), + explicit dott( + const goto_modelt &_goto_model): + goto_model(_goto_model), subgraphscount(0) { } @@ -37,8 +35,7 @@ class dott void output(std::ostream &out); protected: - const namespacet &ns; - const goto_functionst &goto_functions; + const goto_modelt &goto_model; unsigned subgraphscount; @@ -91,6 +88,8 @@ void dott::write_dot_subgraph( } else { + const namespacet ns(goto_model.symbol_table); + std::set seen; goto_programt::const_targetst worklist; worklist.push_back(instructions.begin()); @@ -265,7 +264,7 @@ void dott::output(std::ostream &out) std::list clusters; - forall_goto_functions(it, goto_functions) + forall_goto_functions(it, goto_model.goto_functions) if(it->second.body_available()) write_dot_subgraph(out, id2string(it->first), it->second.body); @@ -350,11 +349,8 @@ void dott::write_edge( out << ";\n"; } -void dot( - const goto_functionst &src, - const namespacet &ns, - std::ostream &out) +void dot(const goto_modelt &src, std::ostream &out) { - dott dot(src, ns); + dott dot(src); dot.output(out); } diff --git a/src/goto-instrument/dot.h b/src/goto-instrument/dot.h index 1a5f84e319b..12d5f0edfbb 100644 --- a/src/goto-instrument/dot.h +++ b/src/goto-instrument/dot.h @@ -12,11 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_DOT_H #define CPROVER_GOTO_INSTRUMENT_DOT_H -#include +#include + +#include void dot( - const goto_functionst &src, - const namespacet &ns, + const goto_modelt &, std::ostream &out); #endif // CPROVER_GOTO_INSTRUMENT_DOT_H diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp index 6c62a07f4f7..5cf1883fb8f 100644 --- a/src/goto-instrument/function.cpp +++ b/src/goto-instrument/function.cpp @@ -79,11 +79,10 @@ code_function_callt function_to_call( } void function_enter( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &goto_model, const irep_idt &id) { - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) { // don't instrument our internal functions if(has_prefix(id2string(f_it->first), CPROVER_PREFIX)) @@ -100,17 +99,16 @@ void function_enter( goto_programt::targett t= body.insert_before(body.instructions.begin()); t->make_function_call( - function_to_call(symbol_table, id, f_it->first)); + function_to_call(goto_model.symbol_table, id, f_it->first)); t->function=f_it->first; } } void function_exit( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &goto_model, const irep_idt &id) { - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) { // don't instrument our internal functions if(has_prefix(id2string(f_it->first), CPROVER_PREFIX)) @@ -136,7 +134,7 @@ void function_exit( goto_programt::instructiont call; call.function=f_it->first; call.make_function_call( - function_to_call(symbol_table, id, f_it->first)); + function_to_call(goto_model.symbol_table, id, f_it->first)); body.insert_before_swap(i_it, call); // move on @@ -164,7 +162,7 @@ void function_exit( { goto_programt::instructiont call; call.make_function_call( - function_to_call(symbol_table, id, f_it->first)); + function_to_call(goto_model.symbol_table, id, f_it->first)); call.function=f_it->first; body.insert_before_swap(last, call); } diff --git a/src/goto-instrument/function.h b/src/goto-instrument/function.h index 88b486df6b0..101a0643e40 100644 --- a/src/goto-instrument/function.h +++ b/src/goto-instrument/function.h @@ -12,21 +12,19 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_FUNCTION_H #define CPROVER_GOTO_INSTRUMENT_FUNCTION_H -#include +#include class code_function_callt function_to_call( - symbol_tablet &symbol_table, + symbol_tablet &, const irep_idt &id, const irep_idt &argument); void function_enter( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &, const irep_idt &id); void function_exit( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &, const irep_idt &id); #endif // CPROVER_GOTO_INSTRUMENT_FUNCTION_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index be77888ad47..dacfa6c8077 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -199,10 +199,10 @@ int goto_instrument_parse_optionst::doit() } goto_unwindt goto_unwind; - goto_unwind(goto_functions, unwind_set, k, unwind_strategy); + goto_unwind(goto_model, unwind_set, k, unwind_strategy); - goto_functions.update(); - goto_functions.compute_loop_numbers(); + goto_model.goto_functions.update(); + goto_model.goto_functions.compute_loop_numbers(); if(cmdline.isset("log")) { @@ -234,11 +234,11 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-threaded")) { - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); - is_threadedt is_threaded(goto_functions); + is_threadedt is_threaded(goto_model); - forall_goto_functions(f_it, goto_functions) + forall_goto_functions(f_it, goto_model.goto_functions) { std::cout << "////\n"; std::cout << "//// Function: " << f_it->first << '\n'; @@ -261,14 +261,13 @@ int goto_instrument_parse_optionst::doit() do_partial_inlining(); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); status() << "Pointer Analysis" << eom; - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); value_set_analysist value_set_analysis(ns); - value_set_analysis(goto_functions); - - show_value_sets(get_ui(), goto_functions, value_set_analysis); + value_set_analysis(goto_model.goto_functions); + show_value_sets(get_ui(), goto_model, value_set_analysis); return 0; } @@ -277,15 +276,14 @@ int goto_instrument_parse_optionst::doit() do_indirect_call_and_rtti_removal(); do_partial_inlining(); do_remove_returns(); - parameter_assignments(symbol_table, goto_functions); + parameter_assignments(goto_model); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); - namespacet ns(symbol_table); global_may_alias_analysist global_may_alias_analysis; - global_may_alias_analysis(goto_functions, ns); - global_may_alias_analysis.output(ns, goto_functions, std::cout); + global_may_alias_analysis(goto_model); + global_may_alias_analysis.output(goto_model, std::cout); return 0; } @@ -294,14 +292,14 @@ int goto_instrument_parse_optionst::doit() { do_indirect_call_and_rtti_removal(); do_partial_inlining(); - parameter_assignments(symbol_table, goto_functions); + parameter_assignments(goto_model); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); - forall_goto_functions(it, goto_functions) + forall_goto_functions(it, goto_model.goto_functions) { local_bitvector_analysist local_bitvector_analysis(it->second); std::cout << ">>>>\n"; @@ -319,23 +317,22 @@ int goto_instrument_parse_optionst::doit() do_indirect_call_and_rtti_removal(); do_partial_inlining(); do_remove_returns(); - parameter_assignments(symbol_table, goto_functions); + parameter_assignments(goto_model); - remove_unused_functions(goto_functions, get_message_handler()); + remove_unused_functions(goto_model, get_message_handler()); if(!cmdline.isset("inline")) { - thread_exit_instrumentation(goto_functions); - mutex_init_instrumentation(symbol_table, goto_functions); + thread_exit_instrumentation(goto_model); + mutex_init_instrumentation(goto_model); } // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); - namespacet ns(symbol_table); custom_bitvector_analysist custom_bitvector_analysis; - custom_bitvector_analysis(goto_functions, ns); - custom_bitvector_analysis.output(ns, goto_functions, std::cout); + custom_bitvector_analysis(goto_model); + custom_bitvector_analysis.output(goto_model, std::cout); return 0; } @@ -345,17 +342,14 @@ int goto_instrument_parse_optionst::doit() do_indirect_call_and_rtti_removal(); do_partial_inlining(); do_remove_returns(); - parameter_assignments(symbol_table, goto_functions); + parameter_assignments(goto_model); // recalculate numbers, etc. - goto_functions.update(); - - namespacet ns(symbol_table); + goto_model.goto_functions.update(); escape_analysist escape_analysis; - escape_analysis(goto_functions, ns); - - escape_analysis.output(ns, goto_functions, std::cout); + escape_analysis(goto_model); + escape_analysis.output(goto_model, std::cout); return 0; } @@ -365,26 +359,25 @@ int goto_instrument_parse_optionst::doit() do_indirect_call_and_rtti_removal(); do_partial_inlining(); do_remove_returns(); - parameter_assignments(symbol_table, goto_functions); + parameter_assignments(goto_model); - remove_unused_functions(goto_functions, get_message_handler()); + remove_unused_functions(goto_model, get_message_handler()); if(!cmdline.isset("inline")) { - thread_exit_instrumentation(goto_functions); - mutex_init_instrumentation(symbol_table, goto_functions); + thread_exit_instrumentation(goto_model); + mutex_init_instrumentation(goto_model); } // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); custom_bitvector_analysist custom_bitvector_analysis; - custom_bitvector_analysis(goto_functions, ns); + custom_bitvector_analysis(goto_model); custom_bitvector_analysis.check( - ns, - goto_functions, + goto_model, cmdline.isset("xml-ui"), std::cout); @@ -397,13 +390,13 @@ int goto_instrument_parse_optionst::doit() do_partial_inlining(); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); status() << "Pointer Analysis" << eom; points_tot points_to; - points_to(goto_functions); + points_to(goto_model); points_to.output(std::cout); return 0; } @@ -414,27 +407,26 @@ int goto_instrument_parse_optionst::doit() do_partial_inlining(); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); status() << "Interval Analysis" << eom; - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); ait interval_analysis; - interval_analysis(goto_functions, ns); - - interval_analysis.output(ns, goto_functions, std::cout); + interval_analysis(goto_model); + interval_analysis.output(goto_model, std::cout); return 0; } if(cmdline.isset("show-call-sequences")) { - show_call_sequences(goto_functions); + show_call_sequences(goto_model); return 0; } if(cmdline.isset("check-call-sequence")) { do_remove_returns(); - check_call_sequence(goto_functions); + check_call_sequence(goto_model); return 0; } @@ -443,15 +435,14 @@ int goto_instrument_parse_optionst::doit() do_indirect_call_and_rtti_removal(); do_partial_inlining(); - namespacet ns(symbol_table); - list_calls_and_arguments(ns, goto_functions); + list_calls_and_arguments(goto_model); return 0; } if(cmdline.isset("show-rw-set")) { - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); if(!cmdline.isset("inline")) { @@ -459,24 +450,24 @@ int goto_instrument_parse_optionst::doit() do_partial_inlining(); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); } status() << "Pointer Analysis" << eom; value_set_analysist value_set_analysis(ns); - value_set_analysis(goto_functions); + value_set_analysis(goto_model.goto_functions); const symbolt &symbol=ns.lookup(ID_main); symbol_exprt main(symbol.name, symbol.type); std::cout << - rw_set_functiont(value_set_analysis, ns, goto_functions, main); + rw_set_functiont(value_set_analysis, goto_model, main); return 0; } if(cmdline.isset("show-symbol-table")) { - show_symbol_table(); + show_symbol_table(goto_model, get_ui()); return 0; } @@ -484,11 +475,10 @@ int goto_instrument_parse_optionst::doit() { do_indirect_call_and_rtti_removal(); - const namespacet ns(symbol_table); + const namespacet ns(goto_model.symbol_table); reaching_definitions_analysist rd_analysis(ns); - rd_analysis(goto_functions, ns); - - rd_analysis.output(ns, goto_functions, std::cout); + rd_analysis(goto_model); + rd_analysis.output(goto_model, std::cout); return 0; } @@ -497,11 +487,10 @@ int goto_instrument_parse_optionst::doit() { do_indirect_call_and_rtti_removal(); - const namespacet ns(symbol_table); + const namespacet ns(goto_model.symbol_table); dependence_grapht dependence_graph(ns); - dependence_graph(goto_functions, ns); - - dependence_graph.output(ns, goto_functions, std::cout); + dependence_graph(goto_model); + dependence_graph.output(goto_model, std::cout); dependence_graph.output_dot(std::cout); return 0; @@ -509,79 +498,78 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("count-eloc")) { - count_eloc(goto_functions); + count_eloc(goto_model); return 0; } if(cmdline.isset("list-eloc")) { - list_eloc(goto_functions); + list_eloc(goto_model); return 0; } if(cmdline.isset("print-path-lengths")) { - print_path_lengths(goto_functions); + print_path_lengths(goto_model); return 0; } if(cmdline.isset("list-symbols")) { - show_symbol_table(true); + show_symbol_table_brief(goto_model, get_ui()); return 0; } if(cmdline.isset("show-uninitialized")) { - show_uninitialized(symbol_table, goto_functions, std::cout); + show_uninitialized(goto_model, std::cout); return 0; } if(cmdline.isset("interpreter")) { status() << "Starting interpreter" << eom; - interpreter(symbol_table, goto_functions, get_message_handler()); + interpreter(goto_model, get_message_handler()); return 0; } if(cmdline.isset("show-claims") || cmdline.isset("show-properties")) { - const namespacet ns(symbol_table); - show_properties(ns, get_ui(), goto_functions); + const namespacet ns(goto_model.symbol_table); + show_properties(goto_model, get_ui()); return 0; } if(cmdline.isset("document-claims-html") || cmdline.isset("document-properties-html")) { - document_properties_html(goto_functions, std::cout); + document_properties_html(goto_model, std::cout); return 0; } if(cmdline.isset("document-claims-latex") || cmdline.isset("document-properties-latex")) { - document_properties_latex(goto_functions, std::cout); + document_properties_latex(goto_model, std::cout); return 0; } if(cmdline.isset("show-loops")) { - show_loop_ids(get_ui(), goto_functions); + show_loop_ids(get_ui(), goto_model); return 0; } if(cmdline.isset("show-natural-loops")) { - const namespacet ns(symbol_table); - show_natural_loops(goto_functions); + show_natural_loops(goto_model); return 0; } if(cmdline.isset("print-internal-representation")) { - for(auto const &pair : goto_functions.function_map) + for(auto const &pair : goto_model.goto_functions.function_map) for(auto const &ins : pair.second.body.instructions) { if(ins.code.is_not_nil()) @@ -594,28 +582,27 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-goto-functions")) { - namespacet ns(symbol_table); - show_goto_functions(ns, get_ui(), goto_functions); + namespacet ns(goto_model.symbol_table); + show_goto_functions(goto_model, get_ui()); return 0; } if(cmdline.isset("list-undefined-functions")) { - const namespacet ns(symbol_table); - list_undefined_functions(goto_functions, ns, std::cout); + list_undefined_functions(goto_model, std::cout); return 0; } // experimental: print structs if(cmdline.isset("show-struct-alignment")) { - print_struct_alignment_problems(symbol_table, std::cout); + print_struct_alignment_problems(goto_model.symbol_table, std::cout); return 0; } if(cmdline.isset("show-locations")) { - show_locations(get_ui(), goto_functions); + show_locations(get_ui(), goto_model); return 0; } @@ -625,11 +612,11 @@ int goto_instrument_parse_optionst::doit() const bool h_libc=!cmdline.isset("no-system-headers"); const bool h_all=cmdline.isset("use-all-headers"); const bool harness=cmdline.isset("harness"); - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); // restore RETURN instructions in case remove_returns had been // applied - restore_returns(symbol_table, goto_functions); + restore_returns(goto_model); if(cmdline.args.size()==2) { @@ -644,7 +631,7 @@ int goto_instrument_parse_optionst::doit() return 10; } (is_cpp ? dump_cpp : dump_c)( - goto_functions, + goto_model.goto_functions, h_libc, h_all, harness, @@ -653,7 +640,7 @@ int goto_instrument_parse_optionst::doit() } else (is_cpp ? dump_cpp : dump_c)( - goto_functions, + goto_model.goto_functions, h_libc, h_all, harness, @@ -665,7 +652,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("call-graph")) { - call_grapht call_graph(goto_functions); + call_grapht call_graph(goto_model); if(cmdline.isset("xml")) call_graph.output_xml(std::cout); @@ -679,7 +666,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("dot")) { - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); if(cmdline.args.size()==2) { @@ -694,10 +681,10 @@ int goto_instrument_parse_optionst::doit() return 10; } - dot(goto_functions, ns, out); + dot(goto_model, out); } else - dot(goto_functions, ns, std::cout); + dot(goto_model, std::cout); return 0; } @@ -706,21 +693,21 @@ int goto_instrument_parse_optionst::doit() { do_indirect_call_and_rtti_removal(); - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); status() << "Performing full inlining" << eom; - goto_inline(goto_functions, ns, ui_message_handler); + goto_inline(goto_model, get_message_handler()); status() << "Accelerating" << eom; - accelerate_functions(goto_functions, symbol_table, cmdline.isset("z3")); - remove_skip(goto_functions); - goto_functions.update(); + accelerate_functions(goto_model, cmdline.isset("z3")); + remove_skip(goto_model); + goto_model.goto_functions.update(); } if(cmdline.isset("horn-encoding")) { status() << "Horn-clause encoding" << eom; - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); if(cmdline.args.size()==2) { @@ -737,10 +724,10 @@ int goto_instrument_parse_optionst::doit() return 1; } - horn_encoding(goto_functions, ns, out); + horn_encoding(goto_model, out); } else - horn_encoding(goto_functions, ns, std::cout); + horn_encoding(goto_model, std::cout); return 0; } @@ -750,14 +737,13 @@ int goto_instrument_parse_optionst::doit() do_indirect_call_and_rtti_removal(); status() << "Removing unused functions" << eom; - remove_unused_functions(goto_functions, get_message_handler()); + remove_unused_functions(goto_model.goto_functions, get_message_handler()); } if(cmdline.isset("undefined-function-is-assume-false")) { do_indirect_call_and_rtti_removal(); - - undefined_function_abort_path(goto_functions); + undefined_function_abort_path(goto_model); } // write new binary? @@ -766,7 +752,7 @@ int goto_instrument_parse_optionst::doit() status() << "Writing GOTO program to `" << cmdline.args[1] << "'" << eom; if(write_goto_binary( - cmdline.args[1], symbol_table, goto_functions, get_message_handler())) + cmdline.args[1], goto_model, get_message_handler())) return 1; else return 0; @@ -812,16 +798,15 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal( status() << "Function Pointer Removal" << eom; remove_function_pointers( get_message_handler(), - symbol_table, - goto_functions, + goto_model, cmdline.isset("pointer-check")); status() << "Virtual function removal" << eom; - remove_virtual_functions(symbol_table, goto_functions); + remove_virtual_functions(goto_model); status() << "Catch and throw removal" << eom; // This introduces instanceof, so order is important: - remove_exceptions(symbol_table, goto_functions); + remove_exceptions(goto_model); status() << "Java instanceof removal" << eom; - remove_instanceof(symbol_table, goto_functions); + remove_instanceof(goto_model); } /// Remove function pointers that can be resolved by analysing const variables @@ -839,8 +824,7 @@ void goto_instrument_parse_optionst::do_remove_const_function_pointers_only() status() << "Removing const function pointers only" << eom; remove_function_pointers( get_message_handler(), - symbol_table, - goto_functions, + goto_model, cmdline.isset("pointer-check"), true); // abort if we can't resolve via const pointers } @@ -855,8 +839,7 @@ void goto_instrument_parse_optionst::do_partial_inlining() if(!cmdline.isset("inline")) { status() << "Partial Inlining" << eom; - const namespacet ns(symbol_table); - goto_partial_inline(goto_functions, ns, ui_message_handler); + goto_partial_inline(goto_model, ui_message_handler); } } @@ -868,7 +851,7 @@ void goto_instrument_parse_optionst::do_remove_returns() remove_returns_done=true; status() << "Removing returns" << eom; - remove_returns(symbol_table, goto_functions); + remove_returns(goto_model); } void goto_instrument_parse_optionst::get_goto_program() @@ -876,7 +859,7 @@ void goto_instrument_parse_optionst::get_goto_program() status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom; if(read_goto_binary(cmdline.args[0], - symbol_table, goto_functions, get_message_handler())) + goto_model, get_message_handler())) throw 0; config.set(cmdline); @@ -929,13 +912,13 @@ void goto_instrument_parse_optionst::instrument_goto_program() { status() << "Adding gotos to skip loops" << eom; if(skip_loops( - goto_functions, + goto_model, cmdline.get_value("skip-loops"), get_message_handler())) throw 0; } - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); // initialize argv with valid pointers if(cmdline.isset("model-argc-argv")) @@ -946,8 +929,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() status() << "Adding up to " << max_argc << " command line arguments" << eom; if(model_argc_argv( - symbol_table, - goto_functions, + goto_model, max_argc, get_message_handler())) throw 0; @@ -956,8 +938,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("remove-function-body")) { remove_functions( - symbol_table, - goto_functions, + goto_model, cmdline.get_values("remove-function-body"), get_message_handler()); } @@ -972,7 +953,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() config.ansi_c.defines.push_back("__CPROVER_CUSTOM_BITVECTOR_ANALYSIS"); // add the library - link_to_library(symbol_table, goto_functions, ui_message_handler); + link_to_library(goto_model, get_message_handler()); } // now do full inlining, if requested @@ -984,12 +965,12 @@ void goto_instrument_parse_optionst::instrument_goto_program() cmdline.isset("custom-bitvector-analysis")) { do_remove_returns(); - thread_exit_instrumentation(goto_functions); - mutex_init_instrumentation(symbol_table, goto_functions); + thread_exit_instrumentation(goto_model); + mutex_init_instrumentation(goto_model); } status() << "Performing full inlining" << eom; - goto_inline(goto_functions, ns, ui_message_handler); + goto_inline(goto_model, get_message_handler()); } if(cmdline.isset("show-custom-bitvector-analysis") || @@ -998,8 +979,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_partial_inlining(); status() << "Propagating Constants" << eom; - constant_propagator_ait constant_propagator_ai(goto_functions, ns); - remove_skip(goto_functions); + constant_propagator_ait constant_propagator_ai(goto_model); + remove_skip(goto_model); } if(cmdline.isset("escape-analysis")) @@ -1007,28 +988,28 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_indirect_call_and_rtti_removal(); do_partial_inlining(); do_remove_returns(); - parameter_assignments(symbol_table, goto_functions); + parameter_assignments(goto_model); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); status() << "Escape Analysis" << eom; escape_analysist escape_analysis; - escape_analysis(goto_functions, ns); - escape_analysis.instrument(goto_functions, ns); + escape_analysis(goto_model); + escape_analysis.instrument(goto_model); // inline added functions, they are often small - goto_partial_inline(goto_functions, ns, ui_message_handler); + goto_partial_inline(goto_model, get_message_handler()); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); } // verify and set invariants and pre/post-condition pairs if(cmdline.isset("apply-code-contracts")) { status() << "Applying Code Contracts" << eom; - code_contracts(symbol_table, goto_functions); + code_contracts(goto_model); } // replace function pointers, if explicitly requested @@ -1055,9 +1036,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(!cmdline.isset("log")) { goto_function_inline( - goto_functions, + goto_model, function, - ns, ui_message_handler, true, caching); @@ -1069,9 +1049,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() jsont result= goto_function_inline_and_log( - goto_functions, + goto_model, function, - ns, ui_message_handler, true, caching); @@ -1095,8 +1074,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() } } - goto_functions.update(); - goto_functions.compute_loop_numbers(); + goto_model.goto_functions.update(); + goto_model.goto_functions.compute_loop_numbers(); } if(cmdline.isset("partial-inline")) @@ -1104,10 +1083,10 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_indirect_call_and_rtti_removal(); status() << "Partial inlining" << eom; - goto_partial_inline(goto_functions, ns, ui_message_handler, true); + goto_partial_inline(goto_model, get_message_handler(), true); - goto_functions.update(); - goto_functions.compute_loop_numbers(); + goto_model.goto_functions.update(); + goto_model.goto_functions.compute_loop_numbers(); } // now do full inlining, if requested @@ -1119,12 +1098,12 @@ void goto_instrument_parse_optionst::instrument_goto_program() cmdline.isset("custom-bitvector-analysis")) { do_remove_returns(); - thread_exit_instrumentation(goto_functions); - mutex_init_instrumentation(symbol_table, goto_functions); + thread_exit_instrumentation(goto_model); + mutex_init_instrumentation(goto_model); } status() << "Performing full inlining" << eom; - goto_inline(goto_functions, ns, ui_message_handler, true); + goto_inline(goto_model, get_message_handler(), true); } if(cmdline.isset("constant-propagator")) @@ -1133,19 +1112,18 @@ void goto_instrument_parse_optionst::instrument_goto_program() status() << "Propagating Constants" << eom; - constant_propagator_ait constant_propagator_ai(goto_functions, ns); - - remove_skip(goto_functions); + constant_propagator_ait constant_propagator_ai(goto_model); + remove_skip(goto_model); } // add generic checks, if needed - goto_check(ns, options, goto_functions); + goto_check(options, goto_model); // check for uninitalized local variables if(cmdline.isset("uninitialized-check")) { status() << "Adding checks for uninitialized local variables" << eom; - add_uninitialized_locals_assertions(symbol_table, goto_functions); + add_uninitialized_locals_assertions(goto_model); } // check for maximum call stack size @@ -1153,8 +1131,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() { status() << "Adding check for maximum call stack size" << eom; stack_depth( - symbol_table, - goto_functions, + goto_model, unsafe_string2unsigned(cmdline.get_value("stack-depth"))); } @@ -1164,14 +1141,14 @@ void goto_instrument_parse_optionst::instrument_goto_program() { status() << "Adding nondeterministic initialization of static/global " "variables" << eom; - nondet_static(ns, goto_functions); + nondet_static(goto_model); } if(cmdline.isset("slice-global-inits")) { status() << "Slicing away initializations of unused global variables" << eom; - slice_global_inits(ns, goto_functions); + slice_global_inits(goto_model); } if(cmdline.isset("string-abstraction")) @@ -1181,9 +1158,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() status() << "String Abstraction" << eom; string_abstraction( - symbol_table, - get_message_handler(), - goto_functions); + goto_model, + get_message_handler()); } // some analyses require function pointer removal and partial inlining @@ -1199,25 +1175,19 @@ void goto_instrument_parse_optionst::instrument_goto_program() status() << "Pointer Analysis" << eom; value_set_analysist value_set_analysis(ns); - value_set_analysis(goto_functions); + value_set_analysis(goto_model.goto_functions); if(cmdline.isset("remove-pointers")) { // removing pointers status() << "Removing Pointers" << eom; - remove_pointers( - goto_functions, - symbol_table, - value_set_analysis); + remove_pointers(goto_model, value_set_analysis); } if(cmdline.isset("race-check")) { status() << "Adding Race Checks" << eom; - race_check( - value_set_analysis, - symbol_table, - goto_functions); + race_check(value_set_analysis, goto_model); } if(cmdline.isset("mm")) @@ -1225,8 +1195,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() // TODO: move to wmm/weak_mem, and copy goto_functions AFTER some of the // modifications. Do the analysis on the copy, after remove_asm, and // instrument the original (without remove_asm) - remove_asm(symbol_table, goto_functions); - goto_functions.update(); + remove_asm(goto_model); + goto_model.goto_functions.update(); std::string mm=cmdline.get_value("mm"); memory_modelt model; @@ -1294,8 +1264,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() weak_memory( model, value_set_analysis, - symbol_table, - goto_functions, + goto_model, cmdline.isset("scc"), inst_strategy, unwind_loops, @@ -1319,8 +1288,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() status() << "Instrumenting interrupt handler" << eom; interrupt( value_set_analysis, - symbol_table, - goto_functions, + goto_model, cmdline.get_value("isr")); } @@ -1328,32 +1296,26 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("mmio")) { status() << "Instrumenting memory-mapped I/O" << eom; - mmio( - value_set_analysis, - symbol_table, - goto_functions); + mmio(value_set_analysis, goto_model); } if(cmdline.isset("concurrency")) { status() << "Sequentializing concurrency" << eom; - concurrency( - value_set_analysis, - symbol_table, - goto_functions); + concurrency(value_set_analysis, goto_model); } } if(cmdline.isset("interval-analysis")) { status() << "Interval analysis" << eom; - interval_analysis(ns, goto_functions); + interval_analysis(goto_model); } if(cmdline.isset("havoc-loops")) { status() << "Havocking loops" << eom; - havoc_loops(goto_functions); + havoc_loops(goto_model); } if(cmdline.isset("k-induction")) @@ -1374,15 +1336,14 @@ void goto_instrument_parse_optionst::instrument_goto_program() status() << "Instrumenting k-induction for k=" << k << ", " << (base_case?"base case":"step case") << eom; - k_induction(goto_functions, base_case, step_case, k); + k_induction(goto_model, base_case, step_case, k); } if(cmdline.isset("function-enter")) { status() << "Function enter instrumentation" << eom; function_enter( - symbol_table, - goto_functions, + goto_model, cmdline.get_value("function-enter")); } @@ -1390,8 +1351,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() { status() << "Function exit instrumentation" << eom; function_exit( - symbol_table, - goto_functions, + goto_model, cmdline.get_value("function-exit")); } @@ -1399,28 +1359,27 @@ void goto_instrument_parse_optionst::instrument_goto_program() { status() << "Branch instrumentation" << eom; branch( - symbol_table, - goto_functions, + goto_model, cmdline.get_value("branch")); } // add failed symbols - add_failed_symbols(symbol_table); + add_failed_symbols(goto_model.symbol_table); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); // add loop ids - goto_functions.compute_loop_numbers(); + goto_model.goto_functions.compute_loop_numbers(); // label the assertions - label_properties(goto_functions); + label_properties(goto_model); // nondet volatile? if(cmdline.isset("nondet-volatile")) { status() << "Making volatile variables non-deterministic" << eom; - nondet_volatile(symbol_table, goto_functions); + nondet_volatile(goto_model); } // reachability slice? @@ -1430,9 +1389,9 @@ void goto_instrument_parse_optionst::instrument_goto_program() status() << "Performing a reachability slice" << eom; if(cmdline.isset("property")) - reachability_slicer(goto_functions, cmdline.get_values("property")); + reachability_slicer(goto_model, cmdline.get_values("property")); else - reachability_slicer(goto_functions); + reachability_slicer(goto_model); } // full slice? @@ -1443,13 +1402,13 @@ void goto_instrument_parse_optionst::instrument_goto_program() status() << "Performing a full slice" << eom; if(cmdline.isset("property")) - property_slicer(goto_functions, ns, cmdline.get_values("property")); + property_slicer(goto_model, cmdline.get_values("property")); else - full_slicer(goto_functions, ns); + full_slicer(goto_model); } // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); } /// display command line help diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 25ed2ce4cee..5dc2c017d41 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -116,7 +116,12 @@ class goto_instrument_parse_optionst: bool partial_inlining_done; bool remove_returns_done; - goto_functionst goto_functions; + goto_modelt goto_model; + + ui_message_handlert::uit get_ui() + { + return ui_message_handler.get_ui(); + } }; #endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H diff --git a/src/goto-instrument/havoc_loops.cpp b/src/goto-instrument/havoc_loops.cpp index d612a31fc03..01bc2701dd8 100644 --- a/src/goto-instrument/havoc_loops.cpp +++ b/src/goto-instrument/havoc_loops.cpp @@ -184,10 +184,10 @@ void havoc_loopst::havoc_loops() havoc_loop(loop.first, loop.second); } -void havoc_loops(goto_functionst &goto_functions) +void havoc_loops(goto_modelt &goto_model) { - function_modifiest function_modifies(goto_functions); + function_modifiest function_modifies(goto_model.goto_functions); - Forall_goto_functions(it, goto_functions) + Forall_goto_functions(it, goto_model.goto_functions) havoc_loopst(function_modifies, it->second); } diff --git a/src/goto-instrument/havoc_loops.h b/src/goto-instrument/havoc_loops.h index dc3245a1162..42edd24d4b9 100644 --- a/src/goto-instrument/havoc_loops.h +++ b/src/goto-instrument/havoc_loops.h @@ -12,8 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_HAVOC_LOOPS_H #define CPROVER_GOTO_INSTRUMENT_HAVOC_LOOPS_H -#include +class goto_modelt; -void havoc_loops(goto_functionst &goto_functions); +void havoc_loops(goto_modelt &); #endif // CPROVER_GOTO_INSTRUMENT_HAVOC_LOOPS_H diff --git a/src/goto-instrument/horn_encoding.cpp b/src/goto-instrument/horn_encoding.cpp index 31fcb187848..bccce9a0580 100644 --- a/src/goto-instrument/horn_encoding.cpp +++ b/src/goto-instrument/horn_encoding.cpp @@ -16,8 +16,7 @@ Date: June 2015 #include void horn_encoding( - const goto_functionst &, - const namespacet &, + const goto_modelt &, std::ostream &out) { } diff --git a/src/goto-instrument/horn_encoding.h b/src/goto-instrument/horn_encoding.h index 44160c35ceb..c1f8fb5fc60 100644 --- a/src/goto-instrument/horn_encoding.h +++ b/src/goto-instrument/horn_encoding.h @@ -14,11 +14,10 @@ Module: Horn-clause Encoding #include -#include +#include void horn_encoding( - const goto_functionst &, - const namespacet &, + const goto_modelt &, std::ostream &out); #endif // CPROVER_GOTO_INSTRUMENT_HORN_ENCODING_H diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-instrument/interrupt.cpp index 38a5a258ff6..23bf63eb1a4 100644 --- a/src/goto-instrument/interrupt.cpp +++ b/src/goto-instrument/interrupt.cpp @@ -189,30 +189,29 @@ symbol_exprt get_isr( void interrupt( value_setst &value_sets, - const symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &goto_model, const irep_idt &interrupt_handler) { // look up the ISR - symbol_exprt isr=get_isr(symbol_table, interrupt_handler); + symbol_exprt isr= + get_isr(goto_model.symbol_table, interrupt_handler); // we first figure out which objects are read/written by the ISR - const namespacet ns(symbol_table); rw_set_functiont isr_rw_set( - value_sets, ns, goto_functions, isr); + value_sets, goto_model, isr); // now instrument - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) if(f_it->first!=CPROVER_PREFIX "initialize" && f_it->first!=goto_functionst::entry_point() && f_it->first!=isr.get_identifier()) interrupt( - value_sets, symbol_table, + value_sets, goto_model.symbol_table, #ifdef LOCAL_MAY f_it->second, #endif f_it->second.body, isr, isr_rw_set); - goto_functions.update(); + goto_model.goto_functions.update(); } diff --git a/src/goto-instrument/interrupt.h b/src/goto-instrument/interrupt.h index 711c4fa32df..775357c2a84 100644 --- a/src/goto-instrument/interrupt.h +++ b/src/goto-instrument/interrupt.h @@ -14,15 +14,13 @@ Date: September 2011 #ifndef CPROVER_GOTO_INSTRUMENT_INTERRUPT_H #define CPROVER_GOTO_INSTRUMENT_INTERRUPT_H -class symbol_tablet; -class goto_functionst; +class goto_modelt; #include "rw_set.h" void interrupt( - value_setst &value_sets, - const class symbol_tablet &symbol_table, - goto_functionst &goto_functions, + value_setst &, + goto_modelt &, const irep_idt &interrupt_handler); #endif // CPROVER_GOTO_INSTRUMENT_INTERRUPT_H diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp index 9a018e1c331..900057f9f8b 100644 --- a/src/goto-instrument/k_induction.cpp +++ b/src/goto-instrument/k_induction.cpp @@ -150,10 +150,10 @@ void k_inductiont::k_induction() } void k_induction( - goto_functionst &goto_functions, + goto_modelt &goto_model, bool base_case, bool step_case, unsigned k) { - Forall_goto_functions(it, goto_functions) + Forall_goto_functions(it, goto_model.goto_functions) k_inductiont(it->second, base_case, step_case, k); } diff --git a/src/goto-instrument/k_induction.h b/src/goto-instrument/k_induction.h index e5af8b0c43f..f8d8ac4d351 100644 --- a/src/goto-instrument/k_induction.h +++ b/src/goto-instrument/k_induction.h @@ -12,10 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_K_INDUCTION_H #define CPROVER_GOTO_INSTRUMENT_K_INDUCTION_H -#include +class goto_modelt; void k_induction( - goto_functionst &goto_functions, + goto_modelt &, bool base_case, bool step_case, unsigned k); diff --git a/src/goto-instrument/mmio.cpp b/src/goto-instrument/mmio.cpp index a7a21a2f1a9..a865077d0f0 100644 --- a/src/goto-instrument/mmio.cpp +++ b/src/goto-instrument/mmio.cpp @@ -164,23 +164,18 @@ void mmio( void mmio( value_setst &value_sets, - class symbol_tablet &symbol_table, - goto_functionst &goto_functions) + goto_modelt &goto_model) { - // we first figure out which objects are read/written by the ISR - - - // now instrument - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) if(f_it->first!=CPROVER_PREFIX "initialize" && f_it->first!=goto_functionst::entry_point()) - mmio(value_sets, symbol_table, + mmio(value_sets, goto_model.symbol_table, #ifdef LOCAL_MAY f_it->second, #endif f_it->second.body); - goto_functions.update(); + goto_model.goto_functions.update(); } diff --git a/src/goto-instrument/mmio.h b/src/goto-instrument/mmio.h index eab567f9873..f2fbec84fa1 100644 --- a/src/goto-instrument/mmio.h +++ b/src/goto-instrument/mmio.h @@ -15,12 +15,10 @@ Date: September 2011 #define CPROVER_GOTO_INSTRUMENT_MMIO_H class value_setst; -class symbol_tablet; -class goto_functionst; +class goto_modelt; void mmio( - value_setst &value_sets, - class symbol_tablet &symbol_table, - goto_functionst &goto_functions); + value_setst &, + goto_modelt &); #endif // CPROVER_GOTO_INSTRUMENT_MMIO_H diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp index 13d8de6c0b3..779bf1bfcc1 100644 --- a/src/goto-instrument/model_argc_argv.cpp +++ b/src/goto-instrument/model_argc_argv.cpp @@ -27,7 +27,7 @@ Date: April 2016 #include #include -#include +#include #include /// Set up argv with up to max_argc pointers into an array of 4096 bytes. @@ -37,18 +37,19 @@ Date: April 2016 /// \param message_handler: message logging /// \return True, if and only if modelling succeeded bool model_argc_argv( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &goto_model, unsigned max_argc, message_handlert &message_handler) { messaget message(message_handler); - const namespacet ns(symbol_table); + const namespacet ns(goto_model.symbol_table); - if(!symbol_table.has_symbol(goto_functions.entry_point())) + if(!goto_model.symbol_table.has_symbol( + goto_model.goto_functions.entry_point())) { message.error() << "Linking not done, missing " - << goto_functions.entry_point() << messaget::eom; + << goto_model.goto_functions.entry_point() + << messaget::eom; return true; } @@ -79,7 +80,7 @@ bool model_argc_argv( std::ostringstream oss; oss << "int ARGC;\n" << "char *ARGV[1];\n" - << "void " << goto_functions.entry_point() << "()\n" + << "void " << goto_model.goto_functions.entry_point() << "()\n" << "{\n" << " unsigned next=0u;\n" << " " CPROVER_PREFIX "assume(ARGC>=1);\n" @@ -118,8 +119,8 @@ bool model_argc_argv( // add __CPROVER_assume if necessary (it might exist already) if(it->first==CPROVER_PREFIX "assume" || it->first==CPROVER_PREFIX "input") - symbol_table.add(it->second); - else if(it->first==goto_functions.entry_point()) + goto_model.symbol_table.add(it->second); + else if(it->first==goto_model.goto_functions.entry_point()) { value=it->second.value; @@ -128,28 +129,32 @@ bool model_argc_argv( replace.insert("ARGV", ns.lookup("argv'").symbol_expr()); replace(value); } - else if(has_prefix(id2string(it->first), - id2string(goto_functions.entry_point())+"::") && - symbol_table.add(it->second)) + else if(has_prefix( + id2string(it->first), + id2string(goto_model.goto_functions.entry_point())+"::") && + goto_model.symbol_table.add(it->second)) UNREACHABLE; } POSTCONDITION(value.is_not_nil()); goto_convert( to_code(value), - symbol_table, + goto_model.symbol_table, init_instructions, message_handler); + Forall_goto_program_instructions(it, init_instructions) { it->source_location.set_file(""); - it->function=goto_functions.entry_point(); + it->function=goto_model.goto_functions.entry_point(); } goto_functionst::function_mapt::iterator start_entry= - goto_functions.function_map.find(goto_functions.entry_point()); + goto_model.goto_functions.function_map.find( + goto_model.goto_functions.entry_point()); + DATA_INVARIANT( - start_entry!=goto_functions.function_map.end() && + start_entry!=goto_model.goto_functions.function_map.end() && start_entry->second.body_available(), "entry point expected to have a body"); @@ -175,7 +180,7 @@ bool model_argc_argv( // update counters etc. remove_skip(start); start.compute_loop_numbers(); - goto_functions.update(); + goto_model.goto_functions.update(); return false; } diff --git a/src/goto-instrument/model_argc_argv.h b/src/goto-instrument/model_argc_argv.h index 08a214f6fd6..9328f22b488 100644 --- a/src/goto-instrument/model_argc_argv.h +++ b/src/goto-instrument/model_argc_argv.h @@ -14,14 +14,12 @@ Date: April 2016 #ifndef CPROVER_GOTO_INSTRUMENT_MODEL_ARGC_ARGV_H #define CPROVER_GOTO_INSTRUMENT_MODEL_ARGC_ARGV_H -class goto_functionst; +class goto_modelt; class message_handlert; -class symbol_tablet; bool model_argc_argv( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &, unsigned max_argc, - message_handlert &message_handler); + message_handlert &); #endif // CPROVER_GOTO_INSTRUMENT_MODEL_ARGC_ARGV_H diff --git a/src/goto-instrument/nondet_static.h b/src/goto-instrument/nondet_static.h index 16114584849..cddbb52c636 100644 --- a/src/goto-instrument/nondet_static.h +++ b/src/goto-instrument/nondet_static.h @@ -15,14 +15,8 @@ Date: November 2011 #ifndef CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H #define CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H -class goto_functionst; -class namespacet; class goto_modelt; -void nondet_static( - const namespacet &, - goto_functionst &); - void nondet_static(goto_modelt &); #endif // CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp index 4da1ebf6731..1e9024e48d0 100644 --- a/src/goto-instrument/nondet_volatile.cpp +++ b/src/goto-instrument/nondet_volatile.cpp @@ -119,12 +119,10 @@ void nondet_volatile( } } -void nondet_volatile( - symbol_tablet &symbol_table, - goto_functionst &goto_functions) +void nondet_volatile(goto_modelt &goto_model) { - Forall_goto_functions(f_it, goto_functions) - nondet_volatile(symbol_table, f_it->second.body); + Forall_goto_functions(f_it, goto_model.goto_functions) + nondet_volatile(goto_model.symbol_table, f_it->second.body); - goto_functions.update(); + goto_model.goto_functions.update(); } diff --git a/src/goto-instrument/nondet_volatile.h b/src/goto-instrument/nondet_volatile.h index 8cb3930fd56..dd92f3b1833 100644 --- a/src/goto-instrument/nondet_volatile.h +++ b/src/goto-instrument/nondet_volatile.h @@ -12,14 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H #define CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H -#include +#include bool is_volatile( - const symbol_tablet &symbol_table, - const typet &type); + const symbol_tablet &, + const typet &); -void nondet_volatile( - symbol_tablet &symbol_table, - goto_functionst &goto_functions); +void nondet_volatile(goto_modelt &); #endif // CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H diff --git a/src/goto-instrument/points_to.h b/src/goto-instrument/points_to.h index 8b4a47d980a..76775a6f636 100644 --- a/src/goto-instrument/points_to.h +++ b/src/goto-instrument/points_to.h @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include #include #include "object_id.h" @@ -26,10 +26,10 @@ class points_tot { } - void operator()(goto_functionst &goto_functions) + void operator()(goto_modelt &goto_model) { // build the CFG data structure - cfg(goto_functions); + cfg(goto_model.goto_functions); // iterate fixedpoint(); diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index aec5eedda53..b426c98815e 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -294,29 +294,29 @@ void race_check( void race_check( value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions) + goto_modelt &goto_model) { - w_guardst w_guards(symbol_table); + w_guardst w_guards(goto_model.symbol_table); - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) if(f_it->first!=goto_functionst::entry_point() && f_it->first!=CPROVER_PREFIX "initialize") race_check( value_sets, - symbol_table, + goto_model.symbol_table, L_M_ARG(f_it->second) f_it->second.body, w_guards); // get "main" goto_functionst::function_mapt::iterator - m_it=goto_functions.function_map.find(goto_functions.entry_point()); + m_it=goto_model.goto_functions.function_map.find( + goto_model.goto_functions.entry_point()); - if(m_it==goto_functions.function_map.end()) + if(m_it==goto_model.goto_functions.function_map.end()) throw "race check instrumentation needs an entry point"; goto_programt &main=m_it->second.body; w_guards.add_initialization(main); - goto_functions.update(); + goto_model.goto_functions.update(); } diff --git a/src/goto-instrument/race_check.h b/src/goto-instrument/race_check.h index 442d142ddc0..829ca529ea6 100644 --- a/src/goto-instrument/race_check.h +++ b/src/goto-instrument/race_check.h @@ -15,22 +15,17 @@ Date: February 2006 #define CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H #include -#include - -class goto_programt; +#include void race_check( - value_setst &value_sets, - class symbol_tablet &symbol_table, + value_setst &, + class symbol_tablet &, #ifdef LOCAL_MAY const goto_functionst::goto_functiont &goto_function, #endif goto_programt &goto_program ); -void race_check( - value_setst &value_sets, - class symbol_tablet &symbol_table, - goto_functionst &goto_functions); +void race_check(value_setst &, goto_modelt &); #endif // CPROVER_GOTO_INSTRUMENT_RACE_CHECK_H diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index c92333e31a3..7773aa7a760 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -80,18 +80,18 @@ void reachability_slicert::slice(goto_functionst &goto_functions) goto_functions.update(); } -void reachability_slicer(goto_functionst &goto_functions) +void reachability_slicer(goto_modelt &goto_model) { reachability_slicert s; assert_criteriont a; - s(goto_functions, a); + s(goto_model.goto_functions, a); } void reachability_slicer( - goto_functionst &goto_functions, + goto_modelt &goto_model, const std::list &properties) { reachability_slicert s; properties_criteriont p(properties); - s(goto_functions, p); + s(goto_model.goto_functions, p); } diff --git a/src/goto-instrument/reachability_slicer.h b/src/goto-instrument/reachability_slicer.h index 4d82e4b194e..25e6a19ba5b 100644 --- a/src/goto-instrument/reachability_slicer.h +++ b/src/goto-instrument/reachability_slicer.h @@ -12,12 +12,15 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H #define CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H -#include +#include +#include -void reachability_slicer(goto_functionst &goto_functions); +class goto_modelt; + +void reachability_slicer(goto_modelt &); void reachability_slicer( - goto_functionst &goto_functions, + goto_modelt &, const std::list &properties); #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-instrument/remove_function.cpp index 131438d1af6..2ec053ccac4 100644 --- a/src/goto-instrument/remove_function.cpp +++ b/src/goto-instrument/remove_function.cpp @@ -15,26 +15,25 @@ Date: April 2017 #include -#include +#include /// Remove the body of function "identifier" such that an analysis will treat it /// as a side-effect free function with non-deterministic return value. /// \par parameters: symbol_table Input symbol table to be modified -/// goto_functions Input functions to be modified +/// goto_model Input program to be modified /// identifier Function to be removed /// message_handler Error/status output void remove_function( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &goto_model, const irep_idt &identifier, message_handlert &message_handler) { messaget message(message_handler); goto_functionst::function_mapt::iterator entry= - goto_functions.function_map.find(identifier); + goto_model.goto_functions.function_map.find(identifier); - if(entry==goto_functions.function_map.end()) + if(entry==goto_model.goto_functions.function_map.end()) { message.error() << "No function " << identifier << " in goto program" << messaget::eom; @@ -52,7 +51,7 @@ void remove_function( message.status() << "Removing body of " << identifier << messaget::eom; entry->second.clear(); - symbol_table.lookup(identifier).value.make_nil(); + goto_model.symbol_table.lookup(identifier).value.make_nil(); } } @@ -60,15 +59,14 @@ void remove_function( /// will treat it as a side-effect free function with non-deterministic return /// value. /// \par parameters: symbol_table Input symbol table to be modified -/// goto_functions Input functions to be modified +/// goto_model Input program to be modified /// names List of functions to be removed /// message_handler Error/status output void remove_functions( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &goto_model, const std::list &names, message_handlert &message_handler) { for(const auto &f : names) - remove_function(symbol_table, goto_functions, f, message_handler); + remove_function(goto_model, f, message_handler); } diff --git a/src/goto-instrument/remove_function.h b/src/goto-instrument/remove_function.h index e11db1757ba..3c88b8ce803 100644 --- a/src/goto-instrument/remove_function.h +++ b/src/goto-instrument/remove_function.h @@ -19,20 +19,17 @@ Date: April 2017 #include -class goto_functionst; +class goto_modelt; class message_handlert; -class symbol_tablet; void remove_function( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &, const irep_idt &identifier, - message_handlert &message_handler); + message_handlert &); void remove_functions( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &, const std::list &names, - message_handlert &message_handler); + message_handlert &); #endif // CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H diff --git a/src/goto-instrument/rw_set.h b/src/goto-instrument/rw_set.h index 15c3766f23c..6de564f0783 100644 --- a/src/goto-instrument/rw_set.h +++ b/src/goto-instrument/rw_set.h @@ -23,7 +23,7 @@ Date: February 2006 #include #include -#include +#include #include #ifdef LOCAL_MAY @@ -203,12 +203,12 @@ class rw_set_functiont:public rw_set_baset public: rw_set_functiont( value_setst &_value_sets, - const namespacet &_ns, - const goto_functionst &_goto_functions, + const goto_modelt &_goto_model, const exprt &function): - rw_set_baset(_ns), + rw_set_baset(ns), + ns(_goto_model.symbol_table), value_sets(_value_sets), - goto_functions(_goto_functions) + goto_functions(_goto_model.goto_functions) { compute_rec(function); } @@ -216,6 +216,7 @@ class rw_set_functiont:public rw_set_baset ~rw_set_functiont() {} protected: + const namespacet ns; value_setst &value_sets; const goto_functionst &goto_functions; diff --git a/src/goto-instrument/show_locations.cpp b/src/goto-instrument/show_locations.cpp index 2b9580add2f..530ad487d7a 100644 --- a/src/goto-instrument/show_locations.cpp +++ b/src/goto-instrument/show_locations.cpp @@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + void show_locations( ui_message_handlert::uit ui, const irep_idt function_id, @@ -64,11 +66,8 @@ void show_locations( void show_locations( ui_message_handlert::uit ui, - const goto_functionst &goto_functions) + const goto_modelt &goto_model) { - for(goto_functionst::function_mapt::const_iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) - show_locations(ui, it->first, it->second.body); + for(const auto &f : goto_model.goto_functions.function_map) + show_locations(ui, f.first, f.second.body); } diff --git a/src/goto-instrument/show_locations.h b/src/goto-instrument/show_locations.h index 3f71b19ca48..af6bf185dcd 100644 --- a/src/goto-instrument/show_locations.h +++ b/src/goto-instrument/show_locations.h @@ -14,10 +14,10 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +class goto_modelt; void show_locations( ui_message_handlert::uit ui, - const goto_functionst &goto_functions); + const goto_modelt &); #endif // CPROVER_GOTO_INSTRUMENT_SHOW_LOCATIONS_H diff --git a/src/goto-instrument/skip_loops.cpp b/src/goto-instrument/skip_loops.cpp index d8be5f1e7ef..c28f2f80fe9 100644 --- a/src/goto-instrument/skip_loops.cpp +++ b/src/goto-instrument/skip_loops.cpp @@ -16,7 +16,7 @@ Date: January 2016 #include #include -#include +#include typedef std::set loop_idst; typedef std::map loop_mapt; @@ -91,7 +91,7 @@ static bool parse_loop_ids( } bool skip_loops( - goto_functionst &goto_functions, + goto_modelt &goto_model, const std::string &loop_ids, message_handlert &message_handler) { @@ -105,7 +105,7 @@ bool skip_loops( } loop_mapt::const_iterator it=loop_map.begin(); - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) { if(it==loop_map.end() || it->firstfirst) break; // possible error handled below @@ -124,7 +124,7 @@ bool skip_loops( } // update counters etc. - goto_functions.update(); + goto_model.goto_functions.update(); return false; } diff --git a/src/goto-instrument/skip_loops.h b/src/goto-instrument/skip_loops.h index c5e84c6172c..d82104436b8 100644 --- a/src/goto-instrument/skip_loops.h +++ b/src/goto-instrument/skip_loops.h @@ -16,12 +16,12 @@ Date: January 2016 #include -class goto_functionst; +class goto_modelt; class message_handlert; bool skip_loops( - goto_functionst &goto_functions, + goto_modelt &, const std::string &loop_ids, - message_handlert &message_handler); + message_handlert &); #endif // CPROVER_GOTO_INSTRUMENT_SKIP_LOOPS_H diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index df319f3deb5..2dc96cdf8bd 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -20,7 +20,7 @@ Date: November 2011 #include #include -#include +#include symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table) { @@ -84,14 +84,15 @@ void stack_depth( } void stack_depth( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &goto_model, const int depth) { - const symbol_exprt sym=add_stack_depth_symbol(symbol_table); + const symbol_exprt sym= + add_stack_depth_symbol(goto_model.symbol_table); + const exprt depth_expr(from_integer(depth, sym.type())); - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) if(f_it->second.body_available() && f_it->first!=CPROVER_PREFIX "initialize" && f_it->first!=goto_functionst::entry_point()) @@ -99,8 +100,11 @@ void stack_depth( // initialize depth to 0 goto_functionst::function_mapt::iterator - i_it=goto_functions.function_map.find(CPROVER_PREFIX "initialize"); - assert(i_it!=goto_functions.function_map.end()); + i_it=goto_model.goto_functions.function_map.find( + CPROVER_PREFIX "initialize"); + DATA_INVARIANT( + i_it!=goto_model.goto_functions.function_map.end(), + "__CPROVER_initialize must exist"); goto_programt &init=i_it->second.body; goto_programt::targett first=init.instructions.begin(); @@ -111,5 +115,5 @@ void stack_depth( it->function=first->function; // update counters etc. - goto_functions.update(); + goto_model.goto_functions.update(); } diff --git a/src/goto-instrument/stack_depth.h b/src/goto-instrument/stack_depth.h index 8d0414121d7..d63037116ac 100644 --- a/src/goto-instrument/stack_depth.h +++ b/src/goto-instrument/stack_depth.h @@ -14,12 +14,10 @@ Date: November 2011 #ifndef CPROVER_GOTO_INSTRUMENT_STACK_DEPTH_H #define CPROVER_GOTO_INSTRUMENT_STACK_DEPTH_H -class symbol_tablet; -class goto_functionst; +class goto_modelt; void stack_depth( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &, const int depth); #endif // CPROVER_GOTO_INSTRUMENT_STACK_DEPTH_H diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp index a2943424a33..c02d9360612 100644 --- a/src/goto-instrument/thread_instrumentation.cpp +++ b/src/goto-instrument/thread_instrumentation.cpp @@ -9,8 +9,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "thread_instrumentation.h" #include + #include +#include + static bool has_start_thread(const goto_programt &goto_program) { for(const auto &instruction : goto_program.instructions) @@ -53,12 +56,12 @@ void thread_exit_instrumentation(goto_programt &goto_program) end->function=function; } -void thread_exit_instrumentation(goto_functionst &goto_functions) +void thread_exit_instrumentation(goto_modelt &goto_model) { // we'll look for START THREAD std::set thread_fkts; - forall_goto_functions(f_it, goto_functions) + forall_goto_functions(f_it, goto_model.goto_functions) { if(has_start_thread(f_it->second.body)) { @@ -77,9 +80,8 @@ void thread_exit_instrumentation(goto_functionst &goto_functions) // now instrument for(const auto &fkt : thread_fkts) - { - thread_exit_instrumentation(goto_functions.function_map[fkt].body); - } + thread_exit_instrumentation( + goto_model.goto_functions.function_map[fkt].body); } void mutex_init_instrumentation( @@ -118,16 +120,14 @@ void mutex_init_instrumentation( } } -void mutex_init_instrumentation( - const symbol_tablet &symbol_table, - goto_functionst &goto_functions) +void mutex_init_instrumentation(goto_modelt &goto_model) { // get pthread_mutex_lock symbol_tablet::symbolst::const_iterator f_it= - symbol_table.symbols.find("pthread_mutex_lock"); + goto_model.symbol_table.symbols.find("pthread_mutex_lock"); - if(f_it==symbol_table.symbols.end()) + if(f_it==goto_model.symbol_table.symbols.end()) return; // get type of lock argument @@ -140,7 +140,7 @@ void mutex_init_instrumentation( if(lock_type.id()!=ID_pointer) return; - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) mutex_init_instrumentation( - symbol_table, f_it->second.body, lock_type.subtype()); + goto_model.symbol_table, f_it->second.body, lock_type.subtype()); } diff --git a/src/goto-instrument/thread_instrumentation.h b/src/goto-instrument/thread_instrumentation.h index c4c92394d72..6bda06ee6d8 100644 --- a/src/goto-instrument/thread_instrumentation.h +++ b/src/goto-instrument/thread_instrumentation.h @@ -10,10 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_THREAD_INSTRUMENTATION_H #define CPROVER_GOTO_INSTRUMENT_THREAD_INSTRUMENTATION_H -#include +class goto_modelt; -void thread_exit_instrumentation(goto_functionst &); - -void mutex_init_instrumentation(const symbol_tablet &, goto_functionst &); +void thread_exit_instrumentation(goto_modelt &); +void mutex_init_instrumentation(goto_modelt &); #endif // CPROVER_GOTO_INSTRUMENT_THREAD_INSTRUMENTATION_H diff --git a/src/goto-instrument/undefined_functions.cpp b/src/goto-instrument/undefined_functions.cpp index f76815d3009..ea5556151bf 100644 --- a/src/goto-instrument/undefined_functions.cpp +++ b/src/goto-instrument/undefined_functions.cpp @@ -15,22 +15,25 @@ Date: July 2016 #include -#include +#include + +#include void list_undefined_functions( - const goto_functionst &goto_functions, - const namespacet &ns, + const goto_modelt &goto_model, std::ostream &os) { - forall_goto_functions(it, goto_functions) + const namespacet ns(goto_model.symbol_table); + + forall_goto_functions(it, goto_model.goto_functions) if(!ns.lookup(it->first).is_macro && !it->second.body_available()) os << it->first << '\n'; } -void undefined_function_abort_path(goto_functionst &goto_functions) +void undefined_function_abort_path(goto_modelt &goto_model) { - Forall_goto_functions(it, goto_functions) + Forall_goto_functions(it, goto_model.goto_functions) Forall_goto_program_instructions(iit, it->second.body) { goto_programt::instructiont &ins=*iit; @@ -47,8 +50,10 @@ void undefined_function_abort_path(goto_functionst &goto_functions) to_symbol_expr(call.function()).get_identifier(); goto_functionst::function_mapt::const_iterator entry= - goto_functions.function_map.find(function); - assert(entry!=goto_functions.function_map.end()); + goto_model.goto_functions.function_map.find(function); + DATA_INVARIANT( + entry!=goto_model.goto_functions.function_map.end(), + "called function must be in function_map"); if(entry->second.body_available()) continue; diff --git a/src/goto-instrument/undefined_functions.h b/src/goto-instrument/undefined_functions.h index e9bb9df6f95..39b6cfe45e1 100644 --- a/src/goto-instrument/undefined_functions.h +++ b/src/goto-instrument/undefined_functions.h @@ -17,14 +17,12 @@ Date: July 2016 #include class namespacet; - -class goto_functionst; +class goto_modelt; void list_undefined_functions( - const goto_functionst &goto_functions, - const namespacet &ns, - std::ostream &os); + const goto_modelt &, + std::ostream &); -void undefined_function_abort_path(goto_functionst &goto_functions); +void undefined_function_abort_path(goto_modelt &); #endif diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index ca33c6bfbbb..5c416946213 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -194,26 +194,23 @@ void uninitializedt::add_assertions(goto_programt &goto_program) } } -void add_uninitialized_locals_assertions( - symbol_tablet &symbol_table, - goto_functionst &goto_functions) +void add_uninitialized_locals_assertions(goto_modelt &goto_model) { - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) { - uninitializedt uninitialized(symbol_table); + uninitializedt uninitialized(goto_model.symbol_table); uninitialized.add_assertions(f_it->second.body); } } void show_uninitialized( - const class symbol_tablet &symbol_table, - const goto_functionst &goto_functions, + const goto_modelt &goto_model, std::ostream &out) { - const namespacet ns(symbol_table); + const namespacet ns(goto_model.symbol_table); - forall_goto_functions(f_it, goto_functions) + forall_goto_functions(f_it, goto_model.goto_functions) { if(f_it->second.body_available()) { diff --git a/src/goto-instrument/uninitialized.h b/src/goto-instrument/uninitialized.h index 11437eee972..281d61894d2 100644 --- a/src/goto-instrument/uninitialized.h +++ b/src/goto-instrument/uninitialized.h @@ -16,15 +16,12 @@ Date: January 2010 #include -#include +#include -void add_uninitialized_locals_assertions( - class symbol_tablet &symbol_table, - goto_functionst &goto_functions); +void add_uninitialized_locals_assertions(goto_modelt &); void show_uninitialized( - const class symbol_tablet &symbol_table, - const goto_functionst &goto_functions, + const goto_modelt &, std::ostream &out); #endif // CPROVER_GOTO_INSTRUMENT_UNINITIALIZED_H diff --git a/src/goto-instrument/unwind.h b/src/goto-instrument/unwind.h index 6e86a5d98e2..6360fbaeb74 100644 --- a/src/goto-instrument/unwind.h +++ b/src/goto-instrument/unwind.h @@ -15,9 +15,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include -class goto_functionst; +class goto_modelt; // -1: do not unwind loop typedef std::map> unwind_sett; @@ -66,11 +66,30 @@ class goto_unwindt } void operator()( - goto_functionst &goto_functions, + goto_functionst &, const unwind_sett &unwind_set, const int k=-1, // -1: no global bound const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL); + void operator()( + goto_modelt &goto_model, + const unsigned k, // global bound + const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL) + { + const unwind_sett unwind_set; + operator()(goto_model.goto_functions, unwind_set, k, unwind_strategy); + } + + void operator()( + goto_modelt &goto_model, + const unwind_sett &unwind_set, + const int k=-1, // -1: no global bound + const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL) + { + operator()( + goto_model.goto_functions, unwind_set, k, unwind_strategy); + } + // unwind log jsont output_log_json() const diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h index ea2a79f8b99..c8b472e079b 100644 --- a/src/goto-instrument/wmm/goto2graph.h +++ b/src/goto-instrument/wmm/goto2graph.h @@ -20,13 +20,12 @@ Date: 2012 #include #include -#include +#include #include "event_graph.h" #include "wmm.h" -class symbol_tablet; -class goto_functionst; +class goto_modelt; class value_setst; class local_may_aliast; @@ -329,11 +328,10 @@ class instrumentert std::multimap id2cycloc; instrumentert( - symbol_tablet &_symbol_table, - goto_functionst &_goto_f, + goto_modelt &_goto_model, messaget &_message): - ns(_symbol_table), - goto_functions(_goto_f), + ns(_goto_model.symbol_table), + goto_functions(_goto_model.goto_functions), render_po_aligned(true), render_by_file(false), render_by_function(false), diff --git a/src/goto-instrument/wmm/instrumenter_pensieve.h b/src/goto-instrument/wmm/instrumenter_pensieve.h index 1e954344322..cb7afeb45dc 100644 --- a/src/goto-instrument/wmm/instrumenter_pensieve.h +++ b/src/goto-instrument/wmm/instrumenter_pensieve.h @@ -15,16 +15,14 @@ Module: Instrumenter #include "event_graph.h" #include "goto2graph.h" -class symbol_tablet; -class goto_functionst; +class goto_modelt; class namespacet; class instrumenter_pensievet:public instrumentert { public: - instrumenter_pensievet(symbol_tablet &_symbol_table, - goto_functionst &_goto_f, messaget &message) - : instrumentert(_symbol_table, _goto_f, message) + instrumenter_pensievet(goto_modelt &_goto_model, messaget &message) + : instrumentert(_goto_model, message) { } diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp index 0e1b5cbbc90..468d944f14a 100644 --- a/src/goto-instrument/wmm/weak_memory.cpp +++ b/src/goto-instrument/wmm/weak_memory.cpp @@ -106,8 +106,7 @@ void introduce_temporaries( void weak_memory( memory_modelt model, value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, @@ -135,10 +134,10 @@ void weak_memory( message.status() << "--------" << messaget::eom; // all access to shared variables is pushed into assignments - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) if(f_it->first!=CPROVER_PREFIX "initialize" && f_it->first!=goto_functionst::entry_point()) - introduce_temporaries(value_sets, symbol_table, f_it->first, + introduce_temporaries(value_sets, goto_model.symbol_table, f_it->first, f_it->second.body, #ifdef LOCAL_MAY f_it->second, @@ -148,7 +147,7 @@ void weak_memory( message.status() << "Temp added" << messaget::eom; unsigned max_thds = 0; - instrumentert instrumenter(symbol_table, goto_functions, message); + instrumentert instrumenter(goto_model, message); max_thds=instrumenter.goto2graph_cfg(value_sets, model, no_dependencies, duplicate_body); message.status()<<"abstraction completed"<::iterator it= shared_buffers.affected_by_delay_set.begin(); @@ -245,19 +246,19 @@ void weak_memory( << ran_it->second << messaget::eom; } - shared_bufferst::cfg_visitort visitor(shared_buffers, symbol_table, - goto_functions); - visitor.weak_memory(value_sets, goto_functions.entry_point(), model); + shared_bufferst::cfg_visitort visitor( + shared_buffers, goto_model.symbol_table, goto_model.goto_functions); + visitor.weak_memory( + value_sets, goto_model.goto_functions.entry_point(), model); /* removes potential skips */ - Forall_goto_functions(f_it, goto_functions) - remove_skip(f_it->second.body); + remove_skip(goto_model); // initialization code for buffers - shared_buffers.add_initialization_code(goto_functions); + shared_buffers.add_initialization_code(goto_model.goto_functions); // update counters etc. - goto_functions.update(); + goto_model.goto_functions.update(); message.status()<< "Goto-program instrumented" << messaget::eom; } diff --git a/src/goto-instrument/wmm/weak_memory.h b/src/goto-instrument/wmm/weak_memory.h index 34b98e6a767..d4eb6078174 100644 --- a/src/goto-instrument/wmm/weak_memory.h +++ b/src/goto-instrument/wmm/weak_memory.h @@ -16,20 +16,19 @@ Date: September 2011 #include "wmm.h" -#include "util/irep.h" +#include -class value_setst; -class goto_functionst; class symbol_tablet; +class value_setst; +class goto_modelt; class message_handlert; class goto_programt; class messaget; void weak_memory( memory_modelt model, - value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + value_setst &, + goto_modelt &, bool SCC, instrumentation_strategyt event_stategy, unsigned unwinding_bound, @@ -43,14 +42,14 @@ void weak_memory( bool render_function, bool cav11_option, bool hide_internals, - message_handlert &message, + message_handlert &, bool ignore_arrays); void introduce_temporaries( - value_setst &value_sets, - symbol_tablet &symbol_table, + value_setst &, + symbol_tablet &, const irep_idt &function, - goto_programt &goto_program, + goto_programt &, #ifdef LOCAL_MAY const goto_functionst::goto_functiont &goto_function, #endif diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp index 88ba69c26c0..62957297922 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -284,24 +284,25 @@ void goto_function_inline( } jsont goto_function_inline_and_log( - goto_functionst &goto_functions, + goto_modelt &goto_model, const irep_idt function, - const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching) { + const namespacet ns(goto_model.symbol_table); + goto_inlinet goto_inline( - goto_functions, + goto_model.goto_functions, ns, message_handler, adjust_function, caching); goto_functionst::function_mapt::iterator f_it= - goto_functions.function_map.find(function); + goto_model.goto_functions.function_map.find(function); - if(f_it==goto_functions.function_map.end()) + if(f_it==goto_model.goto_functions.function_map.end()) return jsont(); goto_functionst::goto_functiont &goto_function=f_it->second; @@ -326,8 +327,8 @@ jsont goto_function_inline_and_log( } goto_inline.goto_inline(function, goto_function, inline_map, true); - goto_functions.update(); - goto_functions.compute_loop_numbers(); + goto_model.goto_functions.update(); + goto_model.goto_functions.compute_loop_numbers(); return goto_inline.output_inline_log_json(); } diff --git a/src/goto-programs/goto_inline.h b/src/goto-programs/goto_inline.h index 3319aa36172..bbb4f0365e5 100644 --- a/src/goto-programs/goto_inline.h +++ b/src/goto-programs/goto_inline.h @@ -65,9 +65,8 @@ void goto_function_inline( bool caching=true); jsont goto_function_inline_and_log( - goto_functionst &goto_functions, + goto_modelt &, const irep_idt function, - const namespacet &ns, message_handlert &message_handler, bool adjust_function=false, bool caching=true); diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 02f230e8943..2153cffb040 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -24,6 +24,7 @@ Date: July 2005 #include #include +#include #include #include @@ -195,12 +196,12 @@ class goto_tracet void show_goto_trace( std::ostream &out, - const namespacet &ns, - const goto_tracet &goto_trace); + const namespacet &, + const goto_tracet &); void trace_value( std::ostream &out, - const namespacet &ns, + const namespacet &, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value); diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 34a2a46a895..1706643206f 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -137,6 +137,10 @@ bool initialize_goto_model( goto_model.symbol_table, goto_model.goto_functions, message_handler); + + // stupid hack + config.set_object_bits_from_symbol_table( + goto_model.symbol_table); } catch(const char *e) { diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 25d2be08cb8..c65bc472a46 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -1049,18 +1049,6 @@ exprt interpretert::get_value(const irep_idt &id) return get_value(get_type, integer2size_t(whole_lhs_object_address)); } -void interpreter( - const symbol_tablet &symbol_table, - const goto_functionst &goto_functions, - message_handlert &message_handler) -{ - interpretert interpreter( - symbol_table, - goto_functions, - message_handler); - interpreter(); -} - /// Prints the current state of the memory map Since messaget mdofifies class /// members, print functions are nonconst void interpretert::print_memory(bool input_flags) @@ -1079,3 +1067,15 @@ void interpretert::print_memory(bool input_flags) debug() << eom; } } + +void interpreter( + const goto_modelt &goto_model, + message_handlert &message_handler) +{ + interpretert interpreter( + goto_model.symbol_table, + goto_model.goto_functions, + message_handler); + interpreter(); +} + diff --git a/src/goto-programs/interpreter.h b/src/goto-programs/interpreter.h index 8d598852b1a..c4b84863bc7 100644 --- a/src/goto-programs/interpreter.h +++ b/src/goto-programs/interpreter.h @@ -14,11 +14,10 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "goto_functions.h" +#include "goto_model.h" void interpreter( - const symbol_tablet &symbol_table, - const goto_functionst &goto_functions, - message_handlert &message_handler); + const goto_modelt &, + message_handlert &); #endif // CPROVER_GOTO_PROGRAMS_INTERPRETER_H diff --git a/src/goto-programs/read_goto_binary.h b/src/goto-programs/read_goto_binary.h index bbaba7a5c11..1cc60e13a37 100644 --- a/src/goto-programs/read_goto_binary.h +++ b/src/goto-programs/read_goto_binary.h @@ -14,10 +14,10 @@ Author: Daniel Kroening, kroening@kroening.com #include -class symbol_tablet; class goto_functionst; -class message_handlert; class goto_modelt; +class message_handlert; +class symbol_tablet; bool read_goto_binary( const std::string &filename, diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 712aaf4b1f3..0c9a922367d 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -584,9 +584,7 @@ void remove_exceptions( /// removes throws/CATCH-POP/CATCH-PUSH void remove_exceptions(goto_modelt &goto_model) { - std::map> exceptions_map; - remove_exceptionst remove_exceptions( + remove_exceptions( goto_model.symbol_table, - exceptions_map); - remove_exceptions(goto_model.goto_functions); + goto_model.goto_functions); } diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index d74e135693b..cc3a68440c3 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -389,10 +389,8 @@ void remove_returnst::restore(goto_functionst &goto_functions) } /// restores return statements -void restore_returns( - symbol_tablet &symbol_table, - goto_functionst &goto_functions) +void restore_returns(goto_modelt &goto_model) { - remove_returnst rr(symbol_table); - rr.restore(goto_functions); + remove_returnst rr(goto_model.symbol_table); + rr.restore(goto_model.goto_functions); } diff --git a/src/goto-programs/remove_returns.h b/src/goto-programs/remove_returns.h index d4e50cae57b..04b113cff18 100644 --- a/src/goto-programs/remove_returns.h +++ b/src/goto-programs/remove_returns.h @@ -29,6 +29,8 @@ void remove_returns(goto_modelt &); // reverse the above operations void restore_returns(symbol_tablet &, goto_functionst &); +void restore_returns(goto_modelt &); + code_typet original_return_type( const symbol_tablet &symbol_table, const irep_idt &function_id); diff --git a/src/goto-programs/remove_static_init_loops.cpp b/src/goto-programs/remove_static_init_loops.cpp index e6493732b62..92554c50e4d 100644 --- a/src/goto-programs/remove_static_init_loops.cpp +++ b/src/goto-programs/remove_static_init_loops.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com /// Unwind loops in static initializers #include "remove_static_init_loops.h" +#include "goto_model.h" #include @@ -104,11 +105,10 @@ void remove_static_init_loopst::unwind_enum_static( /// \par parameters: symbol table, goto_functions and options /// \return side effect is adding loops to unwindset void remove_static_init_loops( - const symbol_tablet &symbol_table, - const goto_functionst &goto_functions, + const goto_modelt &goto_model, optionst &options, message_handlert &msg) { - remove_static_init_loopst remove_loops(symbol_table); - remove_loops.unwind_enum_static(goto_functions, options, msg); + remove_static_init_loopst remove_loops(goto_model.symbol_table); + remove_loops.unwind_enum_static(goto_model.goto_functions, options, msg); } diff --git a/src/goto-programs/remove_static_init_loops.h b/src/goto-programs/remove_static_init_loops.h index 3f781f6a70b..5c31ac527d7 100644 --- a/src/goto-programs/remove_static_init_loops.h +++ b/src/goto-programs/remove_static_init_loops.h @@ -9,18 +9,19 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Unwind loops in static initializers +#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_STATIC_INIT_LOOPS_H +#define CPROVER_GOTO_PROGRAMS_REMOVE_STATIC_INIT_LOOPS_H + #include #include #include #include -#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_STATIC_INIT_LOOPS_H -#define CPROVER_GOTO_PROGRAMS_REMOVE_STATIC_INIT_LOOPS_H +class goto_modelt; void remove_static_init_loops( - const symbol_tablet &, - const goto_functionst &, + const goto_modelt &, optionst &, message_handlert &); diff --git a/src/goto-programs/show_goto_functions.h b/src/goto-programs/show_goto_functions.h index 4f63fde97a6..8cfcbff3ad9 100644 --- a/src/goto-programs/show_goto_functions.h +++ b/src/goto-programs/show_goto_functions.h @@ -14,7 +14,6 @@ Author: Peter Schrammel #include -class goto_functionst; class namespacet; class goto_modelt; @@ -24,11 +23,6 @@ class goto_modelt; #define HELP_SHOW_GOTO_FUNCTIONS \ " --show-goto-functions show goto program\n" -void show_goto_functions( - const namespacet &ns, - ui_message_handlert::uit ui, - const goto_functionst &goto_functions); - void show_goto_functions( const goto_modelt &, ui_message_handlert::uit ui); diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h index b5564818195..98ccc8a948c 100644 --- a/src/goto-programs/show_properties.h +++ b/src/goto-programs/show_properties.h @@ -14,15 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com #include -class goto_functionst; class namespacet; class goto_modelt; -void show_properties( - const namespacet &ns, - ui_message_handlert::uit ui, - const goto_functionst &goto_functions); - void show_properties( const goto_modelt &, ui_message_handlert::uit ui); diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp index 2518a754af5..cc4f7349eb7 100644 --- a/src/goto-programs/slice_global_inits.cpp +++ b/src/goto-programs/slice_global_inits.cpp @@ -25,14 +25,13 @@ Date: December 2016 #include #include -void slice_global_inits( - const namespacet &ns, - goto_functionst &goto_functions) +void slice_global_inits(goto_modelt &goto_model) { // gather all functions reachable from the entry point - call_grapht call_graph(goto_functions); + call_grapht call_graph(goto_model); const call_grapht::grapht &graph=call_graph.graph; + goto_functionst &goto_functions=goto_model.goto_functions; std::list worklist; std::unordered_set functions_reached; diff --git a/src/goto-programs/slice_global_inits.h b/src/goto-programs/slice_global_inits.h index 25a96121961..9067bf83a57 100644 --- a/src/goto-programs/slice_global_inits.h +++ b/src/goto-programs/slice_global_inits.h @@ -14,11 +14,8 @@ Date: December 2016 #ifndef CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H #define CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H -class goto_functionst; -class namespacet; +class goto_modelt; -void slice_global_inits( - const namespacet &ns, - goto_functionst &goto_functions); +void slice_global_inits(goto_modelt &); #endif diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp index 75542144d91..bdc353ad122 100644 --- a/src/goto-programs/write_goto_binary.cpp +++ b/src/goto-programs/write_goto_binary.cpp @@ -17,18 +17,20 @@ Author: CM Wintersteiger #include #include +#include + /// Writes a goto program to disc, using goto binary format ver 2 bool write_goto_binary_v3( std::ostream &out, - const symbol_tablet &lsymbol_table, - const goto_functionst &functions, + const symbol_tablet &symbol_table, + const goto_functionst &goto_functions, irep_serializationt &irepconverter) { // first write symbol table - write_gb_word(out, lsymbol_table.symbols.size()); + write_gb_word(out, symbol_table.symbols.size()); - forall_symbols(it, lsymbol_table.symbols) + forall_symbols(it, symbol_table.symbols) { // Since version 2, symbols are not converted to ireps, // instead they are saved in a custom binary format @@ -72,13 +74,13 @@ bool write_goto_binary_v3( // now write functions, but only those with body unsigned cnt=0; - forall_goto_functions(it, functions) + forall_goto_functions(it, goto_functions) if(it->second.body_available()) cnt++; write_gb_word(out, cnt); - for(const auto &fct : functions.function_map) + for(const auto &fct : goto_functions.function_map) { if(fct.second.body_available()) { @@ -122,8 +124,21 @@ bool write_goto_binary_v3( /// Writes a goto program to disc bool write_goto_binary( std::ostream &out, - const symbol_tablet &lsymbol_table, - const goto_functionst &functions, + const goto_modelt &goto_model, + int version) +{ + return write_goto_binary( + out, + goto_model.symbol_table, + goto_model.goto_functions, + version); +} + +/// Writes a goto program to disc +bool write_goto_binary( + std::ostream &out, + const symbol_tablet &symbol_table, + const goto_functionst &goto_functions, int version) { // header @@ -143,8 +158,7 @@ bool write_goto_binary( case 3: return write_goto_binary_v3( - out, lsymbol_table, functions, - irepconverter); + out, symbol_table, goto_functions, irepconverter); default: throw "unknown goto binary version"; @@ -156,8 +170,7 @@ bool write_goto_binary( /// Writes a goto program to disc bool write_goto_binary( const std::string &filename, - const symbol_tablet &symbol_table, - const goto_functionst &goto_functions, + const goto_modelt &goto_model, message_handlert &message_handler) { std::ofstream out(filename, std::ios::binary); @@ -170,5 +183,5 @@ bool write_goto_binary( return true; } - return write_goto_binary(out, symbol_table, goto_functions); + return write_goto_binary(out, goto_model); } diff --git a/src/goto-programs/write_goto_binary.h b/src/goto-programs/write_goto_binary.h index fd3acd9cb77..d9cf23d6def 100644 --- a/src/goto-programs/write_goto_binary.h +++ b/src/goto-programs/write_goto_binary.h @@ -19,20 +19,23 @@ Author: CM Wintersteiger #include "goto_functions.h" -class symbol_tablet; -class goto_functionst; +class goto_modelt; class message_handlert; bool write_goto_binary( std::ostream &out, - const symbol_tablet &symbol_table, - const goto_functionst &goto_functions, + const goto_modelt &, + int version=GOTO_BINARY_VERSION); + +bool write_goto_binary( + std::ostream &out, + const symbol_tablet &, + const goto_functionst &, int version=GOTO_BINARY_VERSION); bool write_goto_binary( const std::string &filename, - const symbol_tablet &lsymbol_table, - const goto_functionst &goto_functions, - message_handlert &message_handler); + const goto_modelt &, + message_handlert &); #endif // CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp index 11657a78e55..8b3f9cdf082 100644 --- a/src/goto-symex/precondition.cpp +++ b/src/goto-symex/precondition.cpp @@ -10,12 +10,13 @@ Author: Daniel Kroening, kroening@kroening.com /// Symbolic Execution #include "precondition.h" +#include "goto_symex_state.h" #include #include -#include "goto_symex_state.h" +#include class preconditiont { diff --git a/src/musketeer/fence_shared.cpp b/src/musketeer/fence_shared.cpp index 4dc970c513d..01b608cc1e6 100644 --- a/src/musketeer/fence_shared.cpp +++ b/src/musketeer/fence_shared.cpp @@ -108,10 +108,11 @@ class simple_insertiont explicit simple_insertiont( messaget &_message, value_setst &_value_sets, - const symbol_tablet &_symbol_table, - const goto_functionst &_goto_functions) - :message(_message), value_sets(_value_sets), symbol_table(_symbol_table), - ns(_symbol_table), goto_functions(_goto_functions) + const goto_modelt &_goto_model): + message(_message), value_sets(_value_sets), + symbol_table(_goto_model.symbol_table), + ns(_goto_model.symbol_table), + goto_functions(_goto_model.goto_functions) {} virtual ~simple_insertiont() {} @@ -133,9 +134,8 @@ class fence_all_sharedt:public simple_insertiont fence_all_sharedt( messaget &_message, value_setst &_value_sets, - const symbol_tablet &_symbol_table, - const goto_functionst &_goto_functions) - :simple_insertiont(_message, _value_sets, _symbol_table, _goto_functions) + const goto_modelt &_goto_model): + simple_insertiont(_message, _value_sets, _goto_model) {} }; @@ -155,9 +155,8 @@ class fence_all_shared_aegt:public fence_all_sharedt fence_all_shared_aegt( messaget &_message, value_setst &_value_sets, - const symbol_tablet &_symbol_table, - const goto_functionst &_goto_functions) - :fence_all_sharedt(_message, _value_sets, _symbol_table, _goto_functions) + const goto_modelt &_goto_model): + fence_all_sharedt(_message, _value_sets, _goto_model) {} }; @@ -172,9 +171,8 @@ class fence_volatilet:public simple_insertiont fence_volatilet( messaget &_message, value_setst &_value_sets, - const symbol_tablet &_symbol_table, - const goto_functionst &_goto_functions) - :simple_insertiont(_message, _value_sets, _symbol_table, _goto_functions) + const goto_modelt &_goto_model): + simple_insertiont(_message, _value_sets, _goto_model) {} }; @@ -565,35 +563,29 @@ void fence_all_shared_aegt::fence_all_shared_aeg_explore( void fence_all_shared( message_handlert &message_handler, value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions) + goto_modelt &goto_model) { messaget message(message_handler); - fence_all_sharedt instrumenter(message, value_sets, symbol_table, - goto_functions); + fence_all_sharedt instrumenter(message, value_sets, goto_model); instrumenter.do_it(); } void fence_all_shared_aeg( message_handlert &message_handler, value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions) + goto_modelt &goto_model) { messaget message(message_handler); - fence_all_shared_aegt instrumenter(message, value_sets, symbol_table, - goto_functions); + fence_all_shared_aegt instrumenter(message, value_sets, goto_model); instrumenter.do_it(); } void fence_volatile( message_handlert &message_handler, value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions) + goto_modelt &goto_model) { messaget message(message_handler); - fence_volatilet instrumenter(message, value_sets, symbol_table, - goto_functions); + fence_volatilet instrumenter(message, value_sets, goto_model); instrumenter.do_it(); } diff --git a/src/musketeer/fence_shared.h b/src/musketeer/fence_shared.h index 370e39f817f..2aab83ab713 100644 --- a/src/musketeer/fence_shared.h +++ b/src/musketeer/fence_shared.h @@ -15,29 +15,25 @@ Author: Vincent Nimal #define CPROVER_MUSKETEER_FENCE_SHARED_H class value_setst; -class goto_functionst; -class symbol_tablet; +class goto_modelt; class message_handlert; /* finds all the shared variables (including static, global and dynamic) */ void fence_all_shared( - message_handlert &message_handler, - value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions); + message_handlert &, + value_setst &, + goto_modelt &); /* finds all the shared variables (including static, global and dynamic) */ void fence_all_shared_aeg( - message_handlert &message_handler, - value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions); + message_handlert &, + value_setst &, + goto_modelt &); /* finds all the volatile-declared variables */ void fence_volatile( - message_handlert &message_handler, - value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions); + message_handlert &, + value_setst &, + goto_modelt &); #endif // CPROVER_MUSKETEER_FENCE_SHARED_H diff --git a/src/musketeer/fencer.cpp b/src/musketeer/fencer.cpp index f62917df4e6..0c8619e3003 100644 --- a/src/musketeer/fencer.cpp +++ b/src/musketeer/fencer.cpp @@ -25,8 +25,7 @@ Author: Vincent Nimal void fence_weak_memory( memory_modelt model, value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, @@ -50,10 +49,10 @@ void fence_weak_memory( message.status() << "--------" << messaget::eom; // all access to shared variables is pushed into assignments - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) if(f_it->first!=CPROVER_PREFIX "initialize" && f_it->first!=goto_functionst::entry_point()) - introduce_temporaries(value_sets, symbol_table, f_it->first, + introduce_temporaries(value_sets, goto_model.symbol_table, f_it->first, f_it->second.body, #ifdef LOCAL_MAY f_it->second, @@ -62,7 +61,7 @@ void fence_weak_memory( message.status() << "Temporary variables added" << messaget::eom; unsigned max_thds = 0; - instrumentert instrumenter(symbol_table, goto_functions, message); + instrumentert instrumenter(goto_model, message); max_thds=instrumenter.goto2graph_cfg(value_sets, model, no_dependencies, duplicate_body); ++max_thds; @@ -167,11 +166,10 @@ void fence_weak_memory( from here*/ /* removes potential skips */ - Forall_goto_functions(f_it, goto_functions) - remove_skip(f_it->second.body); + remove_skip(goto_model); // update counters etc. - goto_functions.update(); + goto_model.goto_functions.update(); // prints the whole abstract graph if(print_graph) diff --git a/src/musketeer/fencer.h b/src/musketeer/fencer.h index b15cb631971..8788ebc4539 100644 --- a/src/musketeer/fencer.h +++ b/src/musketeer/fencer.h @@ -19,14 +19,12 @@ Author: Vincent Nimal class message_handlert; class value_setst; -class goto_functionst; -class symbol_tablet; +class goto_modelt; void fence_weak_memory( memory_modelt model, - value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + value_setst &, + goto_modelt &, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, @@ -42,7 +40,7 @@ void fence_weak_memory( bool hide_internals, bool print_graph, infer_modet mode, - message_handlert &message_handler, + message_handlert &, bool ignore_arrays); #endif // CPROVER_MUSKETEER_FENCER_H diff --git a/src/musketeer/musketeer_parse_options.cpp b/src/musketeer/musketeer_parse_options.cpp index fabb89a3add..1643ad04f57 100644 --- a/src/musketeer/musketeer_parse_options.cpp +++ b/src/musketeer/musketeer_parse_options.cpp @@ -85,11 +85,11 @@ int goto_fence_inserter_parse_optionst::doit() { register_languages(); - goto_functionst goto_functions; + goto_modelt goto_model; - get_goto_program(goto_functions); + get_goto_program(goto_model); - instrument_goto_program(goto_functions); + instrument_goto_program(goto_model); // write new binary? if(cmdline.args.size()==2) @@ -97,7 +97,7 @@ int goto_fence_inserter_parse_optionst::doit() status() << "Writing GOTO program to " << cmdline.args[1] << eom; if(write_goto_binary( - cmdline.args[1], symbol_table, goto_functions, get_message_handler())) + cmdline.args[1], goto_model, get_message_handler())) return 1; else return 0; @@ -132,17 +132,17 @@ int goto_fence_inserter_parse_optionst::doit() } void goto_fence_inserter_parse_optionst::get_goto_program( - goto_functionst &goto_functions) + goto_modelt &goto_model) { status() << "Reading GOTO program from " << cmdline.args[0] << eom; - if(read_goto_binary(cmdline.args[0], - symbol_table, goto_functions, get_message_handler())) + if(read_goto_binary( + cmdline.args[0], goto_model, get_message_handler())) throw 0; } void goto_fence_inserter_parse_optionst::instrument_goto_program( - goto_functionst &goto_functions) + goto_modelt &goto_model) { optionst options; @@ -155,9 +155,9 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program( // we add the library, as some analyses benefit - link_to_library(symbol_table, goto_functions, ui_message_handler); + link_to_library(goto_model, ui_message_handler); - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); if( cmdline.isset("mm") || cmdline.isset("all-shared") @@ -171,27 +171,26 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program( status() << "remove soundly function pointers" << eom; remove_function_pointers( get_message_handler(), - symbol_table, - goto_functions, + goto_model, cmdline.isset("pointer-check")); } if(cmdline.isset("async")) { status() << "Replace pthread_creates by __CPROVER_ASYNC_0:" << eom; - replace_async(ns, goto_functions); - goto_functions.update(); + replace_async(goto_model); + goto_model.goto_functions.update(); } // do partial inlining status() << "Partial Inlining" << eom; - goto_partial_inline(goto_functions, ns, ui_message_handler); + goto_partial_inline(goto_model, get_message_handler()); if(cmdline.isset("const-function-pointer-propagation")) { /* propagate const pointers to functions */ status() << "Propagate Constant Function Pointers" << eom; - propagate_const_function_pointers(symbol_table, goto_functions, + propagate_const_function_pointers(goto_model, get_message_handler()); } @@ -201,8 +200,7 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program( status() << "Function Pointer Removal" << eom; remove_function_pointers( get_message_handler(), - symbol_table, - goto_functions, + goto_model, cmdline.isset("pointer-check"); #endif @@ -214,18 +212,18 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program( #endif #ifndef LOCAL_MAY - value_set_analysis(goto_functions); + value_set_analysis(goto_model.goto_functions); #endif status() << "Removing asm code" << eom; - remove_asm(symbol_table, goto_functions); - goto_functions.update(); + remove_asm(goto_model); + goto_model.goto_functions.update(); if(cmdline.isset("all-shared")) { status() << "Shared variables accesses detection" << eom; - fence_all_shared(get_message_handler(), value_set_analysis, symbol_table, - goto_functions); + fence_all_shared(get_message_handler(), value_set_analysis, + goto_model); // simple analysis, coupled with script to insert; // does not transform the goto-binary return; @@ -234,7 +232,7 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program( { status() << "Shared variables accesses detection (CF)" << eom; fence_all_shared_aeg(get_message_handler(), value_set_analysis, - symbol_table, goto_functions); + goto_model); // simple analysis, coupled with script to insert; // does not transform the goto-binary return; @@ -243,8 +241,8 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program( { status() << "Detection of variables declared volatile" << eom; - fence_volatile(get_message_handler(), value_set_analysis, symbol_table, - goto_functions); + fence_volatile(get_message_handler(), value_set_analysis, + goto_model); // simple analysis, coupled with script to insert; // does not transform the goto-binary return; @@ -263,8 +261,7 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program( fence_pensieve( value_set_analysis, - symbol_table, - goto_functions, + goto_model, unwind_loops, max_po_trans, !cmdline.isset("no-po-rendering"), @@ -282,7 +279,7 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program( memory_modelt model; status() << "Fence detection for " << mm - << " via critical cycles and ILP" << eom; + << " via critical cycles and ILP" << eom; // strategy of instrumentation instrumentation_strategyt inst_strategy; @@ -355,8 +352,7 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program( fence_weak_memory( model, value_set_analysis, - symbol_table, - goto_functions, + goto_model, cmdline.isset("scc"), inst_strategy, unwind_loops, @@ -378,16 +374,16 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program( } // add failed symbols - add_failed_symbols(symbol_table); + add_failed_symbols(goto_model.symbol_table); // recalculate numbers, etc. - goto_functions.update(); + goto_model.goto_functions.update(); // add loop ids - goto_functions.compute_loop_numbers(); + goto_model.goto_functions.compute_loop_numbers(); // label the assertions - label_properties(goto_functions); + label_properties(goto_model); } /// display command line help diff --git a/src/musketeer/musketeer_parse_options.h b/src/musketeer/musketeer_parse_options.h index 13d0a07ef19..e227e4cf4a3 100644 --- a/src/musketeer/musketeer_parse_options.h +++ b/src/musketeer/musketeer_parse_options.h @@ -16,7 +16,7 @@ Module: Command Line Parsing #include #include -#include +#include #define GOTO_FENCE_INSERTER_OPTIONS \ "(scc)(one-event-per-cycle)(verbosity):" \ @@ -47,11 +47,9 @@ class goto_fence_inserter_parse_optionst: virtual void register_languages(); - void get_goto_program( - goto_functionst &goto_functions); + void get_goto_program(goto_modelt &); - void instrument_goto_program( - goto_functionst &goto_functions); + void instrument_goto_program(goto_modelt &); void set_verbosity(); }; diff --git a/src/musketeer/pensieve.cpp b/src/musketeer/pensieve.cpp index d46397f74a3..4b514dd84d0 100644 --- a/src/musketeer/pensieve.cpp +++ b/src/musketeer/pensieve.cpp @@ -18,8 +18,7 @@ Author: Vincent Nimal void fence_pensieve( value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &goto_model, unsigned unwinding_bound, unsigned input_max_po_trans, bool render_po, @@ -33,10 +32,10 @@ void fence_pensieve( message.status() << "--------" << messaget::eom; // all access to shared variables is pushed into assignments - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) if(f_it->first!=CPROVER_PREFIX "initialize" && f_it->first!=goto_functionst::entry_point()) - introduce_temporaries(value_sets, symbol_table, f_it->first, + introduce_temporaries(value_sets, goto_model.symbol_table, f_it->first, f_it->second.body, #ifdef LOCAL_MAY f_it->second, @@ -46,7 +45,7 @@ void fence_pensieve( unsigned max_thds = 0; - instrumenter_pensievet instrumenter(symbol_table, goto_functions, message); + instrumenter_pensievet instrumenter(goto_model, message); max_thds=instrumenter.goto2graph_cfg(value_sets, Power, true, no_loop); message.status() << "Abstract event graph computed" << messaget::eom; @@ -56,7 +55,7 @@ void fence_pensieve( instrumenter.set_parameters_collection(max_thds); /* necessary for correct printings */ - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); if(naive_mode) instrumenter.collect_pairs_naive(ns); @@ -64,9 +63,9 @@ void fence_pensieve( instrumenter.collect_pairs(ns); /* removes potential skips */ - Forall_goto_functions(f_it, goto_functions) + Forall_goto_functions(f_it, goto_model.goto_functions) remove_skip(f_it->second.body); // update counters etc. - goto_functions.update(); + goto_model.goto_functions.update(); } diff --git a/src/musketeer/pensieve.h b/src/musketeer/pensieve.h index 9513a26c433..a6bf34bd00c 100644 --- a/src/musketeer/pensieve.h +++ b/src/musketeer/pensieve.h @@ -16,14 +16,12 @@ Author: Vincent Nimal #include class value_setst; -class goto_functionst; -class symbol_tablet; +class goto_modelt; class message_handlert; void fence_pensieve( value_setst &value_sets, - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &, unsigned unwinding_bound, unsigned max_po_trans, bool render_po, diff --git a/src/musketeer/propagate_const_function_pointers.cpp b/src/musketeer/propagate_const_function_pointers.cpp index e58efe92429..c7078a50c19 100644 --- a/src/musketeer/propagate_const_function_pointers.cpp +++ b/src/musketeer/propagate_const_function_pointers.cpp @@ -18,8 +18,7 @@ Author: Vincent Nimal #include #include -#include -#include +#include #include #include @@ -142,10 +141,11 @@ class const_function_pointer_propagationt }; public: - const_function_pointer_propagationt(symbol_tablet &_symbol_table, - goto_functionst &_goto_functions, messaget &_message) - :symbol_table(_symbol_table), goto_functions(_goto_functions), - ns(_symbol_table), message(_message) + const_function_pointer_propagationt( + goto_modelt &_goto_model, messaget &_message): + symbol_table(_goto_model.symbol_table), + goto_functions(_goto_model.goto_functions), + ns(_goto_model.symbol_table), message(_message) {} /* Note that it only propagates from MAIN, following the CFG, without @@ -556,13 +556,12 @@ void const_function_pointer_propagationt::propagate( } void propagate_const_function_pointers( - symbol_tablet &symbol_table, - goto_functionst &goto_functions, + goto_modelt &goto_model, message_handlert &message_handler) { messaget message(message_handler); - const_function_pointer_propagationt propagation(symbol_table, - goto_functions, message); + const_function_pointer_propagationt propagation( + goto_model, message); propagation.propagate(); - goto_functions.update(); + goto_model.goto_functions.update(); } diff --git a/src/musketeer/propagate_const_function_pointers.h b/src/musketeer/propagate_const_function_pointers.h index af1b5497b41..660f57afbc5 100644 --- a/src/musketeer/propagate_const_function_pointers.h +++ b/src/musketeer/propagate_const_function_pointers.h @@ -12,8 +12,7 @@ Author: Vincent Nimal #ifndef CPROVER_MUSKETEER_PROPAGATE_CONST_FUNCTION_POINTERS_H #define CPROVER_MUSKETEER_PROPAGATE_CONST_FUNCTION_POINTERS_H -class symbol_tablet; -class goto_functionst; +class goto_modelt; class message_handlert; /* Note that it only propagates from MAIN, following the CFG, without @@ -24,8 +23,7 @@ class message_handlert; functions-based exploration in remove_function_pointers. */ void propagate_const_function_pointers( - symbol_tablet &symbol_tables, - goto_functionst &goto_functions, - message_handlert &message_handler); + goto_modelt &, + message_handlert &); #endif // CPROVER_MUSKETEER_PROPAGATE_CONST_FUNCTION_POINTERS_H diff --git a/src/musketeer/replace_async.h b/src/musketeer/replace_async.h index 9f3a85e1159..5d4a9eb27ff 100644 --- a/src/musketeer/replace_async.h +++ b/src/musketeer/replace_async.h @@ -12,17 +12,14 @@ Date: December 2013 #ifndef CPROVER_MUSKETEER_REPLACE_ASYNC_H #define CPROVER_MUSKETEER_REPLACE_ASYNC_H -#include +#include #include -class goto_functionst; -class namespacet; - -void replace_async( - const namespacet &ns, - goto_functionst &goto_functions) +void replace_async(goto_modelt &goto_model) { - Forall_goto_functions(f_it, goto_functions) + const namespacet ns(goto_model.symbol_table); + + Forall_goto_functions(f_it, goto_model.goto_functions) { goto_programt &program=f_it->second.body; diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp index 857f9e722fc..64f9d5fe071 100644 --- a/src/pointer-analysis/goto_program_dereference.cpp +++ b/src/pointer-analysis/goto_program_dereference.cpp @@ -392,18 +392,18 @@ void remove_pointers( } void remove_pointers( - goto_functionst &goto_functions, - symbol_tablet &symbol_table, + goto_modelt &goto_model, value_setst &value_sets) { - namespacet ns(symbol_table); + namespacet ns(goto_model.symbol_table); optionst options; goto_program_dereferencet - goto_program_dereference(ns, symbol_table, options, value_sets); + goto_program_dereference( + ns, goto_model.symbol_table, options, value_sets); - Forall_goto_functions(it, goto_functions) + Forall_goto_functions(it, goto_model.goto_functions) goto_program_dereference.dereference_program(it->second.body); } diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h index 5f2a76083ab..312dcc9f069 100644 --- a/src/pointer-analysis/goto_program_dereference.h +++ b/src/pointer-analysis/goto_program_dereference.h @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include #include "value_sets.h" #include "value_set_dereference.h" @@ -99,29 +99,28 @@ class goto_program_dereferencet:protected dereference_callbackt void dereference( goto_programt::const_targett target, exprt &expr, - const namespacet &ns, - value_setst &value_sets); + const namespacet &, + value_setst &); void remove_pointers( - goto_programt &goto_program, - symbol_tablet &symbol_table, - value_setst &value_sets); + goto_modelt &, + value_setst &); void remove_pointers( - goto_functionst &goto_functions, - symbol_tablet &symbol_table, - value_setst &value_sets); + goto_functionst &, + symbol_tablet &, + value_setst &); void pointer_checks( - goto_programt &goto_program, - symbol_tablet &symbol_table, - const optionst &options, - value_setst &value_sets); + goto_programt &, + symbol_tablet &, + const optionst &, + value_setst &); void pointer_checks( - goto_functionst &goto_functions, - symbol_tablet &symbol_table, - const optionst &options, - value_setst &value_sets); + goto_functionst &, + symbol_tablet &, + const optionst &, + value_setst &); #endif // CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H diff --git a/src/pointer-analysis/show_value_sets.cpp b/src/pointer-analysis/show_value_sets.cpp index ce555e2dd02..e1dc0bb938e 100644 --- a/src/pointer-analysis/show_value_sets.cpp +++ b/src/pointer-analysis/show_value_sets.cpp @@ -10,16 +10,17 @@ Author: Daniel Kroening, kroening@kroening.com /// Show Value Sets #include "show_value_sets.h" +#include "value_set_analysis.h" -#include +#include #include -#include "value_set_analysis.h" +#include void show_value_sets( ui_message_handlert::uit ui, - const goto_functionst &goto_functions, + const goto_modelt &goto_model, const value_set_analysist &value_set_analysis) { switch(ui) @@ -27,13 +28,13 @@ void show_value_sets( case ui_message_handlert::uit::XML_UI: { xmlt xml; - convert(goto_functions, value_set_analysis, xml); + convert(goto_model.goto_functions, value_set_analysis, xml); std::cout << xml << '\n'; } break; case ui_message_handlert::uit::PLAIN: - value_set_analysis.output(goto_functions, std::cout); + value_set_analysis.output(goto_model.goto_functions, std::cout); break; default: diff --git a/src/pointer-analysis/show_value_sets.h b/src/pointer-analysis/show_value_sets.h index d25b7addd4e..3b080f66e62 100644 --- a/src/pointer-analysis/show_value_sets.h +++ b/src/pointer-analysis/show_value_sets.h @@ -14,18 +14,12 @@ Author: Daniel Kroening, kroening@kroening.com #include -class goto_functionst; -class goto_programt; +class goto_modelt; class value_set_analysist; void show_value_sets( - ui_message_handlert::uit ui, - const goto_functionst &goto_functions, - const value_set_analysist &value_set_analysis); - -void show_value_sets( - ui_message_handlert::uit ui, - const goto_programt &goto_program, - const value_set_analysist &value_set_analysis); + ui_message_handlert::uit, + const goto_modelt &, + const value_set_analysist &); #endif // CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index 6d4fb84db95..ffe90729657 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -25,7 +25,7 @@ class bv_refinementt:public bv_pointerst { const namespacet *ns=nullptr; propt *prop=nullptr; - language_uit::uit ui=language_uit::uit::PLAIN; + ui_message_handlert::uit ui=ui_message_handlert::uit::PLAIN; /// Max number of times we refine a formula node unsigned max_node_refinement=5; /// Enable array refinement diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 021176d4178..50d0fcfb129 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -37,7 +37,7 @@ class string_refinementt final: public bv_refinementt { const namespacet *ns=nullptr; propt *prop=nullptr; - language_uit::uit ui=language_uit::uit::PLAIN; + ui_message_handlert::uit ui=ui_message_handlert::uit::PLAIN; unsigned refinement_bound=0; size_t string_max_length=std::numeric_limits::max(); /// Make non-deterministic character arrays have at least one character diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index d5fd98ff686..b41cf2ffe59 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -59,7 +59,7 @@ Author: Daniel Kroening, kroening@kroening.com symex_parse_optionst::symex_parse_optionst(int argc, const char **argv): parse_options_baset(SYMEX_OPTIONS, argc, argv), - language_uit(cmdline, ui_message_handler), + messaget(ui_message_handler), ui_message_handler(cmdline, "Symex " CBMC_VERSION) { } @@ -341,42 +341,15 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) if(cmdline.isset("cover")) { - std::string criterion=cmdline.get_value("cover"); - - coverage_criteriont c; - - if(criterion=="assertion" || criterion=="assertions") - c=coverage_criteriont::ASSERTION; - else if(criterion=="path" || criterion=="paths") - c=coverage_criteriont::PATH; - else if(criterion=="branch" || criterion=="branches") - c=coverage_criteriont::BRANCH; - else if(criterion=="location" || criterion=="locations") - c=coverage_criteriont::LOCATION; - else if(criterion=="decision" || criterion=="decisions") - c=coverage_criteriont::DECISION; - else if(criterion=="condition" || criterion=="conditions") - c=coverage_criteriont::CONDITION; - else if(criterion=="mcdc") - c=coverage_criteriont::MCDC; - else if(criterion=="cover") - c=coverage_criteriont::COVER; - else - { - error() << "unknown coverage criterion" << eom; - return true; - } - status() << "Instrumenting coverage goals" << eom; - instrument_cover_goals( - symbol_table, goto_model.goto_functions, c, get_message_handler()); - goto_model.goto_functions.update(); + if(instrument_cover_goals(cmdline, goto_model, get_message_handler())) + return true; } // show it? if(cmdline.isset("show-loops")) { - show_loop_ids(get_ui(), goto_model.goto_functions); + show_loop_ids(get_ui(), goto_model); return true; } diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h index 7278cbf1261..7e6f378911c 100644 --- a/src/symex/symex_parse_options.h +++ b/src/symex/symex_parse_options.h @@ -55,7 +55,7 @@ class optionst; class symex_parse_optionst: public parse_options_baset, - public language_uit + public messaget { public: virtual int doit(); @@ -80,6 +80,11 @@ class symex_parse_optionst: void eval_verbosity(); std::string get_test(const goto_tracet &goto_trace); + + ui_message_handlert::uit get_ui() const + { + return ui_message_handler.get_ui(); + } }; #endif // CPROVER_SYMEX_SYMEX_PARSE_OPTIONS_H From fc4d44a95d4dd8957240d146dec0ed883372e152 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 7 Sep 2017 13:15:23 +0100 Subject: [PATCH 3/6] use goto_modelt --- unit/analyses/call_graph.cpp | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/unit/analyses/call_graph.cpp b/unit/analyses/call_graph.cpp index adc2e75e6c8..2f249b42147 100644 --- a/unit/analyses/call_graph.cpp +++ b/unit/analyses/call_graph.cpp @@ -56,7 +56,7 @@ SCENARIO("call_graph", // void C() { } // void D() { } - symbol_tablet symbol_table; + goto_modelt goto_model; code_typet void_function_type; { @@ -68,7 +68,8 @@ SCENARIO("call_graph", calls.move_to_operands(call1); calls.move_to_operands(call2); - symbol_table.add(create_void_function_symbol("A", calls)); + goto_model.symbol_table.add( + create_void_function_symbol("A", calls)); } { @@ -80,17 +81,19 @@ SCENARIO("call_graph", calls.move_to_operands(call1); calls.move_to_operands(call2); - symbol_table.add(create_void_function_symbol("B", calls)); + goto_model.symbol_table.add( + create_void_function_symbol("B", calls)); } - symbol_table.add(create_void_function_symbol("C", code_skipt())); - symbol_table.add(create_void_function_symbol("D", code_skipt())); + goto_model.symbol_table.add( + create_void_function_symbol("C", code_skipt())); + goto_model.symbol_table.add( + create_void_function_symbol("D", code_skipt())); - goto_functionst goto_functions; stream_message_handlert msg(std::cout); - goto_convert(symbol_table, goto_functions, msg); + goto_convert(goto_model, msg); - call_grapht call_graph_from_goto_functions(goto_functions); + call_grapht call_graph_from_goto_functions(goto_model); WHEN("A call graph is constructed from the GOTO functions") { From e4498ca908d011b8aaf950ff41c5f85b5375d896 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 23 Aug 2017 14:45:46 +0100 Subject: [PATCH 4/6] brief list of symbols, from language_uit --- .../goto_instrument_parse_options.cpp | 3 +- src/goto-programs/show_symbol_table.cpp | 77 ++++++++++++++++++- src/goto-programs/show_symbol_table.h | 13 ++++ 3 files changed, 88 insertions(+), 5 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index dacfa6c8077..397dfc10536 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -41,6 +41,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -467,7 +468,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-symbol-table")) { - show_symbol_table(goto_model, get_ui()); + ::show_symbol_table(goto_model, get_ui()); return 0; } diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index eebb63dcfcd..b4230f9086b 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -23,8 +23,44 @@ void show_symbol_table_xml_ui() { } +void show_symbol_table_brief_plain( + const symbol_tablet &symbol_table, + std::ostream &out) +{ + // we want to sort alphabetically + std::set symbols; + + forall_symbols(it, symbol_table.symbols) + symbols.insert(id2string(it->first)); + + const namespacet ns(symbol_table); + + for(const std::string &id : symbols) + { + const symbolt &symbol=ns.lookup(id); + + std::unique_ptr ptr; + + if(symbol.mode=="") + ptr=get_default_language(); + else + { + ptr=get_language_from_mode(symbol.mode); + if(ptr==nullptr) + throw "symbol "+id2string(symbol.name)+" has unknown mode"; + } + + std::string type_str; + + if(symbol.type.is_not_nil()) + ptr->from_type(symbol.type, type_str, ns); + + out << symbol.name << " " << type_str << '\n'; + } +} + void show_symbol_table_plain( - const goto_modelt &goto_model, + const symbol_tablet &symbol_table, std::ostream &out) { out << '\n' << "Symbols:" << '\n' << '\n'; @@ -32,10 +68,10 @@ void show_symbol_table_plain( // we want to sort alphabetically std::set symbols; - forall_symbols(it, goto_model.symbol_table.symbols) + forall_symbols(it, symbol_table.symbols) symbols.insert(id2string(it->first)); - const namespacet ns(goto_model.symbol_table); + const namespacet ns(symbol_table); for(const std::string &id : symbols) { @@ -112,14 +148,40 @@ void show_symbol_table_plain( } } +void show_symbol_table( + const symbol_tablet &symbol_table, + ui_message_handlert::uit ui) +{ + switch(ui) + { + case ui_message_handlert::uit::PLAIN: + show_symbol_table_plain(symbol_table, std::cout); + break; + + case ui_message_handlert::uit::XML_UI: + show_symbol_table_xml_ui(); + break; + + default: + break; + } +} + void show_symbol_table( const goto_modelt &goto_model, ui_message_handlert::uit ui) +{ + show_symbol_table(goto_model.symbol_table, ui); +} + +void show_symbol_table_brief( + const symbol_tablet &symbol_table, + ui_message_handlert::uit ui) { switch(ui) { case ui_message_handlert::uit::PLAIN: - show_symbol_table_plain(goto_model, std::cout); + show_symbol_table_brief_plain(symbol_table, std::cout); break; case ui_message_handlert::uit::XML_UI: @@ -130,3 +192,10 @@ void show_symbol_table( break; } } + +void show_symbol_table_brief( + const goto_modelt &goto_model, + ui_message_handlert::uit ui) +{ + show_symbol_table_brief(goto_model.symbol_table, ui); +} diff --git a/src/goto-programs/show_symbol_table.h b/src/goto-programs/show_symbol_table.h index 5ad717e7049..82e49128967 100644 --- a/src/goto-programs/show_symbol_table.h +++ b/src/goto-programs/show_symbol_table.h @@ -14,9 +14,22 @@ Author: Daniel Kroening, kroening@kroening.com #include +class symbol_tablet; class goto_modelt; void show_symbol_table( + const symbol_tablet &, + ui_message_handlert::uit ui); + +void show_symbol_table_brief( + const symbol_tablet &, + ui_message_handlert::uit ui); + +void show_symbol_table( + const goto_modelt &, + ui_message_handlert::uit ui); + +void show_symbol_table_brief( const goto_modelt &, ui_message_handlert::uit ui); From 8c4ff7b7070548665abee173f58fdc22f993720f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 23 Aug 2017 14:05:19 +0100 Subject: [PATCH 5/6] remove spurious references to langapi/language_ui.h --- src/cbmc/bmc.h | 4 ++-- src/cbmc/cbmc_parse_options.h | 2 -- src/cbmc/cbmc_solvers.h | 6 +++--- src/cbmc/fault_localization.h | 1 - src/goto-cc/gcc_mode.h | 6 +++--- src/goto-cc/goto_cc_mode.h | 4 ++-- src/goto-diff/goto_diff.h | 8 ++++---- src/goto-diff/goto_diff_parse_options.h | 2 -- src/goto-instrument/goto_instrument_parse_options.h | 5 ++--- src/goto-programs/read_goto_binary.cpp | 2 -- src/solvers/refinement/bv_refinement.h | 4 ++-- src/solvers/refinement/string_constraint.h | 1 - src/symex/symex_parse_options.h | 2 -- .../instantiate_not_contains.cpp | 2 +- 14 files changed, 19 insertions(+), 30 deletions(-) diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 6c9a5c6bd31..c1896935460 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -57,7 +57,7 @@ class bmct:public safety_checkert // additional stuff expr_listt bmc_constraints; - void set_ui(language_uit::uit _ui) { ui=_ui; } + void set_ui(ui_message_handlert::uit _ui) { ui=_ui; } // the safety_checkert interface virtual resultt operator()( @@ -75,7 +75,7 @@ class bmct:public safety_checkert prop_convt &prop_conv; // use gui format - language_uit::uit ui; + ui_message_handlert::uit ui; virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv); diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 33c5dca4602..e0d23a986c0 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -15,8 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #include #include diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h index 02bbb8b5db9..2245ff59b70 100644 --- a/src/cbmc/cbmc_solvers.h +++ b/src/cbmc/cbmc_solvers.h @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -25,7 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include "bv_cbmc.h" @@ -123,7 +123,7 @@ class cbmc_solverst:public messaget { } - void set_ui(language_uit::uit _ui) { ui=_ui; } + void set_ui(ui_message_handlert::uit _ui) { ui=_ui; } protected: const optionst &options; @@ -131,7 +131,7 @@ class cbmc_solverst:public messaget namespacet ns; // use gui format - language_uit::uit ui; + ui_message_handlert::uit ui; std::unique_ptr get_default(); std::unique_ptr get_dimacs(); diff --git a/src/cbmc/fault_localization.h b/src/cbmc/fault_localization.h index 008bb819b1e..dd0227327e6 100644 --- a/src/cbmc/fault_localization.h +++ b/src/cbmc/fault_localization.h @@ -15,7 +15,6 @@ Author: Peter Schrammel #include #include #include -#include #include diff --git a/src/goto-cc/gcc_mode.h b/src/goto-cc/gcc_mode.h index 8d77ed29af1..e0a5fc9f4dd 100644 --- a/src/goto-cc/gcc_mode.h +++ b/src/goto-cc/gcc_mode.h @@ -14,12 +14,12 @@ Date: June 2006 #ifndef CPROVER_GOTO_CC_GCC_MODE_H #define CPROVER_GOTO_CC_GCC_MODE_H -#include - #include "compile.h" #include "goto_cc_mode.h" -class compilet; +#include + +#include class gcc_modet:public goto_cc_modet { diff --git a/src/goto-cc/goto_cc_mode.h b/src/goto-cc/goto_cc_mode.h index a0b6ea47a96..6dbad84d3ce 100644 --- a/src/goto-cc/goto_cc_mode.h +++ b/src/goto-cc/goto_cc_mode.h @@ -14,10 +14,10 @@ Date: June 2006 #ifndef CPROVER_GOTO_CC_GOTO_CC_MODE_H #define CPROVER_GOTO_CC_GOTO_CC_MODE_H -#include - #include "goto_cc_cmdline.h" +#include + class goto_cc_modet:public messaget { public: diff --git a/src/goto-diff/goto_diff.h b/src/goto-diff/goto_diff.h index 2b6a9ac923d..23a65221358 100644 --- a/src/goto-diff/goto_diff.h +++ b/src/goto-diff/goto_diff.h @@ -13,9 +13,9 @@ Author: Peter Schrammel #define CPROVER_GOTO_DIFF_GOTO_DIFF_H #include -#include -#include + #include +#include #include @@ -37,14 +37,14 @@ class goto_difft:public messaget virtual bool operator()()=0; - void set_ui(language_uit::uit _ui) { ui=_ui; } + void set_ui(ui_message_handlert::uit _ui) { ui=_ui; } virtual std::ostream &output_functions(std::ostream &out) const; protected: const goto_modelt &goto_model1; const goto_modelt &goto_model2; - language_uit::uit ui; + ui_message_handlert::uit ui; unsigned total_functions_count; typedef std::set irep_id_sett; diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index 505de8410f4..a79cd064706 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -15,8 +15,6 @@ Author: Peter Schrammel #include #include -#include - #include #include diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5dc2c017d41..2a921437603 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -82,7 +81,7 @@ Author: Daniel Kroening, kroening@kroening.com class goto_instrument_parse_optionst: public parse_options_baset, - public language_uit + public messaget { public: virtual int doit(); @@ -90,7 +89,7 @@ class goto_instrument_parse_optionst: goto_instrument_parse_optionst(int argc, const char **argv): parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv), - language_uit(cmdline, ui_message_handler), + messaget(ui_message_handler), ui_message_handler(cmdline, "goto-instrument"), function_pointer_removal_done(false), partial_inlining_done(false), diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index 2b4a3805401..9e7a1968ccc 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -30,8 +30,6 @@ Module: Read Goto Programs #include #include -#include - #include "goto_model.h" #include "link_goto_model.h" #include "read_bin_goto_object.h" diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index ffe90729657..79367186b9b 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H #define CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H -#include +#include #include @@ -114,7 +114,7 @@ class bv_refinementt:public bv_pointerst protected: // use gui format - language_uit::uit ui; + ui_message_handlert::uit ui; }; #endif // CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index c553efb8c7e..f2a19153fe6 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -20,7 +20,6 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H -#include #include #include #include diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h index 7e6f378911c..a3fb841f20b 100644 --- a/src/symex/symex_parse_options.h +++ b/src/symex/symex_parse_options.h @@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #include #include diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index 48cf3ed8e27..ed72dc6aa0c 100644 --- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -122,7 +122,7 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns) bv_refinementt::infot info; info.ns=&ns; info.prop=&sat_check; - const auto ui=language_uit::uit::PLAIN; + const auto ui=ui_message_handlert::uit::PLAIN; info.ui=ui; bv_refinementt solver(info); solver << expr; From 7d30cde2bcdf2ca5a37ff69e32909eff625a6a34 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 7 Sep 2017 13:28:36 +0100 Subject: [PATCH 6/6] missing copyright header --- unit/analyses/call_graph.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/unit/analyses/call_graph.cpp b/unit/analyses/call_graph.cpp index 2f249b42147..36b829cd103 100644 --- a/unit/analyses/call_graph.cpp +++ b/unit/analyses/call_graph.cpp @@ -1,3 +1,10 @@ +/*******************************************************************\ + +Module: Unit test for call graph generation + +Author: + +\*******************************************************************/ #include