Go to the documentation of this file.
99 bool reachability_task =
false;
102 options.
set_option(
"unreachable-instructions",
true);
103 options.
set_option(
"specific-analysis",
true);
104 reachability_task =
true;
108 options.
set_option(
"unreachable-functions",
true);
109 options.
set_option(
"specific-analysis",
true);
110 reachability_task =
true;
114 options.
set_option(
"reachable-functions",
true);
115 options.
set_option(
"specific-analysis",
true);
116 reachability_task =
true;
120 options.
set_option(
"show-local-may-alias",
true);
121 options.
set_option(
"specific-analysis",
true);
175 "simplify-slicing", !(
cmdline.
isset(
"no-simplify-slicing")));
204 options.
set_option(
"location-sensitive",
true);
211 options.
set_option(
"location-sensitive",
true);
238 if(reachability_task)
242 options.
set_option(
"specific-analysis",
false);
251 log.
status() <<
"Domain not specified, defaulting to --constants"
348 log.
error() <<
"Please give exactly one class name, "
349 <<
"and/or use -jar jarfile or --gb goto-binary"
358 std::replace(main_class.begin(), main_class.end(),
'/',
'.');
398 util_make_unique<class_hierarchyt>(lazy_goto_model.
symbol_table);
403 std::unique_ptr<abstract_goto_modelt> goto_model_ptr =
405 std::move(lazy_goto_model));
406 if(goto_model_ptr ==
nullptr)
463 if(json_file.empty())
465 else if(json_file ==
"-")
469 std::ofstream ofs(json_file);
472 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
489 if(json_file.empty())
491 else if(json_file ==
"-")
495 std::ofstream ofs(json_file);
498 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
515 if(json_file.empty())
517 else if(json_file ==
"-")
521 std::ofstream ofs(json_file);
524 log.
error() <<
"Failed to open json output '" << json_file <<
"'"
541 std::cout <<
">>>>\n";
542 std::cout <<
">>>> " << gf_entry.first <<
'\n';
543 std::cout <<
">>>>\n";
545 local_may_alias.
output(std::cout, gf_entry.second, ns);
566 const std::string outfile = options.
get_option(
"outfile");
567 std::ofstream output_stream;
568 if(!(outfile ==
"-"))
569 output_stream.open(outfile);
571 std::ostream &out((outfile ==
"-") ? std::cout : output_stream);
575 log.
error() <<
"Failed to open output file '" << outfile <<
"'"
583 std::unique_ptr<ai_baset> analyzer(
build_analyzer(goto_model, options, ns));
585 if(analyzer ==
nullptr)
587 log.
status() <<
"Task / Interpreter / Domain combination not supported"
594 (*analyzer)(goto_model);
617 goto_model, *analyzer, options, out);
622 goto_model, *analyzer, options, out);
627 goto_model, *analyzer, options, out);
640 log.
error() <<
"no analysis option given -- consider reading --help"
649 log.
status() <<
"Running GOTO functions transformation passes"
682 function.get_function_id(),
690 auto function_is_stub = [&symbol_table, &model](
const irep_idt &id) {
728 " janalyzer [-?] [-h] [--help] show help\n"
742 " --show display the abstract domains\n"
744 " --verify use the abstract domains to check assertions\n"
746 " --simplify file_name use the abstract domains to simplify the program\n"
747 " --no-simplify-slicing do not remove instructions from which no\n"
748 " property can be reached (use with --simplify)\n"
749 " --unreachable-instructions list dead code\n"
751 " --unreachable-functions list functions unreachable from the entry point\n"
753 " --reachable-functions list functions reachable from the entry point\n"
755 "Abstract interpreter options:\n"
757 " --location-sensitive use location-sensitive abstract interpreter\n"
758 " --concurrent use concurrency-aware abstract interpreter\n"
761 " --constants constant domain\n"
762 " --intervals interval domain\n"
763 " --non-null non-null domain\n"
764 " --dependence-graph data and control dependencies between instructions\n"
767 " --text file_name output results in plain text to given file\n"
769 " --json file_name output results in JSON format to given file\n"
770 " --xml file_name output results in XML format to given file\n"
771 " --dot file_name output results in DOT format to given file\n"
773 "Specific analyses:\n"
775 " --taint file_name perform taint analysis using rules in given file\n"
776 " --show-taint print taint analysis results on stdout\n"
777 " --show-local-may-alias perform procedure-local may alias analysis\n"
779 "Java Bytecode frontend options:\n"
782 "Platform options:\n"
785 "Program representations:\n"
786 " --show-parse-tree show parse tree\n"
787 " --show-symbol-table show loaded symbol table\n"
791 "Program instrumentation options:\n"
792 " --no-assertions ignore user assertions\n"
793 " --no-assumptions ignore user assumptions\n"
794 " --property id enable selected properties only\n"
797 " --version show version and exit\n"
798 " --verbosity # verbosity level\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 remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define HELP_CONFIG_PLATFORM
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.
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 set_option(const std::string &option, const bool value)
#define HELP_JAVA_GOTO_BINARY
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
void register_languages() override
function_mapt function_map
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...
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...
janalyzer_parse_optionst(int argc, const char **argv)
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
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)
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.
#define INITIALIZE_FUNCTION
std::string get_value(char option) const
virtual void set_message_handler(message_handlert &_message_handler)
#define HELP_SHOW_PROPERTIES
#define HELP_JAVA_CLASS_NAME
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)
static void transform_assertions_assumptions(goto_programt &goto_program, bool enable_assertions, bool enable_built_in_assertions, bool enable_assumptions)
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 body (see body) and parameter identifiers (see parameter_iden...
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
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
#define HELP_JAVA_METHOD_NAME
::goto_functiont goto_functiont
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
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)
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.
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
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/removed.
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.
#define CPROVER_EXIT_PARSE_ERROR
An error during parsing of the input program.