72 ui_message_handler(cmdline, std::string(
"GOTO-ANALYZER ") +
CBMC_VERSION)
136 options.
set_option(
"specific-analysis",
true);
140 bool reachability_task =
false;
143 options.
set_option(
"unreachable-instructions",
true);
144 options.
set_option(
"specific-analysis",
true);
145 reachability_task =
true;
149 options.
set_option(
"unreachable-functions",
true);
150 options.
set_option(
"specific-analysis",
true);
151 reachability_task =
true;
155 options.
set_option(
"reachable-functions",
true);
156 options.
set_option(
"specific-analysis",
true);
157 reachability_task =
true;
161 options.
set_option(
"show-local-may-alias",
true);
162 options.
set_option(
"specific-analysis",
true);
212 "cannot output goto binary to stdout",
"--simplify");
252 options.
set_option(
"location-sensitive",
true);
259 options.
set_option(
"location-sensitive",
true);
286 if(reachability_task)
290 options.
set_option(
"specific-analysis",
false);
299 status() <<
"Domain not specified, defaulting to --constants" <<
eom;
307 options.
set_option(
"validate-goto-model",
true);
411 catch(
const std::string &e)
419 error() <<
"Numeric exception: " << e <<
eom;
462 catch(
const std::string &e)
470 error() <<
"Numeric exception: " << e <<
eom;
474 catch(
const std::bad_alloc &)
511 if(json_file.empty())
513 else if(json_file==
"-")
517 std::ofstream ofs(json_file);
520 error() <<
"Failed to open json output `" 521 << json_file <<
"'" <<
eom;
536 if(json_file.empty())
538 else if(json_file==
"-")
542 std::ofstream ofs(json_file);
545 error() <<
"Failed to open json output `" 546 << json_file <<
"'" <<
eom;
561 if(json_file.empty())
563 else if(json_file==
"-")
567 std::ofstream ofs(json_file);
570 error() <<
"Failed to open json output `" 571 << json_file <<
"'" <<
eom;
587 std::cout <<
">>>>\n";
588 std::cout <<
">>>> " << it->first <<
'\n';
589 std::cout <<
">>>>\n";
591 local_may_alias.
output(std::cout, it->second, ns);
612 const std::string outfile=options.
get_option(
"outfile");
614 std::ofstream output_stream;
615 if(outfile !=
"-" && !outfile.empty())
616 output_stream.open(outfile);
619 (outfile ==
"-" || outfile.empty()) ? std::cout : output_stream);
623 error() <<
"Failed to open output file `" 624 << outfile <<
"'" <<
eom;
629 status() <<
"Selecting abstract domain" <<
eom;
633 if(analyzer ==
nullptr)
635 status() <<
"Task / Interpreter / Domain combination not supported" 641 status() <<
"Computing abstract states" <<
eom;
670 output_stream.close();
711 error() <<
"no analysis option given -- consider reading --help" 730 catch(
const std::string &e)
762 status() <<
"Removing function pointers and virtual functions" <<
eom;
777 status() <<
"Generic Property Instrumentation" <<
eom;
796 catch(
const std::string &e)
807 catch(
const std::bad_alloc &)
822 "* * Copyright (C) 2017-2018 * *\n" 823 "* * Daniel Kroening, Diffblue * *\n" 824 "* * kroening@kroening.com * *\n" 828 " goto-analyzer [-h] [--help] show help\n" 829 " goto-analyzer file.c ... source file names\n" 832 " --show display the abstract states on the goto program\n" 833 " --show-on-source display the abstract states on the source\n" 835 " --verify use the abstract domains to check assertions\n" 837 " --simplify file_name use the abstract domains to simplify the program\n" 838 " --unreachable-instructions list dead code\n" 840 " --unreachable-functions list functions unreachable from the entry point\n" 842 " --reachable-functions list functions reachable from the entry point\n" 844 "Abstract interpreter options:\n" 846 " --location-sensitive use location-sensitive abstract interpreter\n" 847 " --concurrent use concurrency-aware abstract interpreter\n" 850 " --constants constant domain\n" 851 " --intervals interval domain\n" 852 " --non-null non-null domain\n" 853 " --dependence-graph data and control dependencies between instructions\n" 856 " --text file_name output results in plain text to given file\n" 858 " --json file_name output results in JSON format to given file\n" 859 " --xml file_name output results in XML format to given file\n" 860 " --dot file_name output results in DOT format to given file\n" 862 "Specific analyses:\n" 864 " --taint file_name perform taint analysis using rules in given file\n" 866 "C/C++ frontend options:\n" 867 " -I path set include path (C/C++)\n" 868 " -D macro define preprocessor macro (C/C++)\n" 869 " --arch X set architecture (default: " 871 " --os set operating system (default: " 873 " --c89/99/11 set C language standard (default: " 881 " --cpp98/03/11 set C++ language standard (default: " 892 " --gcc use GCC as preprocessor\n" 894 " --no-library disable built-in abstract C library\n" 898 "Program representations:\n" 899 " --show-parse-tree show parse tree\n" 900 " --show-symbol-table show loaded symbol table\n" 904 "Program instrumentation options:\n" 909 " --version show version and exit\n"
const std::list< std::string > & get_values(const std::string &option) const
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, symbol_tablet &, message_handlert &)> &library)
Complete missing function definitions using the library.
struct configt::ansi_ct ansi_c
Over-approximate Concurrency for Threaded Goto Programs.
std::unique_ptr< languaget > new_cpp_language()
std::unique_ptr< languaget > new_jsil_language()
Remove Indirect Function Calls.
Functions for replacing virtual function call with a static function calls in functions,...
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
goto_analyzer_parse_optionst(int argc, const char **argv)
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
void compute_loop_numbers()
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Remove the 'complex' data type by compilation into structs.
Goto-Analyser Command Line Option Processing.
std::string get_value(char option) const
symbol_tablet symbol_table
Symbol table.
void static_show_domain(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Runs the analyzer and then prints out the domain.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
Set the properties to check.
void show_on_source(const std::string &source_file, const goto_modelt &goto_model, const ai_baset &ai, message_handlert &message_handler)
output source code annotated with abstract states for given file
bool set(const cmdlinet &cmdline)
bool taint_analysis(goto_modelt &goto_model, const std::string &taint_file_name, message_handlert &message_handler, bool show_full, const std::string &json_file_name)
virtual bool isset(char option) const
Initialize a Goto Program.
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
ui_message_handlert ui_message_handler
const std::string get_option(const std::string &option) const
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
ai_baset * build_analyzer(const optionst &, const namespacet &ns)
For the task, build the appropriate kind of analyzer Ideally this should be a pure function of option...
bool get_bool_option(const std::string &option) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Abstract interface to support a programming language.
#define PRECONDITION(CONDITION)
virtual bool process_goto_program(const optionst &options)
bool static_simplifier(goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Simplifies the program using the information in the abstract domain.
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
virtual void register_languages()
virtual void help() override
display command line help
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
void validate(const validation_modet vm) const
Check that the goto model is well-formed.
Class that provides messages with a built-in verbosity 'level'.
#define GOTO_ANALYSER_OPTIONS
std::string banner_string(const std::string &front_end, const std::string &version)
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
static c_standardt default_c_standard()
virtual void get_command_line_options(optionst &options)
List all unreachable instructions.
static irep_idt this_operating_system()
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
bool static_verifier(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Runs the analyzer and then prints out the domain.
message_handlert & get_message_handler()
Goto Programs with Functions.
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & result() const
mstreamt & status() const
#define HELP_SHOW_GOTO_FUNCTIONS
const char * CBMC_VERSION
The basic interface of an abstract interpreter.
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
static std::string binary(const constant_exprt &src)
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
std::unique_ptr< languaget > new_ansi_c_language()
Remove the 'vector' data type by compilation into arrays.
ui_message_handlert::uit get_ui()
virtual void usage_error()
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
void set_option(const std::string &option, const bool value)
static void remove_complex(typet &)
removes complex data type
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
#define forall_goto_functions(it, functions)
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
static cpp_standardt default_cpp_standard()
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
Field-insensitive, location-sensitive may-alias analysis.
virtual int doit() override
invoke main modules
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)