104 options.
set_option(
"specific-analysis",
true);
108 bool reachability_task =
false;
111 options.
set_option(
"unreachable-instructions",
true);
112 options.
set_option(
"specific-analysis",
true);
113 reachability_task =
true;
117 options.
set_option(
"unreachable-functions",
true);
118 options.
set_option(
"specific-analysis",
true);
119 reachability_task =
true;
123 options.
set_option(
"reachable-functions",
true);
124 options.
set_option(
"specific-analysis",
true);
125 reachability_task =
true;
129 options.
set_option(
"show-local-may-alias",
true);
130 options.
set_option(
"specific-analysis",
true);
184 "simplify-slicing", !(
cmdline.
isset(
"no-simplify-slicing")));
213 options.
set_option(
"location-sensitive",
true);
220 options.
set_option(
"location-sensitive",
true);
247 if(reachability_task)
251 options.
set_option(
"specific-analysis",
false);
260 log.
status() <<
"Domain not specified, defaulting to --constants"
357 log.
error() <<
"Please give exactly one class name, "
358 <<
"and/or use -jar jarfile or --gb goto-binary"
367 std::replace(main_class.begin(), main_class.end(),
'/',
'.');
387 language->set_language_options(options);
398 language->show_parse(std::cout);
407 util_make_unique<class_hierarchyt>(lazy_goto_model.
symbol_table);
412 std::unique_ptr<abstract_goto_modelt> goto_model_ptr =
414 std::move(lazy_goto_model));
415 if(goto_model_ptr ==
nullptr)
472 if(json_file.empty())
474 else if(json_file ==
"-")
478 std::ofstream ofs(json_file);
481 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
498 if(json_file.empty())
500 else if(json_file ==
"-")
504 std::ofstream ofs(json_file);
507 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
524 if(json_file.empty())
526 else if(json_file ==
"-")
530 std::ofstream ofs(json_file);
533 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
550 std::cout <<
">>>>\n";
551 std::cout <<
">>>> " << gf_entry.first <<
'\n';
552 std::cout <<
">>>>\n";
554 local_may_alias.
output(std::cout, gf_entry.second, ns);
575 const std::string outfile = options.
get_option(
"outfile");
576 std::ofstream output_stream;
577 if(!(outfile ==
"-"))
578 output_stream.open(outfile);
580 std::ostream &out((outfile ==
"-") ? std::cout : output_stream);
584 log.
error() <<
"Failed to open output file '" << outfile <<
"'"
592 std::unique_ptr<ai_baset> analyzer(
build_analyzer(goto_model, options, ns));
594 if(analyzer ==
nullptr)
596 log.
status() <<
"Task / Interpreter / Domain combination not supported"
603 (*analyzer)(goto_model);
626 goto_model, *analyzer, options, out);
631 goto_model, *analyzer, options, out);
636 goto_model, *analyzer, options, out);
649 log.
error() <<
"no analysis option given -- consider reading --help"
658 log.
status() <<
"Running GOTO functions transformation passes"
691 function.get_function_id(),
699 auto function_is_stub = [&symbol_table, &model](
const irep_idt &id) {
708 function.get_function_id(),
709 function.get_goto_function(),
743 " janalyzer [-?] [-h] [--help] show help\n"
757 " --show display the abstract domains\n"
759 " --verify use the abstract domains to check assertions\n"
761 " --simplify file_name use the abstract domains to simplify the program\n"
762 " --unreachable-instructions list dead code\n"
764 " --unreachable-functions list functions unreachable from the entry point\n"
766 " --reachable-functions list functions reachable from the entry point\n"
768 "Abstract interpreter options:\n"
770 " --location-sensitive use location-sensitive abstract interpreter\n"
771 " --concurrent use concurrency-aware abstract interpreter\n"
774 " --constants constant domain\n"
775 " --intervals interval domain\n"
776 " --non-null non-null domain\n"
777 " --dependence-graph data and control dependencies between instructions\n"
780 " --text file_name output results in plain text to given file\n"
782 " --json file_name output results in JSON format to given file\n"
783 " --xml file_name output results in XML format to given file\n"
784 " --dot file_name output results in DOT format to given file\n"
786 "Specific analyses:\n"
788 " --taint file_name perform taint analysis using rules in given file\n"
790 "Java Bytecode frontend options:\n"
793 "Program representations:\n"
794 " --show-parse-tree show parse tree\n"
795 " --show-symbol-table show loaded symbol table\n"
799 "Program instrumentation options:\n"
803 " --version show version and exit\n"
std::unique_ptr< languaget > new_ansi_c_language()
Abstract interface to eager or lazy GOTO models.
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
This is the basic interface of the abstract interpreter with default implementations of the core func...
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
Base class for concurrency-aware abstract interpretation.
bool set(const cmdlinet &cmdline)
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
janalyzer_parse_optionst(int argc, const char **argv)
void help() override
display command line help
bool can_generate_function_body(const irep_idt &name)
ai_baset * build_analyzer(goto_modelt &goto_model, const optionst &, const namespacet &ns)
For the task, build the appropriate kind of analyzer Ideally this should be a pure function of option...
std::unique_ptr< class_hierarchyt > class_hierarchy
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
void get_command_line_options(optionst &options)
virtual int perform_analysis(goto_modelt &goto_model, const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
int doit() override
invoke main modules
void register_languages() override
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &model, const optionst &options)
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
virtual const symbol_tablet & get_symbol_table() const override
A GOTO model that produces function bodies on demand.
void load_all_functions() const
Eagerly loads all functions from the symbol table.
static lazy_goto_modelt from_handler_object(THandler &handler, const optionst &options, message_handlert &message_handler)
Create a lazy_goto_modelt from a object that defines function/module pass handlers.
void initialize(const std::vector< std::string > &files, const optionst &options)
Performs initial symbol table and language_filest initialization from a given commandline and parsed ...
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
static std::unique_ptr< goto_modelt > process_whole_model_and_freeze(lazy_goto_modelt &&model)
The model returned here has access to the functions we've already loaded but is frozen in the sense t...
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
The symbol table base class interface.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
exprt value
Initial value of symbol.
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_PARSE_ERROR
An error during parsing of the input program.
#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 goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
Checks for Errors in C and Java Programs.
#define HELP_GOTO_CHECK_JAVA
JANALYZER Command Line Option Processing.
#define JANALYZER_OPTIONS
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
std::unique_ptr< languaget > new_java_bytecode_language()
#define HELP_JAVA_METHOD_NAME
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define HELP_JAVA_GOTO_BINARY
#define HELP_JAVA_CLASSPATH
#define HELP_JAVA_CLASS_NAME
Abstract interface to support a programming language.
Field-insensitive, location-sensitive may-alias analysis.
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
nonstd::optional< T > optionalt
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_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
Remove function exceptional returns.
void remove_instanceof(const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
Remove Instance-of Operators.
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Replace function returns by assignments to global variables.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void remove_virtual_functions(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
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_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 CHECK_RETURN(CONDITION)
#define INITIALIZE_FUNCTION
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.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
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.
const char * CBMC_VERSION