Go to the documentation of this file.
143 const bool validate_only =
cmdline.
isset(
"validate-goto-binary");
145 if(validate_only ||
cmdline.
isset(
"validate-goto-model"))
166 bool unwindset_file_given=
cmdline.
isset(
"unwindset-file");
168 if(unwindset_given && unwindset_file_given)
169 throw "only one of --unwindset and --unwindset-file supported at a "
172 if(unwind_given || unwindset_given || unwindset_file_given)
179 if(unwindset_file_given)
185 bool unwinding_assertions=
cmdline.
isset(
"unwinding-assertions");
187 bool continue_as_loops=
cmdline.
isset(
"continue-as-loops");
189 if(unwinding_assertions+partial_loops+continue_as_loops>1)
190 throw "more than one of --unwinding-assertions,--partial-loops,"
191 "--continue-as-loops selected";
196 if(unwinding_assertions)
200 else if(partial_loops)
204 else if(continue_as_loops)
210 goto_unwind(
goto_model, unwindset, unwind_strategy);
215 bool have_file=!filename.empty() && filename!=
"-";
222 std::ofstream of(
widen(filename));
224 std::ofstream of(filename);
227 throw "failed to open file "+filename;
234 std::cout << result <<
'\n';
252 std::cout <<
"////\n";
253 std::cout <<
"//// Function: " << gf_entry.first <<
'\n';
254 std::cout <<
"////\n\n";
261 std::cout <<
"Is threaded: " << (is_threaded(i_it)?
"True":
"False")
328 std::cout <<
">>>>\n";
329 std::cout <<
">>>> " << gf_entry.first <<
'\n';
330 std::cout <<
">>>>\n";
331 local_bitvector_analysis.
output(std::cout, gf_entry.second, ns);
349 local_safe_pointers(gf_entry.second.body);
350 std::cout <<
">>>>\n";
351 std::cout <<
">>>> " << gf_entry.first <<
'\n';
352 std::cout <<
">>>>\n";
354 local_safe_pointers.
output(std::cout, gf_entry.second.body, ns);
358 std::cout, gf_entry.second.body, ns);
376 sese_region_analysis(gf_entry.second.body);
377 std::cout <<
">>>>\n";
378 std::cout <<
">>>> " << gf_entry.first <<
'\n';
379 std::cout <<
">>>>\n";
380 sese_region_analysis.
output(std::cout, gf_entry.second.body, ns);
448 custom_bitvector_analysis.
check(
468 points_to.
output(std::cout);
653 for(
auto const &ins : pair.second.body.instructions)
655 if(ins.get_code().is_not_nil())
657 if(ins.has_condition())
659 log.
status() <<
"[guard] " << ins.get_condition().pretty()
699 const bool is_header =
cmdline.
isset(
"dump-c-type-header");
775 call_graph.
output(std::cout);
791 call_graph.
output(std::cout);
842 log.
status() <<
"Removing calls to functions without a body"
910 "Invalid number of positional arguments passed",
912 "goto-instrument needs one input and one output file, aside from other "
993 if(!result.has_value())
1033 const auto function_pointer_restrictions =
1058 log.
status() <<
"Adding up to " << max_argc <<
" command line arguments"
1138 const std::list<std::pair<std::string, std::string>> contract_flags(
1141 for(
const auto &pair : contract_flags)
1145 log.
error() <<
"Pass at most one of --" << pair.first <<
" and --"
1161 std::set<std::string> to_replace(
1174 std::set<std::string> to_enforce(
1200 else if(
cmdline.
isset(
"remove-const-function-pointers"))
1222 log.
status() <<
"Inlining calls of function '" <<
function <<
"'"
1233 bool have_file=!filename.empty() && filename!=
"-";
1241 std::ofstream of(
widen(filename));
1243 std::ofstream of(filename);
1246 throw "failed to open file "+filename;
1253 std::cout << result <<
'\n';
1274 log.
status() <<
"Removing calls to functions without a body"
1299 c_object_factory_options);
1303 object_factory_parameters,
1308 *generate_implementation,
1318 c_object_factory_options);
1320 auto options_split =
1322 if(options_split.size() < 2)
1324 "not enough arguments for this option",
"--generate-havocing-body"};
1326 if(options_split.size() == 2)
1329 std::string{
"havoc,"} + options_split.back(),
1330 object_factory_parameters,
1334 std::regex(options_split[0]),
1335 *generate_implementation,
1342 for(
size_t i = 1; i + 1 < options_split.size(); i += 2)
1345 std::string{
"havoc,"} + options_split[i + 1],
1346 object_factory_parameters,
1352 *generate_implementation,
1365 log.
status() <<
"Adding checks for uninitialized local variables"
1383 log.
status() <<
"Adding nondeterministic initialization "
1384 "of static/global variables except for "
1385 "the specified ones."
1392 log.
status() <<
"Adding nondeterministic initialization "
1393 "of static/global variables"
1400 log.
status() <<
"Slicing away initializations of unused global variables"
1462 const unsigned max_var=
1465 const unsigned max_po_trans=
1471 log.
status() <<
"Adding weak memory (TSO) Instrumentation"
1477 log.
status() <<
"Adding weak memory (PSO) Instrumentation"
1483 log.
status() <<
"Adding weak memory (RMO) Instrumentation"
1487 else if(mm==
"power")
1489 log.
status() <<
"Adding weak memory (Power) Instrumentation"
1495 log.
error() <<
"Unknown weak memory model '" << mm <<
"'"
1569 if(step_case && base_case)
1570 throw "please specify only one of --step-case and --base-case";
1571 else if(!step_case && !base_case)
1572 throw "please specify one of --step-case and --base-case";
1577 throw "please give k>=1";
1579 log.
status() <<
"Instrumenting k-induction for k=" << k <<
", "
1580 << (base_case ?
"base case" :
"step case") <<
messaget::eom;
1643 log.
status() <<
"Performing a function pointer reachability slice"
1687 log.
status() <<
"Slicing away initializations of unused global variables"
1698 if(
cmdline.
isset(
"aggressive-slice-preserve-function"))
1706 if(
cmdline.
isset(
"aggressive-slice-preserve-functions-containing"))
1711 cmdline.
isset(
"aggressive-slice-preserve-all-direct-paths");
1713 aggressive_slicer.
doit();
1746 " goto-instrument [-?] [-h] [--help] show help\n"
1747 " goto-instrument in out perform instrumentation\n"
1750 " --document-properties-html generate HTML property documentation\n"
1751 " --document-properties-latex generate Latex property documentation\n"
1752 " --dump-c generate C source\n"
1753 " --dump-c-type-header m generate a C header for types local in m\n"
1754 " --dump-cpp generate C++ source\n"
1755 " --dot generate CFG graph in DOT format\n"
1756 " --interpreter do concrete execution\n"
1759 " --show-loops show the loops in the program\n"
1761 " --show-symbol-table show loaded symbol table\n"
1762 " --list-symbols list symbols with type information\n"
1765 " --drop-unused-functions drop functions trivially unreachable from main function\n"
1766 " --print-internal-representation\n"
1767 " show verbose internal representation of the program\n"
1768 " --list-undefined-functions list functions without body\n"
1769 " --show-struct-alignment show struct members that might be concurrently accessed\n"
1770 " --show-natural-loops show natural loop heads\n"
1772 " --list-calls-args list all function calls with their arguments\n"
1773 " --call-graph show graph of function calls\n"
1775 " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1778 " --show-threaded show instructions that may be executed by more than one thread\n"
1779 " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n"
1780 " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n"
1781 " *and* used as a dereference operand\n"
1784 " --validate-goto-binary check the well-formedness of the passed in goto\n"
1785 " binary and then exit\n"
1788 " --no-assertions ignore user assertions\n"
1790 " --uninitialized-check add checks for uninitialized locals (experimental)\n"
1791 " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n"
1792 " --race-check add floating-point data race checks\n"
1794 "Semantic transformations:\n"
1796 " --unwind <n> unwinds the loops <n> times\n"
1797 " --unwindset L:B,... unwind loop L with a bound of B\n"
1798 " --unwindset-file <file> read unwindset from file\n"
1799 " --partial-loops permit paths with partial loops\n"
1800 " --unwinding-assertions generate unwinding assertions\n"
1801 " --continue-as-loops add loop for remaining iterations after unwound part\n"
1802 " --isr <function> instruments an interrupt service routine\n"
1803 " --mmio instruments memory-mapped I/O\n"
1804 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1805 " --nondet-static-exclude e same as nondet-static except for the variable e\n"
1806 " (use multiple times if required)\n"
1807 " --check-invariant function instruments invariant checking function\n"
1808 " --remove-pointers converts pointer arithmetic to base+offset expressions\n"
1809 " --splice-call caller,callee prepends a call to callee in the body of caller\n"
1810 " --undefined-function-is-assume-false\n"
1812 " convert each call to an undefined function to assume(false)\n"
1817 "Loop transformations:\n"
1818 " --k-induction <k> check loops with k-induction\n"
1819 " --step-case k-induction: do step-case\n"
1820 " --base-case k-induction: do base-case\n"
1821 " --havoc-loops over-approximate all loops\n"
1822 " --accelerate add loop accelerators\n"
1823 " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n"
1825 "Memory model instrumentations:\n"
1826 " --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1827 " --scc detects critical cycles per SCC (one thread per SCC)\n"
1828 " --one-event-per-cycle only instruments one event per cycle\n"
1829 " --minimum-interference instruments an optimal number of events\n"
1830 " --my-events only instruments events whose ids appear in inst.evt\n"
1831 " --cfg-kill enables symbolic execution used to reduce spurious cycles\n"
1832 " --no-dependencies no dependency analysis\n"
1834 " --no-po-rendering no representation of the threads in the dot\n"
1835 " --render-cluster-file clusterises the dot by files\n"
1836 " --render-cluster-function clusterises the dot by functions\n"
1840 " --full-slice slice away instructions that don't affect assertions\n"
1841 " --property id slice with respect to specific property only\n"
1842 " --slice-global-inits slice away initializations of unused global variables\n"
1843 " --aggressive-slice remove bodies of any functions not on the shortest path between\n"
1844 " the start function and the function containing the property(s)\n"
1845 " --aggressive-slice-call-depth <n>\n"
1846 " used with aggressive-slice, preserves all functions within <n> function calls\n"
1847 " of the functions on the shortest path\n"
1848 " --aggressive-slice-preserve-function <f>\n"
1849 " force the aggressive slicer to preserve function <f>\n"
1850 " --aggressive-slice-preserve-function containing <f>\n"
1851 " force the aggressive slicer to preserve all functions with names containing <f>\n"
1852 "--aggressive-slice-preserve-all-direct-paths \n"
1853 " force aggressive slicer to preserve all direct paths\n"
1855 "Further transformations:\n"
1856 " --constant-propagator propagate constants and simplify expressions\n"
1857 " --inline perform full inlining\n"
1858 " --partial-inline perform partial inlining\n"
1859 " --function-inline <function> transitively inline all calls <function> makes\n"
1860 " --no-caching disable caching of intermediate results during transitive function inlining\n"
1861 " --log <file> log in json format which code segments were inlined, use with --function-inline\n"
1862 " --remove-function-pointers replace function pointers by case statement over function calls\n"
1863 " --value-set-fi-fp-removal build flow-insensitive value set and replace function pointers by a case statement\n"
1864 " over the possible assignments. If the set of possible assignments is empty the function pointer\n"
1865 " is removed using the standard remove-function-pointers pass. \n"
1869 " --add-library add models of C library functions\n"
1870 " --model-argc-argv <n> model up to <n> command line arguments\n"
1872 " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1883 " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n"
1884 " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n"
1885 " --harness with --dump-c/--dump-cpp: include input generator in output\n"
1886 " --version show version and exit\n"
1888 " --xml-ui use XML-formatted output\n"
1889 " --json-ui use JSON-formatted output\n"
void help() override
display command line help
void value_set_fi_fp_removal(goto_modelt &goto_model, message_handlert &message_handler)
Builds the flow-insensitive value set for all function pointers and replaces function pointers with a...
#define HELP_REACHABILITY_SLICER
std::list< std::string > defines
#define HELP_SHOW_GOTO_FUNCTIONS
Encoding for Threaded Goto Programs.
void horn_encoding(const goto_modelt &, std::ostream &)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Non-graph-based representation of the class hierarchy.
ui_message_handlert ui_message_handler
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.
void parse_unwindset_file(const std::string &file_name)
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
Field-insensitive, location-sensitive bitvector analysis.
#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
bool enforce_contracts(const std::set< std::string > &functions)
Turn requires & ensures into assumptions and assertions for each of the named functions.
virtual bool isset(char option) const
void print_global_state_size(const goto_modelt &goto_model)
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
void do_partial_inlining()
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
bool function_pointer_removal_done
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
#define CHECK_RETURN(CONDITION)
Skip over selected loops by adding gotos.
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
void output(std::ostream &out, const goto_programt &goto_program, const namespacet &ns) const
mstreamt & status() const
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Field-insensitive, location-sensitive bitvector analysis.
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
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...
typet type
Type of symbol.
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
void output_safe_dereferences(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output safely dereferenced expressions per instruction in human-readable format.
bool write_goto_binary(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
#define FLAG_REPLACE_CALL
void dot(const goto_modelt &src, std::ostream &out)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void restrict_function_pointers(goto_modelt &goto_model, const function_pointer_restrictionst &restrictions)
Apply function pointer restrictions to a goto_model.
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
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.
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
void label_function_pointer_call_sites(goto_modelt &goto_model)
This ensures that call instructions can be only one of two things:
bool splice_call(goto_functionst &goto_functions, const std::string &callercallee, const symbol_tablet &symbol_table, message_handlert &message_handler)
void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
Functions for replacing virtual function call with a static function calls in functions,...
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
#define HELP_SHOW_CLASS_HIERARCHY
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.
bool replace_calls(const std::set< std::string > &functions)
Replace all calls to each function in the list with that function's contract.
This template class implements a data-flow analysis which keeps track of what values different variab...
void remove_virtual_functions(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...
Interpreter for GOTO Programs.
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
static void race_check(value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, w_guardst &w_guards)
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Remove calls to functions without a body.
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 show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
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: assert-false, assume-false, assert-false-assume-...
bool preserve_all_direct_paths
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
void set_option(const std::string &option, const bool value)
Weak Memory Instrumentation for Threaded Goto Programs.
int doit() override
invoke main modules
#define FLAG_LOOP_CONTRACTS
Insert final assert false into a function.
#define HELP_REPLACE_CALL
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
bool ensure_one_backedge_per_target(goto_programt::targett &it, goto_programt &goto_program)
struct configt::ansi_ct ansi_c
function_mapt function_map
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Expression to hold a symbol (variable)
void output_xml(std::ostream &out) const
Race Detection for Threaded Goto Programs.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
Documentation of Properties.
#define HELP_ENFORCE_ALL_CONTRACTS
Single-entry, single-exit region analysis.
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_functionst &dest)
void output_dot(std::ostream &out) const
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
std::size_t safe_string2size_t(const std::string &str, int base)
void show_value_sets(ui_message_handlert::uit ui, const goto_modelt &goto_model, const value_set_analysist &value_set_analysis)
static function_pointer_restrictionst from_options(const optionst &options, const goto_modelt &goto_model, message_handlert &message_handler)
Parse function pointer restrictions from command line.
void label_properties(goto_modelt &goto_model)
void print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
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 list_undefined_functions(const goto_modelt &goto_model, std::ostream &os)
std::list< std::string > get_comma_separated_values(const char *option) const
#define HELP_ENFORCE_CONTRACT
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Compute lexical loops in a goto_function.
Harnessing for goto functions.
void parse_unwind(const std::string &unwind)
virtual uit get_ui() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
This is unused by this implementation of guards, but can be used by other implementations of the same...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Set the properties to check.
#define FLAG_REPLACE_ALL_CALLS
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
Dump Goto-Program as DOT Graph.
Interrupt Instrumentation for Goto Programs.
const char * CBMC_VERSION
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)
#define HELP_INSERT_FINAL_ASSERT_FALSE
std::string banner_string(const std::string &front_end, const std::string &version)
void apply_loop_contracts()
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
void branch(goto_modelt &goto_model, const irep_idt &id)
void do_indirect_call_and_rtti_removal(bool force=false)
Given goto functions and a list of function parameters or globals that are function pointers with lis...
void check_call_sequence(const goto_modelt &goto_model)
#define HELP_GOTO_PROGRAM_STATS
void register_languages() override
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 undefined_function_abort_path(goto_modelt &goto_model)
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
#define PRECONDITION(CONDITION)
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
static void interrupt(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, const symbol_exprt &interrupt_handler, const rw_set_baset &isr_rw_set)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void remove_pointers(goto_modelt &goto_model, value_setst &value_sets)
Remove dereferences in all expressions contained in the program goto_model.
Over-approximate Concurrency for Threaded Goto Programs.
void instrument_goto_program()
#define HELP_REMOVE_CALLS_NO_BODY
#define HELP_LOOP_CONTRACTS
void dump_c_type_header(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, const std::string module, std::ostream &out)
std::string get_value(char option) const
Remove function definition.
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
#define HELP_SHOW_PROPERTIES
flow insensitive value set function pointer removal
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
void count_eloc(const goto_modelt &goto_model)
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Local safe pointer analysis.
#define FLAG_ENFORCE_ALL_CONTRACTS
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
void instrument(goto_modelt &)
void slice_global_inits(goto_modelt &goto_model)
void set_from_symbol_table(const symbol_tablet &)
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls made from a particular function.
void compute_loop_numbers()
#define CPROVER_EXIT_CONVERSION_FAILED
Failure to convert / write to another format.
std::wstring widen(const char *s)
#define HELP_REPLACE_FUNCTION_BODY
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
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)
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
bool partial_inlining_done
unsigned safe_string2unsigned(const std::string &str, int base)
static void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program)
#define HELP_ANSI_C_LANGUAGE
void output(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output non-null expressions per instruction in human-readable format.
std::list< std::string > user_specified_properties
This is a may analysis (i.e.
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.
Replace function returns by assignments to global variables.
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...
Function Entering and Exiting.
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Detection for Uninitialized Local Variables.
Field-sensitive, location-insensitive points-to analysis.
message_handlert & get_message_handler()
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
The aggressive slicer removes the body of all the functions except those on the shortest path,...
Handling of functions without body.
goto_functionst goto_functions
GOTO functions.
#define RESTRICT_FUNCTION_POINTER_OPT
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Memory-mapped I/O Instrumentation for Goto Programs.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
bool set(const cmdlinet &cmdline)
Race Detection for Threaded Goto Programs.
Document and give macros for the exit codes of CPROVER binaries.
void output(std::ostream &out) const
Compute natural loops in a goto_function.
#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
std::list< std::string > name_snippets
#define HELP_REPLACE_ALL_CALLS
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
unsigned unsafe_string2unsigned(const std::string &str, int base)
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 accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
Add parameter assignments.
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.
A generic container class for the GOTO intermediate representation of one function.
void output_dot(std::ostream &out) const
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
void check(const goto_modelt &, bool xml, std::ostream &)
void output(std::ostream &out) const
bool insert_final_assert_false(goto_modelt &goto_model, const std::string &function_to_instrument, message_handlert &message_handler)
Transform a goto program by inserting assert(false) at the end of a given function function_to_instru...
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
void parse_unwindset(const std::list< std::string > &unwindset)
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
Initialize command line arguments.
void function_exit(goto_modelt &goto_model, const irep_idt &id)
#define FLAG_ENFORCE_CONTRACT
instrumentation_strategyt
Remove initializations of unused global variables.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
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....
Field-insensitive, location-sensitive, over-approximative escape analysis.
void havoc_loops(goto_modelt &goto_model)
Ensure one backedge per target.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
#define HELP_REPLACE_CALLS
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 list_eloc(const goto_modelt &goto_model)
Label function pointer call sites across a goto model.
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, const irep_idt &function_id, bool add_safety_assertion, bool only_remove_const_fps)
void nondet_volatile(goto_modelt &goto_model, const optionst &options)
Havoc reads from volatile expressions, if enabled in the options.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Dump C from Goto Program.
void thread_exit_instrumentation(goto_programt &goto_program)
const std::list< std::string > & get_values(const std::string &option) const
Remove Indirect Function Calls.
symbol_tablet symbol_table
Symbol table.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
void print_path_lengths(const goto_modelt &goto_model)
irep_idt name
The unique identifier.
void restore_returns(goto_modelt &goto_model)
restores return statements
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)
#define forall_goto_program_instructions(it, program)
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
jsont output_log_json() const
#define HELP_RESTRICT_FUNCTION_POINTER
void interval_analysis(goto_modelt &goto_model)
Initialises the abstract interpretation over interval domain and instruments instructions using inter...
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Inline every function call into the entry_point() function.
Field-insensitive, location-sensitive, over-approximative escape analysis.
#define HELP_NONDET_VOLATILE