55 std::string(
"GOTO-ANALYZER "))
88 options.
set_option(
"unreachable-instructions",
true);
94 options.
set_option(
"unreachable-functions",
true);
100 options.
set_option(
"reachable-functions",
true);
101 options.
set_option(
"specific-analysis",
true);
106 options.
set_option(
"show-local-may-alias",
true);
107 options.
set_option(
"specific-analysis",
true);
152 "cannot output goto binary to stdout",
"--simplify");
192 options.
set_option(
"recursive-interprocedural",
true);
201 options.
set_option(
"one-domain-per-location",
true);
206 options.
set_option(
"legacy-concurrent",
true);
209 options.
set_option(
"one-domain-per-location",
true);
219 options.
set_option(
"one-domain-per-location",
true);
238 options.
set_option(
"local-control-flow-history",
true);
239 options.
set_option(
"local-control-flow-history-forward",
false);
240 options.
set_option(
"local-control-flow-history-backward",
true);
247 options.
set_option(
"local-control-flow-history",
true);
248 options.
set_option(
"local-control-flow-history-forward",
true);
249 options.
set_option(
"local-control-flow-history-backward",
false);
256 options.
set_option(
"local-control-flow-history",
true);
257 options.
set_option(
"local-control-flow-history-forward",
true);
258 options.
set_option(
"local-control-flow-history-backward",
true);
260 "local-control-flow-history-limit",
268 log.
status() <<
"History not specified, defaulting to --ahistorical"
304 options.
set_option(
"dependence-graph-vs",
true);
308 options.
set_option(
"data-dependencies",
true);
317 options.
set_option(
"specific-analysis",
false);
326 log.
status() <<
"Domain not specified, defaulting to --constants"
336 options.
set_option(
"one-domain-per-history",
true);
341 options.
set_option(
"one-domain-per-location",
true);
351 <<
" defaulting to --one-domain-per-history" <<
messaget::eom;
352 options.
set_option(
"one-domain-per-history",
true);
358 options.
set_option(
"validate-goto-model",
true);
388 gcc_version.
get(
"gcc");
531 std::cout <<
">>>>\n";
532 std::cout <<
">>>> " <<
gf_entry.first <<
'\n';
533 std::cout <<
">>>>\n";
556 const std::string outfile=options.
get_option(
"outfile");
559 if(outfile !=
"-" && !outfile.empty())
563 (outfile ==
"-" || outfile.empty()) ? std::cout :
output_stream);
567 log.
error() <<
"Failed to open output file '" << outfile <<
"'"
589 log.
status() <<
"Task / Interpreter combination not supported"
658 log.
error() <<
"no analysis option given -- consider reading --help"
695 "Usage: \tPurpose:\n"
697 " {bgoto-analyzer} [{y-?}|{y-h}|{y--help}] \t show this help\n"
698 " {bgoto-analyzer} {ufile.c...} \t source file names\n"
701 " {y--show} \t display the abstract states on the goto program\n"
702 " {y--show-on-source} \t display the abstract states on the source\n"
703 " {y--verify} \t use the abstract domains to check assertions\n"
704 " {y--simplify} {ufile_name} \t use the abstract domains to simplify the"
706 " {y--no-simplify-slicing} \t do not remove instructions from which no"
707 " property can be reached (use with {y--simplify})\n"
708 " {y--unreachable-instructions} \t list dead code\n"
709 " {y--unreachable-functions} \t list functions unreachable from the entry"
711 " {y--reachable-functions} \t list functions reachable from the entry"
714 "Abstract interpreter options:\n"
715 " {y--legacy-ait} \t recursion for function and one domain per location\n"
716 " {y--recursive-interprocedural} \t use recursion to handle interprocedural"
718 " {y--three-way-merge} \t use VSD's three-way merge on return from function"
720 " {y--legacy-concurrent} \t legacy-ait with an extended fixed-point for"
722 " {y--location-sensitive} \t use location-sensitive abstract interpreter\n"
725 " {y--ahistorical} \t the most basic history, tracks locations only\n"
726 " {y--call-stack} {un} \t track the calling location stack for each"
727 " function limiting to at most {un} recursive loops, 0 to disable\n"
728 " {y--loop-unwind} {un} \t track the number of loop iterations within a"
729 " function limited to {un} histories per location, 0 is unlimited\n"
730 " {y--branching} {un} \t track the forwards jumps (if, switch, etc.) within"
731 " a function limited to {un} histories per location, 0 is unlimited\n"
732 " {y--loop-unwind-and-branching} {un} \t track all local control flow"
733 " limited to {un} histories per location, 0 is unlimited\n"
736 " {y--constants} \t a constant for each variable if possible\n"
737 " {y--intervals} \t an interval for each variable\n"
738 " {y--non-null} \t tracks which pointers are non-null\n"
739 " {y--dependence-graph} \t data and control dependencies between"
741 " {y--vsd}, {y--variable-sensitivity} \t a configurable non-relational"
743 " {y--dependence-graph-vs} \t dependencies between instructions using VSD\n"
745 "Variable sensitivity domain (VSD) options:\n"
749 " {y--one-domain-per-location} \t stores a domain for each location"
751 " {y--one-domain-per-history} \t stores a domain for each history object"
755 " {y--text} {ufile_name} \t output results in plain text to given file\n"
756 " {y--json} {ufile_name} \t output results in JSON format to given file\n"
757 " {y--xml} {ufile_name} \t output results in XML format to given file\n"
758 " {y--dot} {ufile_name} \t output results in DOT format to given file\n"
760 "Specific analyses:\n"
761 " {y--taint} {ufile_name} \t perform taint analysis using rules in given"
763 " {y--show-taint} \t print taint analysis results on stdout\n"
764 " {y--show-local-may-alias} \t perform procedure-local may alias analysis\n"
766 "C/C++ frontend options:\n"
770 "Platform options:\n"
773 "Program representations:\n"
774 " {y--show-parse-tree} \t show parse tree\n"
775 " {y--show-symbol-table} \t show loaded symbol table\n"
779 "Program instrumentation options:\n"
780 " {y--property} {uid} \t enable selected properties only\n"
786 " {y--version} \t show version and exit\n"
788 " {y--verbosity} {u#} \t verbosity level\n"
void cprover_c_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
std::unique_ptr< ai_baset > build_analyzer(const optionst &options, const goto_modelt &goto_model, const namespacet &ns, message_handlert &mh)
Ideally this should be a pure function of options.
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)
struct configt::ansi_ct ansi_c
void get(const std::string &executable)
virtual int doit() override
invoke main modules
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)
void register_languages() override
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...
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()
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
ui_message_handlert ui_message_handler
#define HELP_CONFIG_LIBRARY
#define HELP_CONFIG_PLATFORM
#define HELP_CONFIG_C_CPP
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
static void show_goto_functions(const goto_modelt &goto_model)
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 configure_gcc(const gcc_versiont &gcc_version)
Goto-Analyser Command Line Option Processing.
#define GOTO_ANALYSER_OPTIONS
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, const symbol_tablet &, symbol_tablet &, message_handlert &)> &library)
Complete missing function definitions using the library.
Field-insensitive, location-sensitive may-alias analysis.
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.
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.
#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_table_baset &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.
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)
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.
#define PARSE_OPTIONS_VSD(cmdline, options)
const char * CBMC_VERSION