241 catch(
const std::string error_msg)
247 catch(
const char *error_msg)
276 catch(
const std::string e)
302 status() <<
"Generic Property Instrumentation" <<
eom;
309 status() <<
"Removal of function pointers and virtual functions" <<
eom;
332 status() <<
"Removing unused functions" <<
eom;
342 if(criterion==
"assertion" || criterion==
"assertions")
344 else if(criterion==
"path" || criterion==
"paths")
346 else if(criterion==
"branch" || criterion==
"branches")
348 else if(criterion==
"location" || criterion==
"locations")
350 else if(criterion==
"decision" || criterion==
"decisions")
352 else if(criterion==
"condition" || criterion==
"conditions")
354 else if(criterion==
"mcdc")
356 else if(criterion==
"cover")
360 error() <<
"unknown coverage criterion" <<
eom;
364 status() <<
"Instrumenting coverage goals" <<
eom;
390 catch(
const std::string e)
401 catch(std::bad_alloc)
416 for(path_searcht::property_mapt::const_iterator
417 it=property_map.begin();
418 it!=property_map.end();
423 xmlt xml_result(
"result");
426 std::string status_string;
428 switch(it->second.status)
437 std::cout << xml_result <<
"\n";
441 status() <<
"[" << it->first <<
"] " 442 << it->second.description <<
": ";
443 switch(it->second.status)
454 it->second.is_failure())
464 for(path_searcht::property_mapt::const_iterator
465 it=property_map.begin();
466 it!=property_map.end();
468 if(it->second.is_failure())
471 status() <<
"** " << failed
472 <<
" of " << property_map.size() <<
" failed" 479 result() <<
"VERIFICATION SUCCESSFUL" <<
eom;
508 std::cout <<
'\n' <<
"Counterexample:" <<
'\n';
516 std::cout << xml << std::flush;
527 result() <<
"VERIFICATION FAILED" <<
eom;
555 std::cout <<
"(" << (
sizeof(
void *)*8) <<
"-bit version)";
557 std::cout <<
" * *\n";
560 "* * Daniel Kroening * *\n" 561 "* * University of Oxford * *\n" 562 "* * kroening@kroening.com * *\n" 566 " symex [-?] [-h] [--help] show help\n" 567 " symex file.c ... source file names\n" 569 "Analysis options:\n" 571 " --show-properties show the properties, but don't run analysis\n" 572 " --property id only check one specific property\n" 574 " --stop-on-fail stop analysis once a failed property is detected\n" 576 " --trace give a counterexample trace for failed properties\n" 578 "Frontend options:\n" 579 " -I path set include path (C/C++)\n" 580 " -D macro define preprocessor macro (C/C++)\n" 581 " --preprocess stop after preprocessing\n" 582 " --16, --32, --64 set width of int\n" 583 " --LP64, --ILP64, --LLP64,\n" 584 " --ILP32, --LP32 set width of int, long and pointers\n" 585 " --little-endian allow little-endian word-byte conversions\n" 586 " --big-endian allow big-endian word-byte conversions\n" 587 " --unsigned-char make \"char\" unsigned by default\n" 588 " --show-parse-tree show parse tree\n" 589 " --show-symbol-table show symbol table\n" 591 " --drop-unused-functions drop functions trivially unreachable from main function\n" 592 " --ppc-macos set MACOS/PPC architecture\n" 593 " --mm model set memory model (default: sc)\n" 594 " --arch set architecture (default: " 596 " --os set operating system (default: " 599 " --gcc use GCC as preprocessor\n" 601 " --no-arch don't set up an architecture\n" 602 " --no-library disable built-in abstract C library\n" 604 " --round-to-nearest IEEE floating point rounding mode (default)\n" 605 " --round-to-plus-inf IEEE floating point rounding mode\n" 606 " --round-to-minus-inf IEEE floating point rounding mode\n" 607 " --round-to-zero IEEE floating point rounding mode\n" 608 " --function name set main function name\n" 610 "Program instrumentation options:\n" 612 " --no-assertions ignore user assertions\n" 613 " --no-assumptions ignore user assumptions\n" 614 " --error-label label check that label is unreachable\n" 617 " --unwind nr unwind nr times\n" 618 " --depth nr limit search depth\n" 619 " --context-bound nr limit number of context switches\n" 620 " --branch-bound nr limit number of branches taken\n" 621 " --max-search-time s limit search to approximately s seconds\n" 624 " --version show version and exit\n" 625 " --xml-ui use XML-formatted output\n" 626 " --verbosity # verbosity level\n"
symbol_tablet symbol_table
const std::list< std::string > & get_values(const std::string &option) const
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
void report_cover(const path_searcht::property_mapt &)
const std::string & id2string(const irep_idt &d)
Remove function exceptional returns.
property_mapt property_map
Remove Instance-of Operators.
Remove Indirect Function Calls.
std::map< irep_idt, property_entryt > property_mapt
Remove Virtual Function (Method) Calls.
void remove_unused_functions(goto_functionst &functions, message_handlert &message_handler)
void goto_check(const namespacet &ns, const optionst &options, goto_functionst::goto_functiont &goto_function)
void set_branch_bound(int limit)
unsigned unsafe_string2unsigned(const std::string &str, int base)
languaget * new_ansi_c_language()
Remove the 'complex' data type by compilation into structs.
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler)
bool process_goto_program(const optionst &options)
virtual void help()
display command line help
std::string get_value(char option) const
ui_message_handlert ui_message_handler
void show_properties(const namespacet &ns, const irep_idt &identifier, ui_message_handlert::uit ui, const goto_programt &goto_program)
symbol_tablet symbol_table
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
static mstreamt & eom(mstreamt &m)
xmlt xml(const source_locationt &location)
void remove_exceptions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes throws/CATCH-POP/CATCH-PUSH
void output(std::ostream &out) const
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)
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 instrument_cover_goals(const symbol_tablet &symbol_table, goto_programt &goto_program, coverage_criteriont criterion)
void get_command_line_options(optionst &options)
void set_attribute(const std::string &attribute, unsigned value)
static mstreamt & endl(mstreamt &m)
Abstract interface to support a programming language.
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)
void set_time_limit(int limit)
languaget * new_cpp_language()
virtual void set_message_handler(message_handlert &_message_handler)
void convert(const goto_functionst::goto_functiont &function, xmlt &xml)
takes a goto_function and creates an according xml structure
void set_depth_limit(int limit)
void adjust_float_expressions(exprt &expr, const namespacet &ns)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
languaget * new_java_bytecode_language()
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void set_unwind_limit(int limit)
unsigned safe_string2unsigned(const std::string &str, int base)
static irep_idt this_operating_system()
message_handlert & get_message_handler()
Goto Programs with Functions.
#define HELP_SHOW_GOTO_FUNCTIONS
void set_context_bound(int limit)
void report_properties(const path_searcht::property_mapt &)
symex_parse_optionst(int argc, const char **argv)
Path-based Symbolic Execution.
void memory_info(std::ostream &out)
Remove the 'vector' data type by compilation into arrays.
void set_verbosity(unsigned _verbosity)
CFG made of Program Locations, built from goto_functionst.
virtual void usage_error()
void rewrite_union(exprt &expr, const namespacet &ns)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)
void register_language(language_factoryt factory)
Coverage Instrumentation.
virtual int doit()
invoke main modules
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)
int unsafe_string2int(const std::string &str, int base)
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()
void show_counterexample(const class goto_tracet &)
void build(const goto_functionst &goto_functions)