143 if(unwindset && unwindset_file)
144 throw "only one of --unwindset and --unwindset-file supported at a " 147 if(unwind || unwindset || unwindset_file)
164 std::ifstream
file(fn);
167 throw "cannot open file "+fn;
169 std::stringstream buffer;
170 buffer <<
file.rdbuf();
177 bool unwinding_assertions=
cmdline.
isset(
"unwinding-assertions");
179 bool continue_as_loops=
cmdline.
isset(
"continue-as-loops");
181 if(unwinding_assertions+partial_loops+continue_as_loops>1)
182 throw "more than one of --unwinding-assertions,--partial-loops," 183 "--continue-as-loops selected";
188 if(unwinding_assertions)
192 else if(partial_loops)
196 else if(continue_as_loops)
210 bool have_file=!filename.empty() && filename!=
"-";
217 std::ofstream of(
widen(filename));
219 std::ofstream of(filename);
222 throw "failed to open file "+filename;
229 std::cout <<
result <<
'\n';
243 std::cout <<
"////\n";
244 std::cout <<
"//// Function: " << f_it->first <<
'\n';
245 std::cout <<
"////\n\n";
252 std::cout <<
"Is threaded: " << (is_threaded(i_it)?
"True":
"False")
307 std::cout <<
">>>>\n";
308 std::cout <<
">>>> " << it->first <<
'\n';
309 std::cout <<
">>>>\n";
310 local_bitvector_analysis.
output(std::cout, it->second, ns);
385 custom_bitvector_analysis.
check(
407 points_to.
output(std::cout);
542 status() <<
"Starting interpreter" <<
eom;
585 for(
auto const &ins : pair.second.body.instructions)
587 if(ins.code.is_not_nil())
589 if(ins.guard.is_not_nil())
590 status() <<
"[guard] " << ins.guard.pretty() <<
eom;
663 call_graph.
output(std::cout);
699 status() <<
"Performing full inlining" <<
eom;
710 status() <<
"Horn-clause encoding" <<
eom;
723 error() <<
"Failed to open output file " 740 status() <<
"Removing unused functions" <<
eom;
773 catch(
const std::string e)
784 catch(std::bad_alloc)
800 status() <<
"Function Pointer Removal" <<
eom;
806 status() <<
"Virtual function removal" <<
eom;
808 status() <<
"Catch and throw removal" <<
eom;
810 status() <<
"Java instanceof removal" <<
eom;
826 status() <<
"Removing const function pointers only" <<
eom;
887 options.
set_option(
"assert-to-assume",
false);
918 status() <<
"Adding gotos to skip loops" <<
eom;
934 status() <<
"Adding up to " << max_argc
935 <<
" command line arguments" <<
eom;
979 status() <<
"Performing full inlining" <<
eom;
988 status() <<
"Propagating Constants" <<
eom;
1018 status() <<
"Applying Code Contracts" <<
eom;
1027 else if(
cmdline.
isset(
"remove-const-function-pointers"))
1035 assert(!
function.empty());
1041 status() <<
"Inlining calls of function `" <<
function <<
"'" <<
eom;
1056 bool have_file=!filename.empty() && filename!=
"-";
1070 std::ofstream of(
widen(filename));
1072 std::ofstream of(filename);
1075 throw "failed to open file "+filename;
1082 std::cout <<
result <<
'\n';
1114 status() <<
"Performing full inlining" <<
eom;
1122 status() <<
"Propagating Constants" <<
eom;
1135 status() <<
"Adding checks for uninitialized local variables" <<
eom;
1142 status() <<
"Adding check for maximum call stack size" <<
eom;
1153 status() <<
"Adding nondeterministic initialization of static/global " 1160 status() <<
"Slicing away initializations of unused global variables" 1170 status() <<
"String Abstraction" <<
eom;
1199 value_set_analysis);
1204 status() <<
"Adding Race Checks" <<
eom;
1238 const unsigned unwind_loops=
1241 const unsigned max_var=
1244 const unsigned max_po_trans=
1250 status() <<
"Adding weak memory (TSO) Instrumentation" <<
eom;
1255 status() <<
"Adding weak memory (PSO) Instrumentation" <<
eom;
1260 status() <<
"Adding weak memory (RMO) Instrumentation" <<
eom;
1263 else if(mm==
"power")
1265 status() <<
"Adding weak memory (Power) Instrumentation" <<
eom;
1270 error() <<
"Unknown weak memory model `" << mm <<
"'" <<
eom;
1307 status() <<
"Instrumenting interrupt handler" <<
eom;
1318 status() <<
"Instrumenting memory-mapped I/O" <<
eom;
1327 status() <<
"Sequentializing concurrency" <<
eom;
1352 if(step_case && base_case)
1353 throw "please specify only one of --step-case and --base-case";
1354 else if(!step_case && !base_case)
1355 throw "please specify one of --step-case and --base-case";
1360 throw "please give k>=1";
1362 status() <<
"Instrumenting k-induction for k=" << k <<
", " 1363 << (base_case?
"base case":
"step case") <<
eom;
1370 status() <<
"Function enter instrumentation" <<
eom;
1379 status() <<
"Function exit instrumentation" <<
eom;
1388 status() <<
"Branch instrumentation" <<
eom;
1410 status() <<
"Making volatile variables non-deterministic" <<
eom;
1417 status() <<
"Performing a reachability slice" <<
eom;
1430 status() <<
"Performing a full slice" <<
eom;
1446 "* * Goto-Instrument " CBMC_VERSION " - Copyright (C) 2008-2013 * *\n" 1447 "* * Daniel Kroening * *\n" 1448 "* * kroening@kroening.com * *\n" 1452 " goto-instrument [-?] [-h] [--help] show help\n" 1453 " goto-instrument in out perform instrumentation\n" 1456 " --document-properties-html generate HTML property documentation\n" 1457 " --document-properties-latex generate Latex property documentation\n" 1458 " --dump-c generate C source\n" 1459 " --dump-cpp generate C++ source\n" 1460 " --dot generate CFG graph in DOT format\n" 1461 " --interpreter do concrete execution\n" 1462 " --count-eloc count effective lines of code\n" 1463 " --list-eloc list full path names of lines containing code\n" 1466 " --show-loops show the loops in the program\n" 1467 " --show-properties show the properties\n" 1468 " --show-symbol-table show symbol table\n" 1469 " --list-symbols list symbols with type information\n" 1471 " --print-internal-representation\n" 1472 " show verbose internal representation of the program\n" 1473 " --list-undefined-functions list functions without body\n" 1474 " --show-struct-alignment show struct members that might be concurrently accessed\n" 1475 " --show-natural-loops show natural loop heads\n" 1477 " --list-calls-args list all function calls with their arguments\n" 1480 " --no-assertions ignore user assertions\n" 1482 " --uninitialized-check add checks for uninitialized locals (experimental)\n" 1483 " --error-label label check that label is unreachable\n" 1484 " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" 1485 " --race-check add floating-point data race checks\n" 1487 "Semantic transformations:\n" 1488 " --nondet-volatile makes reads from volatile variables non-deterministic\n" 1489 " --unwind <n> unwinds the loops <n> times\n" 1490 " --unwindset L:B,... unwind loop L with a bound of B\n" 1491 " --unwindset-file <file> read unwindset from file\n" 1492 " --partial-loops permit paths with partial loops\n" 1493 " --unwinding-assertions generate unwinding assertions\n" 1494 " --continue-as-loops add loop for remaining iterations after unwound part\n" 1495 " --isr <function> instruments an interrupt service routine\n" 1496 " --mmio instruments memory-mapped I/O\n" 1497 " --nondet-static add nondeterministic initialization of variables with static lifetime\n" 1498 " --check-invariant function instruments invariant checking function\n" 1499 " --remove-pointers converts pointer arithmetic to base+offset expressions\n" 1501 " --undefined-function-is-assume-false\n" 1502 " convert each call to an undefined function to assume(false)\n" 1504 "Loop transformations:\n" 1505 " --k-induction <k> check loops with k-induction\n" 1506 " --step-case k-induction: do step-case\n" 1507 " --base-case k-induction: do base-case\n" 1508 " --havoc-loops over-approximate all loops\n" 1509 " --accelerate add loop accelerators\n" 1510 " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" 1512 "Memory model instrumentations:\n" 1513 " --mm <tso,pso,rmo,power> instruments a weak memory model\n" 1514 " --scc detects critical cycles per SCC (one thread per SCC)\n" 1515 " --one-event-per-cycle only instruments one event per cycle\n" 1516 " --minimum-interference instruments an optimal number of events\n" 1517 " --my-events only instruments events whose ids appear in inst.evt\n" 1518 " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" 1519 " --no-dependencies no dependency analysis\n" 1521 " --no-po-rendering no representation of the threads in the dot\n" 1522 " --render-cluster-file clusterises the dot by files\n" 1523 " --render-cluster-function clusterises the dot by functions\n" 1526 " --reachability-slice slice away instructions that can't reach assertions\n" 1527 " --full-slice slice away instructions that don't affect assertions\n" 1528 " --property id slice with respect to specific property only\n" 1529 " --slice-global-inits slice away initializations of unused global variables\n" 1531 "Further transformations:\n" 1532 " --constant-propagator propagate constants and simplify expressions\n" 1533 " --inline perform full inlining\n" 1534 " --partial-inline perform partial inlining\n" 1535 " --function-inline <function> transitively inline all calls <function> makes\n" 1536 " --no-caching disable caching of intermediate results during transitive function inlining\n" 1537 " --log <file> log in json format which code segments were inlined, use with --function-inline\n" 1538 " --remove-function-pointers replace function pointers by case statement over function calls\n" 1540 " --add-library add models of C library functions\n" 1541 " --model-argc-argv <n> model up to <n> command line arguments\n" 1543 " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n" 1546 " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" 1547 " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" 1548 " --version show version and exit\n" 1549 " --xml-ui use XML-formatted output\n" 1550 " --json-ui use JSON-formatted output\n"
void do_indirect_call_and_rtti_removal(bool force=false)
symbol_tablet symbol_table
irep_idt name
The unique identifier.
const std::list< std::string > & get_values(const std::string &option) const
Detection for Uninitialized Local Variables.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
struct configt::ansi_ct ansi_c
jsont output_log_json() const
Field-insensitive, location-sensitive bitvector analysis.
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Function Entering and Exiting.
Over-approximate Concurrency for Threaded Goto Programs.
Skip over selected loops by adding gotos.
Remove function exceptional returns.
Remove initializations of unused global variables.
Initialize command line arguments.
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
Remove Instance-of Operators.
void remove_asm(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes assembler
void show_uninitialized(const class symbol_tablet &symbol_table, const goto_functionst &goto_functions, std::ostream &out)
Remove Indirect Function Calls.
std::wstring widen(const char *s)
instrumentation_strategyt
Remove Virtual Function (Method) Calls.
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
void remove_pointers(goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
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)
Field-sensitive, location-insensitive points-to analysis.
unsigned unsafe_string2unsigned(const std::string &str, int base)
void parse_unwindset(const std::string &us, unwind_sett &unwind_set)
Remove function definition.
void print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
std::list< std::string > defines
void undefined_function_abort_path(goto_functionst &goto_functions)
void restore_returns(symbol_tablet &symbol_table, goto_functionst &goto_functions)
restores return statements
void list_undefined_functions(const goto_functionst &goto_functions, const namespacet &ns, std::ostream &os)
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler)
Dump C from Goto Program.
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)
void code_contracts(symbol_tablet &symbol_table, goto_functionst &goto_functions)
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Inline all function calls made from a particular function.
void check_call_sequence(const goto_functionst &goto_functions)
Race Detection for Threaded Goto Programs.
Field-insensitive, location-sensitive bitvector analysis.
virtual void show_symbol_table(bool brief=false)
Memory-mapped I/O Instrumentation for Goto Programs.
void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program)
Interpreter for GOTO Programs.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void function_exit(symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &id)
static mstreamt & eom(mstreamt &m)
Weak Memory Instrumentation for Threaded Goto Programs.
virtual int doit()
invoke main modules
Remove 'asm' statements by compiling into suitable standard code.
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
void remove_exceptions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes throws/CATCH-POP/CATCH-PUSH
void concurrency(value_setst &value_sets, class symbol_tablet &symbol_table, goto_functionst &goto_functions)
Documentation of Properties.
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 function_pointer_removal_done
void add_uninitialized_locals_assertions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
bool set(const cmdlinet &cmdline)
void show_natural_loops(const goto_functionst &goto_functions)
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
virtual bool isset(char option) const
void remove_functions(symbol_tablet &symbol_table, goto_functionst &goto_functions, const std::list< std::string > &names, message_handlert &message_handler)
Remove the body of all functions listed in "names" such that an analysis will treat it as a side-effe...
void remove_instanceof(symbol_tablet &symbol_table, goto_functionst &goto_functions)
See function above.
bool partial_inlining_done
void check(const namespacet &, const goto_functionst &, bool xml, std::ostream &)
void output_xml(std::ostream &out) const
Nondeterministic initialization of certain global scope variables.
void output_dot(std::ostream &out) const
Dump Goto-Program as DOT Graph.
void print_path_lengths(const goto_functionst &goto_functions)
void k_induction(goto_functionst &goto_functions, bool base_case, bool step_case, unsigned k)
void horn_encoding(const goto_functionst &, const namespacet &, std::ostream &out)
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)
Field-insensitive, location-sensitive, over-approximative escape analysis.
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const namespacet &ns, std::ostream &out)
void count_eloc(const goto_functionst &goto_functions)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void do_partial_inlining()
Count effective lines of code.
void instrument_goto_program()
void instrument(goto_functionst &, const namespacet &)
function_mapt function_map
jsont goto_function_inline_and_log(goto_functionst &goto_functions, const irep_idt function, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void output_dot(std::ostream &out) const
void weak_memory(memory_modelt model, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned input_max_var, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, message_handlert &message_handler, bool ignore_arrays)
void output(std::ostream &out) const
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
void show_call_sequences(const irep_idt &function, const goto_programt &goto_program, const goto_programt::const_targett start)
void set_from_symbol_table(const symbol_tablet &)
void reachability_slicer(goto_functionst &goto_functions)
Interrupt Instrumentation for Goto Programs.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void branch(symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &id)
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
Verify and use annotated invariants and pre/post-conditions.
static void list_calls_and_arguments(const namespacet &ns, const irep_idt &function, const goto_programt &goto_program)
void document_properties_latex(const goto_functionst &goto_functions, std::ostream &out)
unsigned safe_string2unsigned(const std::string &str, int base)
void output(std::ostream &out) const
typet type
Type of symbol.
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
message_handlert & get_message_handler()
Goto Programs with Functions.
void list_eloc(const goto_functionst &goto_functions)
#define HELP_SHOW_GOTO_FUNCTIONS
virtual void help()
display command line help
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
void havoc_loops(goto_functionst &goto_functions)
Handling of functions without body.
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const namespacet &ns, std::ostream &out)
void interpreter(const symbol_tablet &symbol_table, const goto_functionst &goto_functions)
void remove_returns(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
void accelerate_functions(goto_functionst &functions, symbol_tablet &symbol_table, bool use_z3)
void dot(const goto_functionst &src, const namespacet &ns, std::ostream &out)
void interrupt(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program, const symbol_exprt &interrupt_handler, const rw_set_baset &isr_rw_set)
void race_check(value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program, w_guardst &w_guards)
void set_verbosity(unsigned _verbosity)
void function_enter(symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &id)
std::map< irep_idt, std::map< unsigned, int > > unwind_sett
Expression to hold a symbol (variable)
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
Compute natural loops in a goto_function.
void set_option(const std::string &option, const bool value)
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
Memory-mapped I/O Instrumentation for Goto Programs.
void add_failed_symbols(symbol_tablet &symbol_table)
Encoding for Threaded Goto Programs.
bool write_goto_binary(std::ostream &out, const symbol_tablet &lsymbol_table, const goto_functionst &functions, int version)
Writes a goto program to disc.
goto_functionst goto_functions
void show_goto_functions(const namespacet &ns, ui_message_handlert::uit ui, const goto_functionst &goto_functions)
#define forall_goto_functions(it, functions)
Field-insensitive, location-sensitive, over-approximative escape analysis.
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
void document_properties_html(const goto_functionst &goto_functions, std::ostream &out)
#define forall_goto_program_instructions(it, program)
void slice_global_inits(const namespacet &ns, goto_functionst &goto_functions)
Add parameter assignments.
void label_properties(goto_modelt &goto_model)
virtual void register_languages()
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
void interval_analysis(const namespacet &ns, goto_functionst &goto_functions)
bool model_argc_argv(symbol_tablet &symbol_table, goto_functionst &goto_functions, unsigned max_argc, message_handlert &message_handler)
void show_value_sets(ui_message_handlert::uit ui, const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis)
void thread_exit_instrumentation(goto_programt &goto_program)
Race Detection for Threaded Goto Programs.
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const int i_depth, const exprt &max_depth)