133 bool unwindset_file_given=
cmdline.
isset(
"unwindset-file");
135 if(unwindset_given && unwindset_file_given)
136 throw "only one of --unwindset and --unwindset-file supported at a " 139 if(unwind_given || unwindset_given || unwindset_file_given)
146 if(unwindset_file_given)
152 bool unwinding_assertions=
cmdline.
isset(
"unwinding-assertions");
154 bool continue_as_loops=
cmdline.
isset(
"continue-as-loops");
156 if(unwinding_assertions+partial_loops+continue_as_loops>1)
157 throw "more than one of --unwinding-assertions,--partial-loops," 158 "--continue-as-loops selected";
163 if(unwinding_assertions)
167 else if(partial_loops)
171 else if(continue_as_loops)
177 goto_unwind(
goto_model, unwindset, unwind_strategy);
182 bool have_file=!filename.empty() && filename!=
"-";
189 std::ofstream of(
widen(filename));
191 std::ofstream of(filename);
194 throw "failed to open file "+filename;
201 std::cout <<
result <<
'\n';
219 std::cout <<
"////\n";
220 std::cout <<
"//// Function: " << f_it->first <<
'\n';
221 std::cout <<
"////\n\n";
228 std::cout <<
"Is threaded: " << (is_threaded(i_it)?
"True":
"False")
280 std::cout <<
">>>>\n";
281 std::cout <<
">>>> " << it->first <<
'\n';
282 std::cout <<
">>>>\n";
283 local_bitvector_analysis.
output(std::cout, it->second, ns);
301 local_safe_pointers(it->second.body);
302 std::cout <<
">>>>\n";
303 std::cout <<
">>>> " << it->first <<
'\n';
304 std::cout <<
">>>>\n";
306 local_safe_pointers.
output(std::cout, it->second.body);
310 std::cout, it->second.body);
379 custom_bitvector_analysis.
check(
399 points_to.
output(std::cout);
534 status() <<
"Starting interpreter" <<
eom;
576 for(
auto const &ins : pair.second.body.instructions)
578 if(ins.code.is_not_nil())
580 if(ins.guard.is_not_nil())
581 status() <<
"[guard] " << ins.guard.pretty() <<
eom;
671 call_graph.
output(std::cout);
687 call_graph.
output(std::cout);
736 status() <<
"Performing full inlining" <<
eom;
739 status() <<
"Removing calls to functions without a body" <<
eom;
751 status() <<
"Horn-clause encoding" <<
eom;
764 error() <<
"Failed to open output file " 781 status() <<
"Removing unused functions" <<
eom;
813 catch(
const std::string &e)
821 error() <<
"Numeric exception : " << e <<
eom;
825 catch(
const std::bad_alloc &)
841 status() <<
"Function Pointer Removal" <<
eom;
846 status() <<
"Virtual function removal" <<
eom;
848 status() <<
"Cleaning inline assembler statements" <<
eom;
864 status() <<
"Removing const function pointers only" <<
eom;
922 options.
set_option(
"assert-to-assume",
false);
953 status() <<
"Adding gotos to skip loops" <<
eom;
969 status() <<
"Adding up to " << max_argc
970 <<
" command line arguments" <<
eom;
1016 status() <<
"Performing full inlining" <<
eom;
1023 status() <<
"Propagating Constants" <<
eom;
1052 status() <<
"Applying Code Contracts" <<
eom;
1061 else if(
cmdline.
isset(
"remove-const-function-pointers"))
1083 status() <<
"Inlining calls of function `" <<
function <<
"'" <<
eom;
1097 bool have_file=!filename.empty() && filename!=
"-";
1110 std::ofstream of(
widen(filename));
1112 std::ofstream of(filename);
1115 throw "failed to open file "+filename;
1122 std::cout <<
result <<
'\n';
1143 status() <<
"Removing calls to functions without a body" <<
eom;
1156 status() <<
"Propagating Constants" <<
eom;
1168 status() <<
"Adding checks for uninitialized local variables" <<
eom;
1175 status() <<
"Adding check for maximum call stack size" <<
eom;
1185 status() <<
"Adding nondeterministic initialization of static/global " 1192 status() <<
"Slicing away initializations of unused global variables" 1202 status() <<
"String Abstraction" <<
eom;
1231 status() <<
"Adding Race Checks" <<
eom;
1256 const unsigned max_var=
1259 const unsigned max_po_trans=
1265 status() <<
"Adding weak memory (TSO) Instrumentation" <<
eom;
1270 status() <<
"Adding weak memory (PSO) Instrumentation" <<
eom;
1275 status() <<
"Adding weak memory (RMO) Instrumentation" <<
eom;
1278 else if(mm==
"power")
1280 status() <<
"Adding weak memory (Power) Instrumentation" <<
eom;
1285 error() <<
"Unknown weak memory model `" << mm <<
"'" <<
eom;
1320 status() <<
"Instrumenting interrupt handler" <<
eom;
1330 status() <<
"Instrumenting memory-mapped I/O" <<
eom;
1336 status() <<
"Sequentializing concurrency" <<
eom;
1358 if(step_case && base_case)
1359 throw "please specify only one of --step-case and --base-case";
1360 else if(!step_case && !base_case)
1361 throw "please specify one of --step-case and --base-case";
1366 throw "please give k>=1";
1368 status() <<
"Instrumenting k-induction for k=" << k <<
", " 1369 << (base_case?
"base case":
"step case") <<
eom;
1376 status() <<
"Function enter instrumentation" <<
eom;
1384 status() <<
"Function exit instrumentation" <<
eom;
1392 status() <<
"Branch instrumentation" <<
eom;
1413 status() <<
"Making volatile variables non-deterministic" <<
eom;
1422 status() <<
"Performing a reachability slice" <<
eom;
1435 status() <<
"Performing a full slice" <<
eom;
1445 status() <<
"Performing call splicing" <<
eom;
1463 *generate_implementation,
1473 status() <<
"Slicing away initializations of unused global variables" 1477 status() <<
"Performing an aggressive slice" <<
eom;
1484 if(
cmdline.
isset(
"aggressive-slice-preserve-function"))
1492 if(
cmdline.
isset(
"aggressive-slice-preserve-functions-containing"))
1497 cmdline.
isset(
"aggressive-slice-preserve-all-direct-paths");
1499 aggressive_slicer.
doit();
1501 status() <<
"Performing a reachability slice" <<
eom;
1518 "* * Copyright (C) 2008-2013 * *\n" 1519 "* * Daniel Kroening * *\n" 1520 "* * kroening@kroening.com * *\n" 1524 " goto-instrument [-?] [-h] [--help] show help\n" 1525 " goto-instrument in out perform instrumentation\n" 1528 " --document-properties-html generate HTML property documentation\n" 1529 " --document-properties-latex generate Latex property documentation\n" 1530 " --dump-c generate C source\n" 1531 " --dump-cpp generate C++ source\n" 1532 " --dot generate CFG graph in DOT format\n" 1533 " --interpreter do concrete execution\n" 1536 " --show-loops show the loops in the program\n" 1538 " --show-symbol-table show loaded symbol table\n" 1539 " --list-symbols list symbols with type information\n" 1542 " --drop-unused-functions drop functions trivially unreachable from main function\n" 1543 " --print-internal-representation\n" 1544 " show verbose internal representation of the program\n" 1545 " --list-undefined-functions list functions without body\n" 1546 " --show-struct-alignment show struct members that might be concurrently accessed\n" 1547 " --show-natural-loops show natural loop heads\n" 1549 " --list-calls-args list all function calls with their arguments\n" 1550 " --call-graph show graph of function calls\n" 1552 " --reachable-call-graph show graph of function calls potentially reachable from main function\n" 1555 " --show-threaded show instructions that may be executed by more than one thread\n" 1556 " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n" 1557 " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n" 1558 " *and* used as a dereference operand\n" 1561 " --no-assertions ignore user assertions\n" 1563 " --uninitialized-check add checks for uninitialized locals (experimental)\n" 1564 " --error-label label check that label is unreachable\n" 1565 " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" 1566 " --race-check add floating-point data race checks\n" 1568 "Semantic transformations:\n" 1569 " --nondet-volatile makes reads from volatile variables non-deterministic\n" 1570 " --unwind <n> unwinds the loops <n> times\n" 1571 " --unwindset L:B,... unwind loop L with a bound of B\n" 1572 " --unwindset-file <file> read unwindset from file\n" 1573 " --partial-loops permit paths with partial loops\n" 1574 " --unwinding-assertions generate unwinding assertions\n" 1575 " --continue-as-loops add loop for remaining iterations after unwound part\n" 1576 " --isr <function> instruments an interrupt service routine\n" 1577 " --mmio instruments memory-mapped I/O\n" 1578 " --nondet-static add nondeterministic initialization of variables with static lifetime\n" 1579 " --check-invariant function instruments invariant checking function\n" 1580 " --remove-pointers converts pointer arithmetic to base+offset expressions\n" 1581 " --splice-call caller,callee prepends a call to callee in the body of caller\n" 1582 " --undefined-function-is-assume-false\n" 1584 " convert each call to an undefined function to assume(false)\n" 1587 "Loop transformations:\n" 1588 " --k-induction <k> check loops with k-induction\n" 1589 " --step-case k-induction: do step-case\n" 1590 " --base-case k-induction: do base-case\n" 1591 " --havoc-loops over-approximate all loops\n" 1592 " --accelerate add loop accelerators\n" 1593 " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" 1595 "Memory model instrumentations:\n" 1596 " --mm <tso,pso,rmo,power> instruments a weak memory model\n" 1597 " --scc detects critical cycles per SCC (one thread per SCC)\n" 1598 " --one-event-per-cycle only instruments one event per cycle\n" 1599 " --minimum-interference instruments an optimal number of events\n" 1600 " --my-events only instruments events whose ids appear in inst.evt\n" 1601 " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" 1602 " --no-dependencies no dependency analysis\n" 1604 " --no-po-rendering no representation of the threads in the dot\n" 1605 " --render-cluster-file clusterises the dot by files\n" 1606 " --render-cluster-function clusterises the dot by functions\n" 1609 " --reachability-slice slice away instructions that can't reach assertions\n" 1610 " --full-slice slice away instructions that don't affect assertions\n" 1611 " --property id slice with respect to specific property only\n" 1612 " --slice-global-inits slice away initializations of unused global variables\n" 1613 " --aggressive-slice remove bodies of any functions not on the shortest path between\n" 1614 " the start function and the function containing the property(s)\n" 1615 " --aggressive-slice-call-depth <n>\n" 1616 " used with aggressive-slice, preserves all functions within <n> function calls\n" 1617 " of the functions on the shortest path\n" 1618 " --aggressive-slice-preserve-function <f>\n" 1619 " force the aggressive slicer to preserve function <f>\n" 1620 " --aggressive-slice-preserve-function containing <f>\n" 1621 " force the aggressive slicer to preserve all functions with names containing <f>\n" 1622 "--aggressive-slice-preserve-all-direct-paths \n" 1623 " force aggressive slicer to preserve all direct paths\n" 1625 "Further transformations:\n" 1626 " --constant-propagator propagate constants and simplify expressions\n" 1627 " --inline perform full inlining\n" 1628 " --partial-inline perform partial inlining\n" 1629 " --function-inline <function> transitively inline all calls <function> makes\n" 1630 " --no-caching disable caching of intermediate results during transitive function inlining\n" 1631 " --log <file> log in json format which code segments were inlined, use with --function-inline\n" 1632 " --remove-function-pointers replace function pointers by case statement over function calls\n" 1635 " --add-library add models of C library functions\n" 1636 " --model-argc-argv <n> model up to <n> command line arguments\n" 1638 " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n" 1642 " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" 1643 " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" 1644 " --harness with --dump-c/--dump-cpp: include input generator in output\n" 1645 " --version show version and exit\n" 1647 " --xml-ui use XML-formatted output\n" 1648 " --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.
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)
Remove Virtual Function (Method) Calls.
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
#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.
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.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
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)
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)
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_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
bool preserve_all_direct_paths
void print_path_lengths(const goto_modelt &goto_model)
Documentation of Properties.
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
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 &)
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert::uit ui)
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
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)
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert::uit ui)
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 output_xml(std::ostream &out) const
Nondeterministic initialization of certain global scope variables.
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...
#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
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
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 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 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)
removes assembler
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 > user_specified_properties
Goto Programs with Functions.
static irep_idt entry_point()
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & result() const
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
#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 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 show_class_hierarchy(const class_hierarchyt &hierarchy, message_handlert &message_handler, ui_message_handlert::uit ui, bool children_only)
Output the class hierarchy.
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...
goto_programt & goto_program
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)
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 namespace_baset::lookup().
void print_global_state_size(const goto_modelt &goto_model)
virtual void register_languages()
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
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)
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)
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const int i_depth, const exprt &max_depth)