82 std::string(
"GOTO-ANALYZER "))
115 options.
set_option(
"specific-analysis",
true);
119 bool reachability_task =
false;
122 options.
set_option(
"unreachable-instructions",
true);
123 options.
set_option(
"specific-analysis",
true);
124 reachability_task =
true;
128 options.
set_option(
"unreachable-functions",
true);
129 options.
set_option(
"specific-analysis",
true);
130 reachability_task =
true;
134 options.
set_option(
"reachable-functions",
true);
135 options.
set_option(
"specific-analysis",
true);
136 reachability_task =
true;
140 options.
set_option(
"show-local-may-alias",
true);
141 options.
set_option(
"specific-analysis",
true);
186 "cannot output goto binary to stdout",
"--simplify");
226 options.
set_option(
"recursive-interprocedural",
true);
235 options.
set_option(
"one-domain-per-location",
true);
240 options.
set_option(
"legacy-concurrent",
true);
243 options.
set_option(
"one-domain-per-location",
true);
253 options.
set_option(
"one-domain-per-location",
true);
272 options.
set_option(
"local-control-flow-history",
true);
273 options.
set_option(
"local-control-flow-history-forward",
false);
274 options.
set_option(
"local-control-flow-history-backward",
true);
281 options.
set_option(
"local-control-flow-history",
true);
282 options.
set_option(
"local-control-flow-history-forward",
true);
283 options.
set_option(
"local-control-flow-history-backward",
false);
290 options.
set_option(
"local-control-flow-history",
true);
291 options.
set_option(
"local-control-flow-history-forward",
true);
292 options.
set_option(
"local-control-flow-history-backward",
true);
294 "local-control-flow-history-limit",
302 log.
status() <<
"History not specified, defaulting to --ahistorical"
333 "data-dependencies",
cmdline.
isset(
"vsd-data-dependencies"));
339 options.
set_option(
"dependence-graph-vs",
true);
340 options.
set_option(
"data-dependencies",
true);
347 if(reachability_task)
351 options.
set_option(
"specific-analysis",
false);
360 log.
status() <<
"Domain not specified, defaulting to --constants"
370 options.
set_option(
"one-domain-per-history",
true);
375 options.
set_option(
"one-domain-per-location",
true);
385 <<
" defaulting to --one-domain-per-history" <<
messaget::eom;
386 options.
set_option(
"one-domain-per-history",
true);
392 options.
set_option(
"validate-goto-model",
true);
404 auto vs_object_factory =
413 std::unique_ptr<ai_history_factory_baset> hf =
nullptr;
421 hf = util_make_unique<call_stack_history_factoryt>(
426 hf = util_make_unique<local_control_flow_history_factoryt>(
433 std::unique_ptr<ai_domain_factory_baset> df =
nullptr;
446 df = util_make_unique<variable_sensitivity_domain_factoryt>(
447 vs_object_factory, vsd_config);
454 std::unique_ptr<ai_storage_baset> st =
nullptr;
457 st = util_make_unique<history_sensitive_storaget>();
461 st = util_make_unique<location_sensitive_storaget>();
466 if(hf !=
nullptr && df !=
nullptr && st !=
nullptr)
471 std::move(hf), std::move(df), std::move(st));
479 std::move(hf), std::move(df), std::move(st));
502 auto df = util_make_unique<variable_sensitivity_domain_factoryt>(
503 vs_object_factory, vsd_config);
623 if(json_file.empty())
625 else if(json_file==
"-")
629 std::ofstream ofs(json_file);
632 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
648 if(json_file.empty())
650 else if(json_file==
"-")
654 std::ofstream ofs(json_file);
657 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
673 if(json_file.empty())
675 else if(json_file==
"-")
679 std::ofstream ofs(json_file);
682 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
699 std::cout <<
">>>>\n";
700 std::cout <<
">>>> " << gf_entry.first <<
'\n';
701 std::cout <<
">>>>\n";
703 local_may_alias.
output(std::cout, gf_entry.second, ns);
724 const std::string outfile=options.
get_option(
"outfile");
726 std::ofstream output_stream;
727 if(outfile !=
"-" && !outfile.empty())
728 output_stream.open(outfile);
731 (outfile ==
"-" || outfile.empty()) ? std::cout : output_stream);
735 log.
error() <<
"Failed to open output file '" << outfile <<
"'"
743 std::unique_ptr<ai_baset> analyzer;
755 if(analyzer ==
nullptr)
757 log.
status() <<
"Task / Interpreter combination not supported"
789 output_stream.close();
826 log.
error() <<
"no analysis option given -- consider reading --help"
865 " goto-analyzer [-h] [--help] show help\n"
866 " goto-analyzer file.c ... source file names\n"
869 " --show display the abstract states on the goto program\n"
870 " --show-on-source display the abstract states on the source\n"
872 " --verify use the abstract domains to check assertions\n"
874 " --simplify file_name use the abstract domains to simplify the program\n"
875 " --unreachable-instructions list dead code\n"
877 " --unreachable-functions list functions unreachable from the entry point\n"
879 " --reachable-functions list functions reachable from the entry point\n"
881 "Abstract interpreter options:\n"
883 " --recursive-interprocedural use recursion to handle interprocedural reasoning\n"
885 " --three-way-merge use VSD's three-way merge on return from function call\n"
887 " --legacy-ait recursion for function and one domain per location\n"
889 " --legacy-concurrent legacy-ait with an extended fixed-point for concurrency\n"
893 " --ahistorical the most basic history, tracks locations only\n"
895 " --call-stack n track the calling location stack for each function\n"
897 " limiting to at most n recursive loops, 0 to disable\n"
899 " --loop-unwind n track the number of loop iterations within a function\n"
901 " limited to n histories per location, 0 is unlimited\n"
903 " --branching n track the forwards jumps (if, switch, etc.) within a function\n"
905 " limited to n histories per location, 0 is unlimited\n"
907 " --loop-unwind-and-branching n track all local control flow\n"
909 " limited to n histories per location, 0 is unlimited\n"
912 " --constants a constant for each variable if possible\n"
913 " --intervals an interval for each variable\n"
914 " --non-null tracks which pointers are non-null\n"
915 " --dependence-graph data and control dependencies between instructions\n"
916 " --vsd a configurable non-relational domain\n"
917 " --dependence-graph-vs dependencies between instructions using VSD\n"
919 "Variable sensitivity domain (VSD) options:\n"
920 " --vsd-values value tracking - constants|intervals|set-of-constants\n"
921 " --vsd-structs struct field sensitive analysis - top-bottom|every-field\n"
922 " --vsd-arrays array entry sensitive analysis - top-bottom|every-element\n"
923 " --vsd-pointers pointer sensitive analysis - top-bottom|constants|value-set\n"
924 " --vsd-unions union sensitive analysis - top-bottom\n"
925 " --vsd-flow-insensitive disables flow sensitivity\n"
926 " --vsd-data-dependencies track data dependencies\n"
930 " --one-domain-per-history stores a domain for each history object created\n"
931 " --one-domain-per-location stores a domain for each location reached\n"
934 " --text file_name output results in plain text to given file\n"
936 " --json file_name output results in JSON format to given file\n"
937 " --xml file_name output results in XML format to given file\n"
938 " --dot file_name output results in DOT format to given file\n"
940 "Specific analyses:\n"
942 " --taint file_name perform taint analysis using rules in given file\n"
944 "C/C++ frontend options:\n"
948 "Platform options:\n"
951 "Program representations:\n"
952 " --show-parse-tree show parse tree\n"
953 " --show-symbol-table show loaded symbol table\n"
957 "Program instrumentation options:\n"
963 " --version show version and exit\n"
980 options.
set_option(
"flow-insensitive", cmdline.
isset(
"vsd-flow-insensitive"));
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 ...
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
std::unique_ptr< languaget > new_ansi_c_language()
History for tracking the call stack and performing interprocedural analysis.
This is the basic interface of the abstract interpreter with default implementations of the core func...
An easy factory implementation for histories that don't need parameters.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::string get_value(char option) const
virtual bool isset(char option) const
const std::list< std::string > & get_values(const std::string &option) const
bool set(const cmdlinet &cmdline)
static irep_idt this_architecture()
static irep_idt this_operating_system()
struct configt::ansi_ct ansi_c
virtual int doit() override
invoke main modules
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...
virtual void register_languages()
virtual void get_command_line_options(optionst &options)
goto_analyzer_parse_optionst(int argc, const char **argv)
virtual bool process_goto_program(const optionst &options)
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
virtual void help() override
display command line help
function_mapt function_map
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.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
std::string what() const override
A human readable description of what went wrong.
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
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.
mstreamt & status() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
unsigned int get_unsigned_int_option(const std::string &option) const
bool get_bool_option(const std::string &option) const
void set_option(const std::string &option, const bool value)
const std::string get_option(const std::string &option) const
virtual void usage_error()
ui_message_handlert ui_message_handler
static variable_sensitivity_object_factory_ptrt configured_with(const vsd_configt &options)
#define HELP_CONFIG_LIBRARY
#define HELP_CONFIG_PLATFORM
#define HELP_CONFIG_C_CPP
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
std::unique_ptr< languaget > new_cpp_language()
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
void vsd_options(optionst &options, const cmdlinet &cmdline)
Goto-Analyser Command Line Option Processing.
#define GOTO_ANALYSER_OPTIONS
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Goto Programs with Functions.
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
Over-approximate Concurrency for Threaded Goto Programs.
std::unique_ptr< languaget > new_jsil_language()
static std::string binary(const constant_exprt &src)
Abstract interface to support a programming language.
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.
Track function-local control flow for loop unwinding and path senstivity.
Field-insensitive, location-sensitive may-alias analysis.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
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...
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
Functions for replacing virtual function call with a static function calls in functions,...
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
#define HELP_SHOW_GOTO_FUNCTIONS
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
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
#define PRECONDITION(CONDITION)
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.
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.
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.
static vsd_configt from_options(const optionst &options)
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)
An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivit...
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
List all unreachable instructions.
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...
A forked and modified version of analyses/dependence_graph.
There are different ways of handling arrays, structures, unions and pointers.
Tracks the user-supplied configuration for VSD and build the correct type of abstract object when nee...
const char * CBMC_VERSION