145 std::ofstream out(
"simulator.c");
148 throw std::string(
"failed to create file simulator.c");
150 dump_c(goto_functions,
true,
false, ns, out);
152 status() <<
"instrumentation complete; compile and execute simulator.c" 158 catch(
const std::string error_msg)
164 catch(
const char *error_msg)
170 catch(std::bad_alloc)
198 error() <<
"Please provide a program to verify" <<
eom;
206 status() <<
"Reading GOTO program from file" <<
eom;
224 error() <<
"The goto binary has no entry point; please complete linking" 233 error() <<
"Please give one source file only" <<
eom;
240 std::ifstream infile(
widen(filename));
242 std::ifstream infile(filename);
247 error() <<
"failed to open input file `" << filename <<
"'" <<
eom;
253 if(language==
nullptr)
255 error() <<
"failed to figure out type of file `" << filename <<
"'" 262 status() <<
"Parsing " << filename <<
eom;
264 if(language->
parse(infile, filename))
293 error() <<
"No entry point; please provide a main function" <<
eom;
297 status() <<
"Generating GOTO Program" <<
eom;
326 status() <<
"Generic Property Instrumentation" <<
eom;
360 void clobber_parse_optionst::report_properties(
363 for(
const auto &prop_pair : property_map)
365 if(
get_ui()==ui_message_handlert::XML_UI)
367 xmlt xml_result(
"result");
368 xml_result.set_attribute(
"claim",
id2string(prop_pair.first));
370 std::string status_string;
372 switch(prop_pair.second.status)
374 case path_searcht::PASS: status_string=
"OK";
break;
375 case path_searcht::FAIL: status_string=
"FAILURE";
break;
379 xml_result.set_attribute(
"status", status_string);
381 std::cout << xml_result <<
"\n";
385 status() <<
"[" << prop_pair.first <<
"] " 386 << prop_pair.second.description <<
": ";
387 switch(prop_pair.second.status)
389 case path_searcht::PASS:
status() <<
"OK";
break;
390 case path_searcht::FAIL:
status() <<
"FAILED";
break;
397 prop_pair.second.status==path_searcht::FAIL)
407 for(
const auto &prop_pair : property_map)
408 if(prop_pair.second.status==path_searcht::FAIL)
411 status() <<
"** " << failed
412 <<
" of " << property_map.size() <<
" failed" 420 result() <<
"VERIFICATION SUCCESSFUL" <<
eom;
449 std::cout <<
"\nCounterexample:\n";
457 std::cout <<
xml <<
'\n';
468 result() <<
"VERIFICATION FAILED" <<
eom;
496 std::cout <<
"(" << (
sizeof(
void *)*8) <<
"-bit version)";
498 std::cout <<
" * *\n";
501 "* * Daniel Kroening * *\n" 502 "* * University of Oxford * *\n" 503 "* * kroening@kroening.com * *\n" 507 " symex [-?] [-h] [--help] show help\n" 508 " symex file.c ... source file names\n" 510 "Frontend options:\n" 511 " -I path set include path (C/C++)\n" 512 " -D macro define preprocessor macro (C/C++)\n" 513 " --preprocess stop after preprocessing\n" 514 " --16, --32, --64 set width of int\n" 515 " --LP64, --ILP64, --LLP64,\n" 516 " --ILP32, --LP32 set width of int, long and pointers\n" 517 " --little-endian allow little-endian word-byte conversions\n" 518 " --big-endian allow big-endian word-byte conversions\n" 519 " --unsigned-char make \"char\" unsigned by default\n" 520 " --show-parse-tree show parse tree\n" 521 " --show-symbol-table show symbol table\n" 523 " --ppc-macos set MACOS/PPC architecture\n" 524 " --mm model set memory model (default: sc)\n" 525 " --arch set architecture (default: " 527 " --os set operating system (default: " 530 " --gcc use GCC as preprocessor\n" 532 " --no-arch don't set up an architecture\n" 533 " --no-library disable built-in abstract C library\n" 535 " --round-to-nearest IEEE floating point rounding mode (default)\n" 536 " --round-to-plus-inf IEEE floating point rounding mode\n" 537 " --round-to-minus-inf IEEE floating point rounding mode\n" 538 " --round-to-zero IEEE floating point rounding mode\n" 540 "Program instrumentation options:\n" 542 " --show-properties show the properties\n" 543 " --no-assertions ignore user assertions\n" 544 " --no-assumptions ignore user assumptions\n" 545 " --error-label label check that label is unreachable\n" 548 " --function name set main function name\n" 549 " --property nr only check one specific property\n" 550 " --depth nr limit search depth\n" 551 " --context-bound nr limit number of context switches\n" 552 " --unwind nr unwind nr times\n" 555 " --version show version and exit\n" 556 " --xml-ui use XML-formatted output\n" symbol_tablet symbol_table
const std::list< std::string > & get_values(const std::string &option) const
bool set_properties(goto_functionst &goto_functions)
void show_counterexample(const class goto_tracet &)
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
const std::string & id2string(const irep_idt &d)
ui_message_handlert ui_message_handler
std::wstring widen(const char *s)
std::map< irep_idt, property_entryt > property_mapt
void goto_check(const namespacet &ns, const optionst &options, goto_functionst::goto_functiont &goto_function)
void make_assertions_false(goto_modelt &goto_model)
languaget * new_ansi_c_language()
bool is_goto_binary(const std::string &filename)
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler)
Dump C from Goto Program.
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)
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 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()
virtual int doit()
invoke main modules
bool set(const cmdlinet &cmdline)
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
virtual bool isset(char option) const
virtual void help()
display command line help
static irep_idt entry_point()
static mstreamt & endl(mstreamt &m)
Abstract interface to support a programming language.
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
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void set_from_symbol_table(const symbol_tablet &)
bool get_goto_program(const optionst &options, goto_functionst &goto_functions)
bool process_goto_program(const optionst &options, goto_functionst &goto_functions)
virtual void show_parse(std::ostream &out)=0
virtual void clear_parse()
static irep_idt this_operating_system()
message_handlert & get_message_handler()
Goto Programs with Functions.
#define HELP_SHOW_GOTO_FUNCTIONS
languaget * get_language_from_filename(const std::string &filename)
clobber_parse_optionst(int argc, const char **argv)
void memory_info(std::ostream &out)
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const namespacet &ns, std::ostream &out)
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)
void show_goto_functions(const namespacet &ns, ui_message_handlert::uit ui, const goto_functionst &goto_functions)
virtual bool parse(std::istream &instream, const std::string &path)=0
void get_command_line_options(optionst &options)
int unsafe_string2int(const std::string &str, int base)
void label_properties(goto_modelt &goto_model)
static irep_idt this_architecture()