62 ui_message_handler(cmdline,
"GOTO-ANALYZER " CBMC_VERSION)
157 <<
sizeof(
void *)*8 <<
"-bit " 192 if(json_file.empty())
194 else if(json_file==
"-")
198 std::ofstream ofs(json_file);
201 error() <<
"Failed to open json output `" 202 << json_file <<
"'" <<
eom;
216 if(json_file.empty())
218 else if(json_file==
"-")
222 std::ofstream ofs(json_file);
225 error() <<
"Failed to open json output `" 226 << json_file <<
"'" <<
eom;
240 if(json_file.empty())
242 else if(json_file==
"-")
246 std::ofstream ofs(json_file);
249 error() <<
"Failed to open json output `" 250 << json_file <<
"'" <<
eom;
266 std::cout <<
">>>>\n";
267 std::cout <<
">>>> " << it->first <<
'\n';
268 std::cout <<
">>>>\n";
270 local_may_alias.
output(std::cout, it->second, ns);
305 error() <<
"no analysis option given -- consider reading --help" 324 catch(
const std::string e)
353 status() <<
"Removing function pointers and virtual functions" <<
eom;
374 status() <<
"Generic Property Instrumentation" <<
eom;
405 catch(
const std::string e)
416 catch(std::bad_alloc)
430 "* * GOTO-ANALYSER " CBMC_VERSION " - Copyright (C) 2016 ";
432 std::cout <<
"(" << (
sizeof(
void *)*8) <<
"-bit version)";
434 std::cout <<
" * *\n";
437 "* * Daniel Kroening, DiffBlue * *\n" 438 "* * kroening@kroening.com * *\n" 442 " goto-analyzer [-h] [--help] show help\n" 443 " goto-analyzer file.c ... source file names\n" 448 " --taint file_name perform taint analysis using rules in given file\n" 449 " --unreachable-instructions list dead code\n" 451 " --unreachable-functions list functions unreachable from the entry point\n" 453 " --reachable-functions list functions reachable from the entry point\n" 454 " --intervals interval analysis\n" 455 " --non-null non-null analysis\n" 457 "Analysis options:\n" 459 " --json file_name output results in JSON format to given file\n" 460 " --xml file_name output results in XML format to given file\n" 462 "C/C++ frontend options:\n" 463 " -I path set include path (C/C++)\n" 464 " -D macro define preprocessor macro (C/C++)\n" 465 " --arch X set architecture (default: " 467 " --os set operating system (default: " 469 " --c89/99/11 set C language standard (default: " 477 " --cpp98/03/11 set C++ language standard (default: " 488 " --gcc use GCC as preprocessor\n" 490 " --no-library disable built-in abstract C library\n" 492 "Java Bytecode frontend options:\n" 493 " --classpath dir/jar set the classpath\n" 494 " --main-class class-name set the name of the main class\n" 496 "Program representations:\n" 497 " --show-parse-tree show parse tree\n" 498 " --show-symbol-table show symbol table\n" 501 " --show-properties show the properties, but don't run analysis\n" 503 "Program instrumentation options:\n" 507 " --version show version and exit\n"
const std::list< std::string > & get_values(const std::string &option) const
struct configt::ansi_ct ansi_c
Remove function exceptional returns.
Remove Instance-of Operators.
void remove_asm(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes assembler
Remove Indirect Function Calls.
Remove Virtual Function (Method) Calls.
goto_analyzer_parse_optionst(int argc, const char **argv)
void goto_check(const namespacet &ns, const optionst &options, goto_functionst::goto_functiont &goto_function)
unsigned unsafe_string2unsigned(const std::string &str, int base)
languaget * new_ansi_c_language()
Remove the 'complex' data type by compilation into structs.
Goto-Analyser Command Line Option Processing.
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler)
std::string get_value(char option) const
void show_properties(const namespacet &ns, const irep_idt &identifier, ui_message_handlert::uit ui, const goto_programt &goto_program)
virtual void show_symbol_table(bool brief=false)
symbol_tablet symbol_table
static mstreamt & eom(mstreamt &m)
Remove 'asm' statements by compiling into suitable standard code.
void remove_exceptions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes throws/CATCH-POP/CATCH-PUSH
void remove_virtual_functions(const symbol_tablet &symbol_table, goto_functionst &goto_functions)
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...
Set the properties to check.
void compute_loop_numbers()
bool set(const cmdlinet &cmdline)
languaget * new_jsil_language()
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)
virtual bool isset(char option) const
void remove_instanceof(symbol_tablet &symbol_table, goto_functionst &goto_functions)
See function above.
Initialize a Goto Program.
void show_intervals(const goto_modelt &goto_model, std::ostream &out)
ui_message_handlert ui_message_handler
Abstract interface to support a programming language.
virtual bool process_goto_program(const optionst &options)
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)
languaget * new_cpp_language()
virtual void register_languages()
virtual void help() override
display command line help
#define GOTO_ANALYSER_OPTIONS
languaget * new_java_bytecode_language()
static c_standardt default_c_standard()
virtual void get_command_line_options(optionst &options)
List all unreachable instructions.
static irep_idt this_operating_system()
message_handlert & get_message_handler()
Goto Programs with Functions.
#define HELP_SHOW_GOTO_FUNCTIONS
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
bool static_analyzer(const goto_modelt &goto_model, const optionst &options, message_handlert &message_handler)
void remove_returns(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
Remove the 'vector' data type by compilation into arrays.
void set_verbosity(unsigned _verbosity)
virtual void usage_error()
void register_language(language_factoryt factory)
void set_option(const std::string &option, const bool value)
static void remove_complex(typet &)
removes complex data type
void show_goto_functions(const namespacet &ns, ui_message_handlert::uit ui, const goto_functionst &goto_functions)
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
#define forall_goto_functions(it, functions)
static cpp_standardt default_cpp_standard()
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
void label_properties(goto_modelt &goto_model)
bool initialize_goto_model(goto_modelt &goto_model, const cmdlinet &cmdline, message_handlert &message_handler)
goto_functionst goto_functions
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
Field-insensitive, location-sensitive may-alias analysis.
virtual int doit() override
invoke main modules