Go to the documentation of this file.
79 std::string(
"GOTO-ANALYZER "))
147 options.
set_option(
"specific-analysis",
true);
151 bool reachability_task =
false;
154 options.
set_option(
"unreachable-instructions",
true);
155 options.
set_option(
"specific-analysis",
true);
156 reachability_task =
true;
160 options.
set_option(
"unreachable-functions",
true);
161 options.
set_option(
"specific-analysis",
true);
162 reachability_task =
true;
166 options.
set_option(
"reachable-functions",
true);
167 options.
set_option(
"specific-analysis",
true);
168 reachability_task =
true;
172 options.
set_option(
"show-local-may-alias",
true);
173 options.
set_option(
"specific-analysis",
true);
218 "cannot output goto binary to stdout",
"--simplify");
258 options.
set_option(
"recursive-interprocedural",
true);
265 options.
set_option(
"one-domain-per-location",
true);
270 options.
set_option(
"legacy-concurrent",
true);
273 options.
set_option(
"one-domain-per-location",
true);
283 options.
set_option(
"one-domain-per-location",
true);
302 options.
set_option(
"local-control-flow-history",
true);
303 options.
set_option(
"local-control-flow-history-forward",
false);
304 options.
set_option(
"local-control-flow-history-backward",
true);
311 options.
set_option(
"local-control-flow-history",
true);
312 options.
set_option(
"local-control-flow-history-forward",
true);
313 options.
set_option(
"local-control-flow-history-backward",
false);
320 options.
set_option(
"local-control-flow-history",
true);
321 options.
set_option(
"local-control-flow-history-forward",
true);
322 options.
set_option(
"local-control-flow-history-backward",
true);
324 "local-control-flow-history-limit",
332 log.
status() <<
"History not specified, defaulting to --ahistorical"
362 if(reachability_task)
366 options.
set_option(
"specific-analysis",
false);
375 log.
status() <<
"Domain not specified, defaulting to --constants"
385 options.
set_option(
"one-domain-per-history",
true);
390 options.
set_option(
"one-domain-per-location",
true);
400 <<
" defaulting to --one-domain-per-history" <<
messaget::eom;
401 options.
set_option(
"one-domain-per-history",
true);
407 options.
set_option(
"validate-goto-model",
true);
422 std::unique_ptr<ai_history_factory_baset> hf =
nullptr;
430 hf = util_make_unique<call_stack_history_factoryt>(
435 hf = util_make_unique<local_control_flow_history_factoryt>(
442 std::unique_ptr<ai_domain_factory_baset> df =
nullptr;
457 std::unique_ptr<ai_storage_baset> st =
nullptr;
460 st = util_make_unique<history_sensitive_storaget>();
464 st = util_make_unique<location_sensitive_storaget>();
469 if(hf !=
nullptr && df !=
nullptr && st !=
nullptr)
474 std::move(hf), std::move(df), std::move(st));
605 if(json_file.empty())
607 else if(json_file==
"-")
611 std::ofstream ofs(json_file);
614 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
630 if(json_file.empty())
632 else if(json_file==
"-")
636 std::ofstream ofs(json_file);
639 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
655 if(json_file.empty())
657 else if(json_file==
"-")
661 std::ofstream ofs(json_file);
664 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
681 std::cout <<
">>>>\n";
682 std::cout <<
">>>> " << it->first <<
'\n';
683 std::cout <<
">>>>\n";
685 local_may_alias.
output(std::cout, it->second, ns);
706 const std::string outfile=options.
get_option(
"outfile");
708 std::ofstream output_stream;
709 if(outfile !=
"-" && !outfile.empty())
710 output_stream.open(outfile);
713 (outfile ==
"-" || outfile.empty()) ? std::cout : output_stream);
717 log.
error() <<
"Failed to open output file '" << outfile <<
"'"
727 if(analyzer ==
nullptr)
729 log.
status() <<
"Task / Interpreter combination not supported"
761 output_stream.close();
799 log.
error() <<
"no analysis option given -- consider reading --help"
826 log.
status() <<
"Removing function pointers and virtual functions"
869 " goto-analyzer [-h] [--help] show help\n"
870 " goto-analyzer file.c ... source file names\n"
873 " --show display the abstract states on the goto program\n"
874 " --show-on-source display the abstract states on the source\n"
876 " --verify use the abstract domains to check assertions\n"
878 " --simplify file_name use the abstract domains to simplify the program\n"
879 " --unreachable-instructions list dead code\n"
881 " --unreachable-functions list functions unreachable from the entry point\n"
883 " --reachable-functions list functions reachable from the entry point\n"
885 "Abstract interpreter options:\n"
887 " --recursive-interprocedural use recursion to handle interprocedural reasoning\n"
889 " --legacy-ait recursion for function and one domain per location\n"
891 " --legacy-concurrent legacy-ait with an extended fixed-point for concurrency\n"
895 " --ahistorical the most basic history, tracks locations only\n"
897 " --call-stack n track the calling location stack for each function\n"
899 " limiting to at most n recursive loops, 0 to disable\n"
901 " --loop-unwind n track the number of loop iterations within a function\n"
903 " limited to n histories per location, 0 is unlimited\n"
905 " --branching n track the forwards jumps (if, switch, etc.) within a function\n"
907 " limited to n histories per location, 0 is unlimited\n"
909 " --loop-unwind-and-branching n track all local control flow\n"
911 " limited to n histories per location, 0 is unlimited\n"
914 " --constants a constant for each variable if possible\n"
915 " --intervals an interval for each variable\n"
916 " --non-null tracks which pointers are non-null\n"
917 " --dependence-graph data and control dependencies between instructions\n"
921 " --one-domain-per-history stores a domain for each history object created\n"
922 " --one-domain-per-location stores a domain for each location reached\n"
925 " --text file_name output results in plain text to given file\n"
927 " --json file_name output results in JSON format to given file\n"
928 " --xml file_name output results in XML format to given file\n"
929 " --dot file_name output results in DOT format to given file\n"
931 "Specific analyses:\n"
933 " --taint file_name perform taint analysis using rules in given file\n"
935 "C/C++ frontend options:\n"
936 " -I path set include path (C/C++)\n"
937 " -D macro define preprocessor macro (C/C++)\n"
938 " --arch X set architecture (default: "
940 " --os set operating system (default: "
942 " --c89/99/11 set C language standard (default: "
950 " --cpp98/03/11 set C++ language standard (default: "
961 " --gcc use GCC as preprocessor\n"
963 " --no-library disable built-in abstract C library\n"
966 "Program representations:\n"
967 " --show-parse-tree show parse tree\n"
968 " --show-symbol-table show loaded symbol table\n"
972 "Program instrumentation options:\n"
977 " --version show version and exit\n"
#define UNREACHABLE
This should be used to mark dead code.
#define HELP_SHOW_GOTO_FUNCTIONS
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
ui_message_handlert ui_message_handler
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
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.
virtual bool isset(char option) const
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
void static_verifier(const abstract_goto_modelt &abstract_goto_model, const ai_baset &ai, propertiest &properties)
Use the information from the abstract interpreter to fill out the statuses of the passed properties.
virtual void get_command_line_options(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.
Track function-local control flow for loop unwinding and path senstivity.
const std::string get_option(const std::string &option) const
mstreamt & status() const
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
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...
Goto-Analyser Command Line Option Processing.
Functions for replacing virtual function call with a static function calls in functions,...
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
void set_option(const std::string &option, const bool value)
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
struct configt::ansi_ct ansi_c
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...
goto_analyzer_parse_optionst(int argc, const char **argv)
void label_properties(goto_modelt &goto_model)
virtual void usage_error()
std::unique_ptr< languaget > new_cpp_language()
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
static void remove_vector(typet &)
removes vector data type
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Remove the 'complex' data type by compilation into structs.
Set the properties to check.
const char * CBMC_VERSION
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
virtual bool process_goto_program(const optionst &options)
Initialize a Goto Program.
std::string banner_string(const std::string &front_end, const std::string &version)
Field-insensitive, location-sensitive may-alias analysis.
An easy factory implementation for histories that don't need parameters.
#define PRECONDITION(CONDITION)
Over-approximate Concurrency for Threaded Goto Programs.
std::string get_value(char option) const
virtual int doit() override
invoke main modules
Abstract interface to support a programming language.
List all unreachable instructions.
#define HELP_SHOW_PROPERTIES
static irep_idt this_operating_system()
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
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.
virtual void help() override
display command line help
void compute_loop_numbers()
#define GOTO_ANALYSER_OPTIONS
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
unsigned int get_unsigned_int_option(const std::string &option) const
static c_standardt default_c_standard()
void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
Some variables have different initial values based on what flags are being passed to cbmc; since the ...
Remove the 'vector' data type by compilation into arrays.
static void remove_complex(typet &)
removes complex data type
Replace function returns by assignments to global variables.
virtual void register_languages()
static irep_idt this_architecture()
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
goto_functionst goto_functions
GOTO functions.
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
bool set(const cmdlinet &cmdline)
static cpp_standardt default_cpp_standard()
Document and give macros for the exit codes of CPROVER binaries.
bool get_bool_option(const std::string &option) const
bool taint_analysis(goto_modelt &goto_model, const std::string &taint_file_name, message_handlert &message_handler, bool show_full, const optionalt< std::string > &json_file_name)
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
This is the basic interface of the abstract interpreter with default implementations of the core func...
std::unique_ptr< languaget > new_ansi_c_language()
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
static std::string binary(const constant_exprt &src)
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...
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
#define forall_goto_functions(it, functions)
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Goto Programs with Functions.
History for tracking the call stack and performing interprocedural analysis.
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
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
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.
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, const irep_idt &function_id, bool add_safety_assertion, bool only_remove_const_fps)
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const std::list< std::string > & get_values(const std::string &option) const
Remove Indirect Function Calls.
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
symbol_tablet symbol_table
Symbol table.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
std::unique_ptr< languaget > new_jsil_language()