Go to the documentation of this file.
63 ui_message_handler(cmdline, std::string(
"JANALYZER ") +
CBMC_VERSION)
105 options.
set_option(
"specific-analysis",
true);
109 bool reachability_task =
false;
112 options.
set_option(
"unreachable-instructions",
true);
113 options.
set_option(
"specific-analysis",
true);
114 reachability_task =
true;
118 options.
set_option(
"unreachable-functions",
true);
119 options.
set_option(
"specific-analysis",
true);
120 reachability_task =
true;
124 options.
set_option(
"reachable-functions",
true);
125 options.
set_option(
"specific-analysis",
true);
126 reachability_task =
true;
130 options.
set_option(
"show-local-may-alias",
true);
131 options.
set_option(
"specific-analysis",
true);
185 "simplify-slicing", !(
cmdline.
isset(
"no-simplify-slicing")));
214 options.
set_option(
"location-sensitive",
true);
221 options.
set_option(
"location-sensitive",
true);
248 if(reachability_task)
252 options.
set_option(
"specific-analysis",
false);
261 status() <<
"Domain not specified, defaulting to --constants" <<
eom;
368 catch(
const std::string &e)
376 error() <<
"Numeric exception: " << e <<
eom;
414 catch(
const std::string &e)
422 error() <<
"Numeric exception: " << e <<
eom;
426 catch(
const std::bad_alloc &)
461 if(json_file.empty())
463 else if(json_file ==
"-")
467 std::ofstream ofs(json_file);
470 error() <<
"Failed to open json output `" << json_file <<
"'" <<
eom;
486 if(json_file.empty())
488 else if(json_file ==
"-")
492 std::ofstream ofs(json_file);
495 error() <<
"Failed to open json output `" << json_file <<
"'" <<
eom;
511 if(json_file.empty())
513 else if(json_file ==
"-")
517 std::ofstream ofs(json_file);
520 error() <<
"Failed to open json output `" << json_file <<
"'" <<
eom;
536 std::cout <<
">>>>\n";
537 std::cout <<
">>>> " << it->first <<
'\n';
538 std::cout <<
">>>>\n";
540 local_may_alias.
output(std::cout, it->second, ns);
561 const std::string outfile = options.
get_option(
"outfile");
562 std::ofstream output_stream;
563 if(!(outfile ==
"-"))
564 output_stream.open(outfile);
566 std::ostream &out((outfile ==
"-") ? std::cout : output_stream);
570 error() <<
"Failed to open output file `" << outfile <<
"'" <<
eom;
575 status() <<
"Selecting abstract domain" <<
eom;
579 if(analyzer ==
nullptr)
581 status() <<
"Task / Interpreter / Domain combination not supported"
587 status() <<
"Computing abstract states" <<
eom;
634 error() <<
"no analysis option given -- consider reading --help" <<
eom;
652 catch(
const std::string &e)
671 status() <<
"Removing function pointers and virtual functions" <<
eom;
696 status() <<
"Generic Property Instrumentation" <<
eom;
712 catch(
const std::string &e)
723 catch(
const std::bad_alloc &)
739 "* * Copyright (C) 2016-2018 * *\n"
740 "* * Daniel Kroening, Diffblue * *\n"
741 "* * kroening@kroening.com * *\n"
745 " janalyzer [-?] [-h] [--help] show help\n"
746 " janalyzer class name of class or JAR file to be checked\n"
747 " In the case of a JAR file, if a main class can be\n"
748 " inferred from --main-class, --function, or the JAR\n"
749 " manifest (checked in this order), the behavior is\n"
750 " the same as running janalyzer on the corresponding\n"
754 " --show display the abstract domains\n"
756 " --verify use the abstract domains to check assertions\n"
758 " --simplify file_name use the abstract domains to simplify the program\n"
759 " --unreachable-instructions list dead code\n"
761 " --unreachable-functions list functions unreachable from the entry point\n"
763 " --reachable-functions list functions reachable from the entry point\n"
765 "Abstract interpreter options:\n"
767 " --location-sensitive use location-sensitive abstract interpreter\n"
768 " --concurrent use concurrency-aware abstract interpreter\n"
771 " --constants constant domain\n"
772 " --intervals interval domain\n"
773 " --non-null non-null domain\n"
774 " --dependence-graph data and control dependencies between instructions\n"
777 " --text file_name output results in plain text to given file\n"
779 " --json file_name output results in JSON format to given file\n"
780 " --xml file_name output results in XML format to given file\n"
781 " --dot file_name output results in DOT format to given file\n"
783 "Specific analyses:\n"
785 " --taint file_name perform taint analysis using rules in given file\n"
787 "Java Bytecode frontend options:\n"
788 " --classpath dir/jar set the classpath\n"
789 " --main-class class-name set the name of the main class\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"
bool taint_analysis(goto_modelt &goto_model, const std::string &taint_file_name, message_handlert &message_handler, bool show_full, const std::string &json_file_name)
Class that provides messages with a built-in verbosity 'level'.
const char * CBMC_VERSION
#define HELP_SHOW_GOTO_FUNCTIONS
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
Non-graph-based representation of the class hierarchy.
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
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...
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
void remove_exceptions_using_instanceof(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
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)
virtual bool process_goto_program(const optionst &options)
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.
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
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)
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
void remove_virtual_functions(const 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...
virtual void register_languages()
std::unique_ptr< languaget > new_java_bytecode_language()
bool static_verifier(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Runs the analyzer and then prints out the domain.
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
#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)
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
void label_properties(goto_modelt &goto_model)
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)
static void remove_vector(typet &)
removes vector data type
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)
virtual int doit() override
invoke main modules
mstreamt & result() const
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)
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
ui_message_handlert ui_message_handler
std::string get_value(char option) const
#define HELP_SHOW_PROPERTIES
static irep_idt this_operating_system()
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
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.
void compute_loop_numbers()
ui_message_handlert::uit get_ui()
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
static void remove_complex(typet &)
removes complex data type
static irep_idt this_architecture()
void remove_instanceof(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...
message_handlert & get_message_handler()
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
virtual void get_command_line_options(optionst &options)
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
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)
bool get_bool_option(const std::string &option) const
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
The basic interface of an abstract interpreter.
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
#define forall_goto_functions(it, functions)
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
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
const std::list< std::string > & get_values(const std::string &option) const
symbol_tablet symbol_table
Symbol table.