41 ui_message_handler(cmdline,
"CLOBBER " CBMC_VERSION)
84 std::cout << CBMC_VERSION <<
'\n';
142 std::ofstream out(
"simulator.c");
145 throw std::string(
"failed to create file simulator.c");
147 dump_c(goto_model.goto_functions,
true,
false,
false, ns, out);
149 status() <<
"instrumentation complete; compile and execute simulator.c" 155 catch(
const std::string &error_msg)
161 catch(
const char *error_msg)
167 catch(
const std::bad_alloc &)
199 status() <<
"Generic Property Instrumentation" <<
eom;
219 void clobber_parse_optionst::report_properties(
220 const path_searcht::property_mapt &property_map)
222 for(
const auto &prop_pair : property_map)
224 if(
get_ui()==ui_message_handlert::XML_UI)
226 xmlt xml_result(
"result");
227 xml_result.set_attribute(
"claim",
id2string(prop_pair.first));
229 std::string status_string;
231 switch(prop_pair.second.status)
233 case path_searcht::PASS: status_string=
"OK";
break;
234 case path_searcht::FAIL: status_string=
"FAILURE";
break;
235 case path_searcht::NOT_REACHED: status_string=
"OK";
break;
238 xml_result.set_attribute(
"status", status_string);
240 std::cout << xml_result <<
"\n";
244 status() <<
"[" << prop_pair.first <<
"] " 245 << prop_pair.second.description <<
": ";
246 switch(prop_pair.second.status)
248 case path_searcht::PASS:
status() <<
"OK";
break;
249 case path_searcht::FAIL:
status() <<
"FAILED";
break;
250 case path_searcht::NOT_REACHED:
status() <<
"OK";
break;
256 prop_pair.second.status==path_searcht::FAIL)
266 for(
const auto &prop_pair : property_map)
267 if(prop_pair.second.status==path_searcht::FAIL)
270 status() <<
"** " << failed
271 <<
" of " << property_map.size() <<
" failed" 279 result() <<
"VERIFICATION SUCCESSFUL" <<
eom;
308 std::cout <<
"\nCounterexample:\n";
316 std::cout <<
xml <<
'\n';
327 result() <<
"VERIFICATION FAILED" <<
eom;
352 std::cout <<
'\n' <<
banner_string(
"CLOBBER", CBMC_VERSION) <<
'\n' 354 "* * Copyright (C) 2014 * *\n" 355 "* * Daniel Kroening * *\n" 356 "* * University of Oxford * *\n" 357 "* * kroening@kroening.com * *\n" 361 " symex [-?] [-h] [--help] show help\n" 362 " symex file.c ... source file names\n" 364 "Frontend options:\n" 365 " -I path set include path (C/C++)\n" 366 " -D macro define preprocessor macro (C/C++)\n" 367 " --preprocess stop after preprocessing\n" 368 " --16, --32, --64 set width of int\n" 369 " --LP64, --ILP64, --LLP64,\n" 370 " --ILP32, --LP32 set width of int, long and pointers\n" 371 " --little-endian allow little-endian word-byte conversions\n" 372 " --big-endian allow big-endian word-byte conversions\n" 373 " --unsigned-char make \"char\" unsigned by default\n" 374 " --show-parse-tree show parse tree\n" 375 " --show-symbol-table show loaded symbol table\n" 377 " --ppc-macos set MACOS/PPC architecture\n" 378 " --mm model set memory model (default: sc)\n" 379 " --arch set architecture (default: " 381 " --os set operating system (default: " 384 " --gcc use GCC as preprocessor\n" 386 " --no-arch don't set up an architecture\n" 387 " --no-library disable built-in abstract C library\n" 389 " --round-to-nearest IEEE floating point rounding mode (default)\n" 390 " --round-to-plus-inf IEEE floating point rounding mode\n" 391 " --round-to-minus-inf IEEE floating point rounding mode\n" 392 " --round-to-zero IEEE floating point rounding mode\n" 394 "Program instrumentation options:\n" 396 " --show-properties show the properties\n" 397 " --no-assertions ignore user assertions\n" 398 " --no-assumptions ignore user assumptions\n" 399 " --error-label label check that label is unreachable\n" 402 " --function name set main function name\n" 403 " --property nr only check one specific property\n" 404 " --depth nr limit search depth\n" 405 " --context-bound nr limit number of context switches\n" 406 " --unwind nr unwind nr times\n" 409 " --version show version and exit\n" 410 " --xml-ui use XML-formatted output\n" symbol_tablet symbol_table
const std::list< std::string > & get_values(const std::string &option) const
void show_counterexample(const class goto_tracet &)
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
std::unique_ptr< languaget > new_cpp_language()
const std::string & id2string(const irep_idt &d)
ui_message_handlert ui_message_handler
void compute_loop_numbers()
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...
void make_assertions_false(goto_modelt &goto_model)
Dump C from Goto Program.
std::string get_value(char option) const
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
static mstreamt & eom(mstreamt &m)
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
xmlt xml(const source_locationt &location)
bool set_properties(goto_functionst &)
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.
virtual int doit()
invoke main modules
bool set(const cmdlinet &cmdline)
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
virtual bool isset(char option) const
Initialize a Goto Program.
virtual void help()
display command line help
bool process_goto_program(const optionst &options, goto_modelt &)
static mstreamt & endl(mstreamt &m)
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
std::string banner_string(const std::string &front_end, const std::string &version)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
void get_command_line_options(optionst &)
static irep_idt this_operating_system()
message_handlert & get_message_handler()
mstreamt & result() const
mstreamt & status() const
#define HELP_SHOW_GOTO_FUNCTIONS
clobber_parse_optionst(int argc, const char **argv)
goto_modelt initialize_goto_model(const cmdlinet &cmdline, message_handlert &message_handler)
void memory_info(std::ostream &out)
std::unique_ptr< languaget > new_ansi_c_language()
virtual void usage_error()
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
void set_option(const std::string &option, const bool value)
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.
static irep_idt this_architecture()
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)