Go to the documentation of this file.
112 options.
set_option(
"specific-analysis",
true);
116 bool reachability_task =
false;
119 options.
set_option(
"unreachable-instructions",
true);
120 options.
set_option(
"specific-analysis",
true);
121 reachability_task =
true;
125 options.
set_option(
"unreachable-functions",
true);
126 options.
set_option(
"specific-analysis",
true);
127 reachability_task =
true;
131 options.
set_option(
"reachable-functions",
true);
132 options.
set_option(
"specific-analysis",
true);
133 reachability_task =
true;
137 options.
set_option(
"show-local-may-alias",
true);
138 options.
set_option(
"specific-analysis",
true);
192 "simplify-slicing", !(
cmdline.
isset(
"no-simplify-slicing")));
221 options.
set_option(
"location-sensitive",
true);
228 options.
set_option(
"location-sensitive",
true);
255 if(reachability_task)
259 options.
set_option(
"specific-analysis",
false);
268 log.
status() <<
"Domain not specified, defaulting to --constants"
370 log.
error() <<
"Please give exactly one class name, "
371 <<
"and/or use -jar jarfile or --gb goto-binary"
380 std::replace(main_class.begin(), main_class.end(),
'/',
'.');
420 util_make_unique<class_hierarchyt>(lazy_goto_model.
symbol_table);
425 std::unique_ptr<abstract_goto_modelt> goto_model_ptr =
427 std::move(lazy_goto_model));
428 if(goto_model_ptr ==
nullptr)
485 if(json_file.empty())
487 else if(json_file ==
"-")
491 std::ofstream ofs(json_file);
494 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
511 if(json_file.empty())
513 else if(json_file ==
"-")
517 std::ofstream ofs(json_file);
520 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
537 if(json_file.empty())
539 else if(json_file ==
"-")
543 std::ofstream ofs(json_file);
546 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
563 std::cout <<
">>>>\n";
564 std::cout <<
">>>> " << it->first <<
'\n';
565 std::cout <<
">>>>\n";
567 local_may_alias.
output(std::cout, it->second, ns);
588 const std::string outfile = options.
get_option(
"outfile");
589 std::ofstream output_stream;
590 if(!(outfile ==
"-"))
591 output_stream.open(outfile);
593 std::ostream &out((outfile ==
"-") ? std::cout : output_stream);
597 log.
error() <<
"Failed to open output file '" << outfile <<
"'"
605 std::unique_ptr<ai_baset> analyzer(
build_analyzer(goto_model, options, ns));
607 if(analyzer ==
nullptr)
609 log.
status() <<
"Task / Interpreter / Domain combination not supported"
616 (*analyzer)(goto_model);
639 goto_model, *analyzer, options, out);
644 goto_model, *analyzer, options, out);
649 goto_model, *analyzer, options, out);
662 log.
error() <<
"no analysis option given -- consider reading --help"
671 log.
status() <<
"Running GOTO functions transformation passes"
704 function.get_function_id(),
712 auto function_is_stub = [&symbol_table, &model](
const irep_idt &id) {
721 function.get_function_id(),
function.get_goto_function(), ns, options);
752 " janalyzer [-?] [-h] [--help] show help\n"
766 " --show display the abstract domains\n"
768 " --verify use the abstract domains to check assertions\n"
770 " --simplify file_name use the abstract domains to simplify the program\n"
771 " --unreachable-instructions list dead code\n"
773 " --unreachable-functions list functions unreachable from the entry point\n"
775 " --reachable-functions list functions reachable from the entry point\n"
777 "Abstract interpreter options:\n"
779 " --location-sensitive use location-sensitive abstract interpreter\n"
780 " --concurrent use concurrency-aware abstract interpreter\n"
783 " --constants constant domain\n"
784 " --intervals interval domain\n"
785 " --non-null non-null domain\n"
786 " --dependence-graph data and control dependencies between instructions\n"
789 " --text file_name output results in plain text to given file\n"
791 " --json file_name output results in JSON format to given file\n"
792 " --xml file_name output results in XML format to given file\n"
793 " --dot file_name output results in DOT format to given file\n"
795 "Specific analyses:\n"
797 " --taint file_name perform taint analysis using rules in given file\n"
799 "Java Bytecode frontend options:\n"
802 "Program representations:\n"
803 " --show-parse-tree show parse tree\n"
804 " --show-symbol-table show loaded symbol table\n"
808 "Program instrumentation options:\n"
812 " --version show version and exit\n"
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define HELP_SHOW_GOTO_FUNCTIONS
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
virtual void show_parse(std::ostream &out)=0
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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...
std::unique_ptr< class_hierarchyt > class_hierarchy
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
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)
#define CHECK_RETURN(CONDITION)
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 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.
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)
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 register_languages()
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::unique_ptr< languaget > new_java_bytecode_language()
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Functions for replacing virtual function call with a static function calls in functions,...
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...
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)
#define HELP_JAVA_GOTO_BINARY
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
void label_properties(goto_modelt &goto_model)
virtual void set_language_options(const optionst &)
Set language-specific options.
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...
virtual void help() override
display command line help
virtual void usage_error()
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Remove the 'complex' data type by compilation into structs.
janalyzer_parse_optionst(int argc, const char **argv)
Set the properties to check.
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.
virtual int perform_analysis(goto_modelt &goto_model, const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
const char * CBMC_VERSION
virtual int doit() override
invoke main modules
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
std::string banner_string(const std::string &front_end, const std::string &version)
Field-insensitive, location-sensitive may-alias analysis.
A GOTO model that produces function bodies on demand.
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
The symbol table base class interface.
Over-approximate Concurrency for Threaded Goto Programs.
#define INITIALIZE_FUNCTION
std::string get_value(char option) const
Abstract interface to support a programming language.
virtual void set_message_handler(message_handlert &_message_handler)
List all unreachable instructions.
#define HELP_SHOW_PROPERTIES
#define HELP_JAVA_CLASS_NAME
static irep_idt this_operating_system()
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
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.
A goto function, consisting of function type (see type), function body (see body),...
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 ...
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &model, const optionst &options)
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
nonstd::optional< T > optionalt
JANALYZER Command Line Option Processing.
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
#define HELP_JAVA_METHOD_NAME
Remove the 'vector' data type by compilation into arrays.
Replace function returns by assignments to global variables.
Remove function exceptional returns.
Remove Instance-of Operators.
::goto_functiont goto_functiont
static irep_idt this_architecture()
exprt value
Initial value of symbol.
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
void get_command_line_options(optionst &options)
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)
bool set(const cmdlinet &cmdline)
#define HELP_JAVA_CLASSPATH
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)
Base class for concurrency-aware abstract interpretation.
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.
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
struct configt::javat java
bool can_generate_function_body(const irep_idt &name)
#define forall_goto_functions(it, functions)
Abstract interface to eager or lazy GOTO models.
void load_all_functions() const
Eagerly loads all functions from the symbol table.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Goto Programs with Functions.
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.
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.
#define JANALYZER_OPTIONS
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...
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)
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
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 const symbol_tablet & get_symbol_table() const override
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
#define CPROVER_EXIT_PARSE_ERROR
An error during parsing of the input program.