129 const bool validate_only =
cmdline.
isset(
"validate-goto-binary");
131 if(validate_only ||
cmdline.
isset(
"validate-goto-model"))
152 bool unwindset_file_given=
cmdline.
isset(
"unwindset-file");
154 if(unwindset_given && unwindset_file_given)
155 throw "only one of --unwindset and --unwindset-file supported at a " 158 if(unwind_given || unwindset_given || unwindset_file_given)
165 if(unwindset_file_given)
171 bool unwinding_assertions=
cmdline.
isset(
"unwinding-assertions");
173 bool continue_as_loops=
cmdline.
isset(
"continue-as-loops");
175 if(unwinding_assertions+partial_loops+continue_as_loops>1)
176 throw "more than one of --unwinding-assertions,--partial-loops," 177 "--continue-as-loops selected";
182 if(unwinding_assertions)
186 else if(partial_loops)
190 else if(continue_as_loops)
196 goto_unwind(
goto_model, unwindset, unwind_strategy);
201 bool have_file=!filename.empty() && filename!=
"-";
208 std::ofstream of(
widen(filename));
210 std::ofstream of(filename);
213 throw "failed to open file "+filename;
220 std::cout <<
result <<
'\n';
238 std::cout <<
"////\n";
239 std::cout <<
"//// Function: " << f_it->first <<
'\n';
240 std::cout <<
"////\n\n";
247 std::cout <<
"Is threaded: " << (is_threaded(i_it)?
"True":
"False")
299 std::cout <<
">>>>\n";
300 std::cout <<
">>>> " << it->first <<
'\n';
301 std::cout <<
">>>>\n";
302 local_bitvector_analysis.
output(std::cout, it->second, ns);
320 local_safe_pointers(it->second.body);
321 std::cout <<
">>>>\n";
322 std::cout <<
">>>> " << it->first <<
'\n';
323 std::cout <<
">>>>\n";
325 local_safe_pointers.
output(std::cout, it->second.body);
329 std::cout, it->second.body);
398 custom_bitvector_analysis.
check(
418 points_to.
output(std::cout);
553 status() <<
"Starting interpreter" <<
eom;
595 for(
auto const &ins : pair.second.body.instructions)
597 if(ins.code.is_not_nil())
599 if(ins.guard.is_not_nil())
600 status() <<
"[guard] " << ins.guard.pretty() <<
eom;
690 call_graph.
output(std::cout);
706 call_graph.
output(std::cout);
754 status() <<
"Performing full inlining" <<
eom;
757 status() <<
"Removing calls to functions without a body" <<
eom;
769 status() <<
"Horn-clause encoding" <<
eom;
782 error() <<
"Failed to open output file " 799 status() <<
"Removing unused functions" <<
eom;
831 catch(
const std::string &e)
839 error() <<
"Numeric exception : " << e <<
eom;
843 catch(
const std::bad_alloc &)
859 status() <<
"Function Pointer Removal" <<
eom;
864 status() <<
"Virtual function removal" <<
eom;
866 status() <<
"Cleaning inline assembler statements" <<
eom;
882 status() <<
"Removing const function pointers only" <<
eom;
945 options.
set_option(
"assert-to-assume",
false);
976 status() <<
"Adding gotos to skip loops" <<
eom;
992 status() <<
"Adding up to " << max_argc
993 <<
" command line arguments" <<
eom;
1042 status() <<
"Performing full inlining" <<
eom;
1049 status() <<
"Propagating Constants" <<
eom;
1078 status() <<
"Applying Code Contracts" <<
eom;
1087 else if(
cmdline.
isset(
"remove-const-function-pointers"))
1109 status() <<
"Inlining calls of function `" <<
function <<
"'" <<
eom;
1123 bool have_file=!filename.empty() && filename!=
"-";
1136 std::ofstream of(
widen(filename));
1138 std::ofstream of(filename);
1141 throw "failed to open file "+filename;
1148 std::cout <<
result <<
'\n';
1169 status() <<
"Removing calls to functions without a body" <<
eom;
1182 status() <<
"Propagating Constants" <<
eom;
1194 status() <<
"Adding checks for uninitialized local variables" <<
eom;
1201 status() <<
"Adding check for maximum call stack size" <<
eom;
1211 status() <<
"Adding nondeterministic initialization of static/global " 1218 status() <<
"Slicing away initializations of unused global variables" 1228 status() <<
"String Abstraction" <<
eom;
1257 status() <<
"Adding Race Checks" <<
eom;
1282 const unsigned max_var=
1285 const unsigned max_po_trans=
1291 status() <<
"Adding weak memory (TSO) Instrumentation" <<
eom;
1296 status() <<
"Adding weak memory (PSO) Instrumentation" <<
eom;
1301 status() <<
"Adding weak memory (RMO) Instrumentation" <<
eom;
1304 else if(mm==
"power")
1306 status() <<
"Adding weak memory (Power) Instrumentation" <<
eom;
1311 error() <<
"Unknown weak memory model `" << mm <<
"'" <<
eom;
1346 status() <<
"Instrumenting interrupt handler" <<
eom;
1356 status() <<
"Instrumenting memory-mapped I/O" <<
eom;
1362 status() <<
"Sequentializing concurrency" <<
eom;
1384 if(step_case && base_case)
1385 throw "please specify only one of --step-case and --base-case";
1386 else if(!step_case && !base_case)
1387 throw "please specify one of --step-case and --base-case";
1392 throw "please give k>=1";
1394 status() <<
"Instrumenting k-induction for k=" << k <<
", " 1395 << (base_case?
"base case":
"step case") <<
eom;
1402 status() <<
"Function enter instrumentation" <<
eom;
1410 status() <<
"Function exit instrumentation" <<
eom;
1418 status() <<
"Branch instrumentation" <<
eom;
1439 status() <<
"Making volatile variables non-deterministic" <<
eom;
1448 status() <<
"Performing a reachability slice" <<
eom;
1459 status() <<
"Performing a function pointer reachability slice" <<
eom;
1470 status() <<
"Performing a full slice" <<
eom;
1480 status() <<
"Performing call splicing" <<
eom;
1498 *generate_implementation,
1508 status() <<
"Slicing away initializations of unused global variables" 1512 status() <<
"Performing an aggressive slice" <<
eom;
1519 if(
cmdline.
isset(
"aggressive-slice-preserve-function"))
1527 if(
cmdline.
isset(
"aggressive-slice-preserve-functions-containing"))
1532 cmdline.
isset(
"aggressive-slice-preserve-all-direct-paths");
1534 aggressive_slicer.
doit();
1536 status() <<
"Performing a reachability slice" <<
eom;
1553 "* * Copyright (C) 2008-2013 * *\n" 1554 "* * Daniel Kroening * *\n" 1555 "* * kroening@kroening.com * *\n" 1559 " goto-instrument [-?] [-h] [--help] show help\n" 1560 " goto-instrument in out perform instrumentation\n" 1563 " --document-properties-html generate HTML property documentation\n" 1564 " --document-properties-latex generate Latex property documentation\n" 1565 " --dump-c generate C source\n" 1566 " --dump-cpp generate C++ source\n" 1567 " --dot generate CFG graph in DOT format\n" 1568 " --interpreter do concrete execution\n" 1571 " --show-loops show the loops in the program\n" 1573 " --show-symbol-table show loaded symbol table\n" 1574 " --list-symbols list symbols with type information\n" 1577 " --drop-unused-functions drop functions trivially unreachable from main function\n" 1578 " --print-internal-representation\n" 1579 " show verbose internal representation of the program\n" 1580 " --list-undefined-functions list functions without body\n" 1581 " --show-struct-alignment show struct members that might be concurrently accessed\n" 1582 " --show-natural-loops show natural loop heads\n" 1584 " --list-calls-args list all function calls with their arguments\n" 1585 " --call-graph show graph of function calls\n" 1587 " --reachable-call-graph show graph of function calls potentially reachable from main function\n" 1590 " --show-threaded show instructions that may be executed by more than one thread\n" 1591 " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n" 1592 " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n" 1593 " *and* used as a dereference operand\n" 1596 " --validate-goto-binary check the well-formedness of the passed in goto\n" 1597 " binary and then exit\n" 1600 " --no-assertions ignore user assertions\n" 1602 " --uninitialized-check add checks for uninitialized locals (experimental)\n" 1603 " --error-label label check that label is unreachable\n" 1604 " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" 1605 " --race-check add floating-point data race checks\n" 1607 "Semantic transformations:\n" 1608 " --nondet-volatile makes reads from volatile variables non-deterministic\n" 1609 " --unwind <n> unwinds the loops <n> times\n" 1610 " --unwindset L:B,... unwind loop L with a bound of B\n" 1611 " --unwindset-file <file> read unwindset from file\n" 1612 " --partial-loops permit paths with partial loops\n" 1613 " --unwinding-assertions generate unwinding assertions\n" 1614 " --continue-as-loops add loop for remaining iterations after unwound part\n" 1615 " --isr <function> instruments an interrupt service routine\n" 1616 " --mmio instruments memory-mapped I/O\n" 1617 " --nondet-static add nondeterministic initialization of variables with static lifetime\n" 1618 " --check-invariant function instruments invariant checking function\n" 1619 " --remove-pointers converts pointer arithmetic to base+offset expressions\n" 1620 " --splice-call caller,callee prepends a call to callee in the body of caller\n" 1621 " --undefined-function-is-assume-false\n" 1623 " convert each call to an undefined function to assume(false)\n" 1626 "Loop transformations:\n" 1627 " --k-induction <k> check loops with k-induction\n" 1628 " --step-case k-induction: do step-case\n" 1629 " --base-case k-induction: do base-case\n" 1630 " --havoc-loops over-approximate all loops\n" 1631 " --accelerate add loop accelerators\n" 1632 " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" 1634 "Memory model instrumentations:\n" 1635 " --mm <tso,pso,rmo,power> instruments a weak memory model\n" 1636 " --scc detects critical cycles per SCC (one thread per SCC)\n" 1637 " --one-event-per-cycle only instruments one event per cycle\n" 1638 " --minimum-interference instruments an optimal number of events\n" 1639 " --my-events only instruments events whose ids appear in inst.evt\n" 1640 " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" 1641 " --no-dependencies no dependency analysis\n" 1643 " --no-po-rendering no representation of the threads in the dot\n" 1644 " --render-cluster-file clusterises the dot by files\n" 1645 " --render-cluster-function clusterises the dot by functions\n" 1649 " --full-slice slice away instructions that don't affect assertions\n" 1650 " --property id slice with respect to specific property only\n" 1651 " --slice-global-inits slice away initializations of unused global variables\n" 1652 " --aggressive-slice remove bodies of any functions not on the shortest path between\n" 1653 " the start function and the function containing the property(s)\n" 1654 " --aggressive-slice-call-depth <n>\n" 1655 " used with aggressive-slice, preserves all functions within <n> function calls\n" 1656 " of the functions on the shortest path\n" 1657 " --aggressive-slice-preserve-function <f>\n" 1658 " force the aggressive slicer to preserve function <f>\n" 1659 " --aggressive-slice-preserve-function containing <f>\n" 1660 " force the aggressive slicer to preserve all functions with names containing <f>\n" 1661 "--aggressive-slice-preserve-all-direct-paths \n" 1662 " force aggressive slicer to preserve all direct paths\n" 1664 "Further transformations:\n" 1665 " --constant-propagator propagate constants and simplify expressions\n" 1666 " --inline perform full inlining\n" 1667 " --partial-inline perform partial inlining\n" 1668 " --function-inline <function> transitively inline all calls <function> makes\n" 1669 " --no-caching disable caching of intermediate results during transitive function inlining\n" 1670 " --log <file> log in json format which code segments were inlined, use with --function-inline\n" 1671 " --remove-function-pointers replace function pointers by case statement over function calls\n" 1674 " --add-library add models of C library functions\n" 1675 " --model-argc-argv <n> model up to <n> command line arguments\n" 1677 " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n" 1681 " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" 1682 " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" 1683 " --harness with --dump-c/--dump-cpp: include input generator in output\n" 1684 " --version show version and exit\n" 1686 " --xml-ui use XML-formatted output\n" 1687 " --json-ui use JSON-formatted output\n"
void do_indirect_call_and_rtti_removal(bool force=false)
irep_idt name
The unique identifier.
const std::list< std::string > & get_values(const std::string &option) const
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, symbol_tablet &, message_handlert &)> &library)
Complete missing function definitions using the library.
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
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties...
Field-insensitive, location-sensitive bitvector analysis.
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
Function Entering and Exiting.
Over-approximate Concurrency for Threaded Goto Programs.
#define HELP_REACHABILITY_SLICER
void undefined_function_abort_path(goto_modelt &goto_model)
Skip over selected loops by adding gotos.
void output_safe_dereferences(std::ostream &stream, const goto_programt &program)
Output safely dereferenced expressions per instruction in human-readable format.
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 Indirect Function Calls.
std::wstring widen(const char *s)
instrumentation_strategyt
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Functions for replacing virtual function call with a static function calls in functions, groups of functions and goto programs.
Non-graph-based representation of the class hierarchy.
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)
void list_undefined_functions(const goto_modelt &goto_model, std::ostream &os)
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)
Field-sensitive, location-insensitive points-to analysis.
unsigned unsafe_string2unsigned(const std::string &str, int base)
void compute_loop_numbers()
Remove function definition.
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 print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
std::list< std::string > defines
std::size_t safe_string2size_t(const std::string &str, int base)
#define HELP_SHOW_CLASS_HIERARCHY
Remove calls to functions without a body.
Dump C from Goto Program.
std::string get_value(char option) const
ui_message_handlert ui_message_handler
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 remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
function_mapt function_map
Race Detection for Threaded Goto Programs.
Field-insensitive, location-sensitive bitvector analysis.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
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_tablet symbol_table
Symbol table.
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
Weak Memory Instrumentation for Threaded Goto Programs.
virtual int doit()
invoke main modules
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
void remove_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
bool preserve_all_direct_paths
void print_path_lengths(const goto_modelt &goto_model)
Documentation of Properties.
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
void preserve_functions(const std::list< std::string > &function_list)
Adds a list of functions to the set of functions for the aggressive slicer to preserve.
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...
bool model_argc_argv(goto_modelt &goto_model, unsigned max_argc, message_handlert &message_handler)
Set up argv with up to max_argc pointers into an array of 4096 bytes.
Set the properties to check.
bool function_pointer_removal_done
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Output the abstract states for a whole program.
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)
void dot(const goto_modelt &src, std::ostream &out)
void horn_encoding(const goto_modelt &, std::ostream &)
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
Read a goto binary from a file, but do not update config.
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3)
void check(const goto_modelt &, bool xml, std::ostream &)
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
virtual bool isset(char option) const
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
bool partial_inlining_done
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
void output_xml(std::ostream &out) const
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void list_eloc(const goto_modelt &goto_model)
void output_dot(std::ostream &out) const
std::list< std::string > name_snippets
#define HELP_REPLACE_CALLS
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Dump Goto-Program as DOT Graph.
void remove_functions(goto_modelt &goto_model, 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...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
void slice_global_inits(goto_modelt &goto_model)
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 parse_unwindset_file(const std::string &file_name)
void restore_returns(goto_modelt &goto_model)
restores return statements
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void validate(const validation_modet vm) const
Check that the goto model is well-formed.
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void do_partial_inlining()
void show_value_sets(ui_message_handlert::uit ui, const goto_modelt &goto_model, const value_set_analysist &value_set_analysis)
void instrument_goto_program()
std::string banner_string(const std::string &front_end, const std::string &version)
void output(std::ostream &stream, const goto_programt &program)
Output non-null expressions per instruction in human-readable format.
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void output_dot(std::ostream &out) const
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void output(std::ostream &out) const
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
void parse_unwindset(const std::string &unwindset)
#define HELP_GOTO_PROGRAM_STATS
void set_from_symbol_table(const symbol_tablet &)
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
Interrupt Instrumentation for Goto Programs.
A generic container class for the GOTO intermediate representation of one function.
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
Verify and use annotated invariants and pre/post-conditions.
unsigned safe_string2unsigned(const std::string &str, int base)
#define HELP_REMOVE_CALLS_NO_BODY
void havoc_loops(goto_modelt &goto_model)
void output(std::ostream &out) const
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
typet type
Type of symbol.
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
Generate function bodies with some default behavior A list of currently accepted command line argumen...
message_handlert & get_message_handler()
std::list< std::string > get_comma_separated_values(const char *option) const
std::list< std::string > user_specified_properties
Goto Programs with Functions.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & result() const
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
mstreamt & status() const
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
#define HELP_SHOW_GOTO_FUNCTIONS
const char * CBMC_VERSION
virtual void help()
display command line help
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
void add_failed_symbols(symbol_table_baset &symbol_table)
Create a failed-dereference symbol for all symbols in the given table that need one (i...
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Harnessing for goto functions.
#define CPROVER_EXIT_CONVERSION_FAILED
Failure to convert / write to another format.
void check_call_sequence(const goto_modelt &goto_model)
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
Handling of functions without body.
Local safe pointer analysis.
void weak_memory(memory_modelt model, value_setst &value_sets, goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, 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)
ui_message_handlert::uit get_ui()
#define HELP_REPLACE_FUNCTION_BODY
void count_eloc(const goto_modelt &goto_model)
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
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 interval_analysis(goto_modelt &goto_model)
Initialises the abstract interpretation over interval domain and instruments instructions using inter...
Expression to hold a symbol (variable)
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
void code_contracts(goto_modelt &goto_model)
#define CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT
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.
Encoding for Threaded Goto Programs.
The aggressive slicer removes the body of all the functions except those on the shortest path...
void parse_unwind(const std::string &unwind)
void instrument(goto_modelt &)
#define forall_goto_functions(it, functions)
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
void function_exit(goto_modelt &goto_model, const irep_idt &id)
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Field-insensitive, location-sensitive, over-approximative escape analysis.
#define forall_goto_program_instructions(it, program)
Add parameter assignments.
message_handlert * message_handler
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void print_global_state_size(const goto_modelt &goto_model)
This is a may analysis (i.e.
virtual void register_languages()
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
void function_path_reachability_slicer(goto_modelt &goto_model, const std::list< std::string > &functions_list)
Perform reachability slicing on goto_model for selected functions.
void branch(goto_modelt &goto_model, const irep_idt &id)
void thread_exit_instrumentation(goto_programt &goto_program)
Race Detection for Threaded Goto Programs.
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)
bool splice_call(goto_functionst &goto_functions, const std::string &callercallee, const symbol_tablet &symbol_table, message_handlert &message_handler)
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)