Go to the documentation of this file.
142 const bool validate_only =
cmdline.
isset(
"validate-goto-binary");
144 if(validate_only ||
cmdline.
isset(
"validate-goto-model"))
165 bool unwindset_file_given=
cmdline.
isset(
"unwindset-file");
167 if(unwindset_given && unwindset_file_given)
168 throw "only one of --unwindset and --unwindset-file supported at a "
171 if(unwind_given || unwindset_given || unwindset_file_given)
178 if(unwindset_file_given)
184 bool unwinding_assertions=
cmdline.
isset(
"unwinding-assertions");
186 bool continue_as_loops=
cmdline.
isset(
"continue-as-loops");
188 if(unwinding_assertions+partial_loops+continue_as_loops>1)
189 throw "more than one of --unwinding-assertions,--partial-loops,"
190 "--continue-as-loops selected";
195 if(unwinding_assertions)
199 else if(partial_loops)
203 else if(continue_as_loops)
209 goto_unwind(
goto_model, unwindset, unwind_strategy);
214 bool have_file=!filename.empty() && filename!=
"-";
221 std::ofstream of(
widen(filename));
223 std::ofstream of(filename);
226 throw "failed to open file "+filename;
233 std::cout << result <<
'\n';
251 std::cout <<
"////\n";
252 std::cout <<
"//// Function: " << f_it->first <<
'\n';
253 std::cout <<
"////\n\n";
260 std::cout <<
"Is threaded: " << (is_threaded(i_it)?
"True":
"False")
327 std::cout <<
">>>>\n";
328 std::cout <<
">>>> " << it->first <<
'\n';
329 std::cout <<
">>>>\n";
330 local_bitvector_analysis.
output(std::cout, it->second, ns);
348 local_safe_pointers(it->second.body);
349 std::cout <<
">>>>\n";
350 std::cout <<
">>>> " << it->first <<
'\n';
351 std::cout <<
">>>>\n";
353 local_safe_pointers.
output(std::cout, it->second.body, ns);
357 std::cout, it->second.body, ns);
375 sese_region_analysis(it->second.body);
376 std::cout <<
">>>>\n";
377 std::cout <<
">>>> " << it->first <<
'\n';
378 std::cout <<
">>>>\n";
379 sese_region_analysis.
output(std::cout, it->second.body, ns);
447 custom_bitvector_analysis.
check(
467 points_to.
output(std::cout);
649 for(
auto const &ins : pair.second.body.instructions)
651 if(ins.code.is_not_nil())
653 if(ins.has_condition())
655 log.
status() <<
"[guard] " << ins.get_condition().pretty()
695 const bool is_header =
cmdline.
isset(
"dump-c-type-header");
771 call_graph.
output(std::cout);
787 call_graph.
output(std::cout);
838 log.
status() <<
"Removing calls to functions without a body"
906 "Invalid number of positional arguments passed",
908 "goto-instrument needs one input and one output file, aside from other "
989 if(!result.has_value())
1011 options.
set_option(
"assert-to-assume",
true);
1013 options.
set_option(
"assert-to-assume",
false);
1051 const auto function_pointer_restrictions =
1076 log.
status() <<
"Adding up to " << max_argc <<
" command line arguments"
1156 const std::list<std::pair<std::string, std::string>> contract_flags(
1159 for(
const auto &pair : contract_flags)
1163 log.
error() <<
"Pass at most one of --" << pair.first <<
" and --"
1178 std::set<std::string> to_replace(
1191 std::set<std::string> to_enforce(
1214 else if(
cmdline.
isset(
"remove-const-function-pointers"))
1236 log.
status() <<
"Inlining calls of function '" <<
function <<
"'"
1247 bool have_file=!filename.empty() && filename!=
"-";
1255 std::ofstream of(
widen(filename));
1257 std::ofstream of(filename);
1260 throw "failed to open file "+filename;
1267 std::cout << result <<
'\n';
1288 log.
status() <<
"Removing calls to functions without a body"
1313 c_object_factory_options);
1317 object_factory_parameters,
1322 *generate_implementation,
1332 c_object_factory_options);
1334 auto options_split =
1336 if(options_split.size() < 2)
1338 "not enough arguments for this option",
"--generate-havocing-body"};
1340 if(options_split.size() == 2)
1343 std::string{
"havoc,"} + options_split.back(),
1344 object_factory_parameters,
1348 std::regex(options_split[0]),
1349 *generate_implementation,
1356 for(
size_t i = 1; i + 1 < options_split.size(); i += 2)
1359 std::string{
"havoc,"} + options_split[i + 1],
1360 object_factory_parameters,
1366 *generate_implementation,
1379 log.
status() <<
"Adding checks for uninitialized local variables"
1397 log.
status() <<
"Adding nondeterministic initialization "
1398 "of static/global variables except for "
1399 "the specified ones."
1406 log.
status() <<
"Adding nondeterministic initialization "
1407 "of static/global variables"
1414 log.
status() <<
"Slicing away initializations of unused global variables"
1476 const unsigned max_var=
1479 const unsigned max_po_trans=
1485 log.
status() <<
"Adding weak memory (TSO) Instrumentation"
1491 log.
status() <<
"Adding weak memory (PSO) Instrumentation"
1497 log.
status() <<
"Adding weak memory (RMO) Instrumentation"
1501 else if(mm==
"power")
1503 log.
status() <<
"Adding weak memory (Power) Instrumentation"
1509 log.
error() <<
"Unknown weak memory model '" << mm <<
"'"
1583 if(step_case && base_case)
1584 throw "please specify only one of --step-case and --base-case";
1585 else if(!step_case && !base_case)
1586 throw "please specify one of --step-case and --base-case";
1591 throw "please give k>=1";
1593 log.
status() <<
"Instrumenting k-induction for k=" << k <<
", "
1594 << (base_case ?
"base case" :
"step case") <<
messaget::eom;
1657 log.
status() <<
"Performing a function pointer reachability slice"
1701 log.
status() <<
"Slicing away initializations of unused global variables"
1712 if(
cmdline.
isset(
"aggressive-slice-preserve-function"))
1720 if(
cmdline.
isset(
"aggressive-slice-preserve-functions-containing"))
1725 cmdline.
isset(
"aggressive-slice-preserve-all-direct-paths");
1727 aggressive_slicer.
doit();
1760 " goto-instrument [-?] [-h] [--help] show help\n"
1761 " goto-instrument in out perform instrumentation\n"
1764 " --document-properties-html generate HTML property documentation\n"
1765 " --document-properties-latex generate Latex property documentation\n"
1766 " --dump-c generate C source\n"
1767 " --dump-c-type-header m generate a C header for types local in m\n"
1768 " --dump-cpp generate C++ source\n"
1769 " --dot generate CFG graph in DOT format\n"
1770 " --interpreter do concrete execution\n"
1773 " --show-loops show the loops in the program\n"
1775 " --show-symbol-table show loaded symbol table\n"
1776 " --list-symbols list symbols with type information\n"
1779 " --drop-unused-functions drop functions trivially unreachable from main function\n"
1780 " --print-internal-representation\n"
1781 " show verbose internal representation of the program\n"
1782 " --list-undefined-functions list functions without body\n"
1783 " --show-struct-alignment show struct members that might be concurrently accessed\n"
1784 " --show-natural-loops show natural loop heads\n"
1786 " --list-calls-args list all function calls with their arguments\n"
1787 " --call-graph show graph of function calls\n"
1789 " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1792 " --show-threaded show instructions that may be executed by more than one thread\n"
1793 " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n"
1794 " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n"
1795 " *and* used as a dereference operand\n"
1798 " --validate-goto-binary check the well-formedness of the passed in goto\n"
1799 " binary and then exit\n"
1802 " --no-assertions ignore user assertions\n"
1804 " --uninitialized-check add checks for uninitialized locals (experimental)\n"
1805 " --error-label label check that label is unreachable\n"
1806 " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n"
1807 " --race-check add floating-point data race checks\n"
1809 "Semantic transformations:\n"
1811 " --unwind <n> unwinds the loops <n> times\n"
1812 " --unwindset L:B,... unwind loop L with a bound of B\n"
1813 " --unwindset-file <file> read unwindset from file\n"
1814 " --partial-loops permit paths with partial loops\n"
1815 " --unwinding-assertions generate unwinding assertions\n"
1816 " --continue-as-loops add loop for remaining iterations after unwound part\n"
1817 " --isr <function> instruments an interrupt service routine\n"
1818 " --mmio instruments memory-mapped I/O\n"
1819 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1820 " --nondet-static-exclude e same as nondet-static except for the variable e\n"
1821 " (use multiple times if required)\n"
1822 " --check-invariant function instruments invariant checking function\n"
1823 " --remove-pointers converts pointer arithmetic to base+offset expressions\n"
1824 " --splice-call caller,callee prepends a call to callee in the body of caller\n"
1825 " --undefined-function-is-assume-false\n"
1827 " convert each call to an undefined function to assume(false)\n"
1832 "Loop transformations:\n"
1833 " --k-induction <k> check loops with k-induction\n"
1834 " --step-case k-induction: do step-case\n"
1835 " --base-case k-induction: do base-case\n"
1836 " --havoc-loops over-approximate all loops\n"
1837 " --accelerate add loop accelerators\n"
1838 " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n"
1840 "Memory model instrumentations:\n"
1841 " --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1842 " --scc detects critical cycles per SCC (one thread per SCC)\n"
1843 " --one-event-per-cycle only instruments one event per cycle\n"
1844 " --minimum-interference instruments an optimal number of events\n"
1845 " --my-events only instruments events whose ids appear in inst.evt\n"
1846 " --cfg-kill enables symbolic execution used to reduce spurious cycles\n"
1847 " --no-dependencies no dependency analysis\n"
1849 " --no-po-rendering no representation of the threads in the dot\n"
1850 " --render-cluster-file clusterises the dot by files\n"
1851 " --render-cluster-function clusterises the dot by functions\n"
1855 " --full-slice slice away instructions that don't affect assertions\n"
1856 " --property id slice with respect to specific property only\n"
1857 " --slice-global-inits slice away initializations of unused global variables\n"
1858 " --aggressive-slice remove bodies of any functions not on the shortest path between\n"
1859 " the start function and the function containing the property(s)\n"
1860 " --aggressive-slice-call-depth <n>\n"
1861 " used with aggressive-slice, preserves all functions within <n> function calls\n"
1862 " of the functions on the shortest path\n"
1863 " --aggressive-slice-preserve-function <f>\n"
1864 " force the aggressive slicer to preserve function <f>\n"
1865 " --aggressive-slice-preserve-function containing <f>\n"
1866 " force the aggressive slicer to preserve all functions with names containing <f>\n"
1867 "--aggressive-slice-preserve-all-direct-paths \n"
1868 " force aggressive slicer to preserve all direct paths\n"
1870 "Further transformations:\n"
1871 " --constant-propagator propagate constants and simplify expressions\n"
1872 " --inline perform full inlining\n"
1873 " --partial-inline perform partial inlining\n"
1874 " --function-inline <function> transitively inline all calls <function> makes\n"
1875 " --no-caching disable caching of intermediate results during transitive function inlining\n"
1876 " --log <file> log in json format which code segments were inlined, use with --function-inline\n"
1877 " --remove-function-pointers replace function pointers by case statement over function calls\n"
1878 " --value-set-fi-fp-removal build flow-insensitive value set and replace function pointers by a case statement\n"
1879 " over the possible assignments. If the set of possible assignments is empty the function pointer\n"
1880 " is removed using the standard remove-function-pointers pass. \n"
1884 " --add-library add models of C library functions\n"
1885 " --model-argc-argv <n> model up to <n> command line arguments\n"
1887 " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1890 "Function contracts and invariants:\n"
1897 " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n"
1898 " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n"
1899 " --harness with --dump-c/--dump-cpp: include input generator in output\n"
1900 " --version show version and exit\n"
1902 " --xml-ui use XML-formatted output\n"
1903 " --json-ui use JSON-formatted output\n"
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
virtual bool isset(char option) const
void print_global_state_size(const goto_modelt &goto_model)
virtual void help()
display command line help
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()
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.
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 parse_unwindset(const std::string &unwindset)
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.
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
#define FLAG_REPLACE_ALL_CALLS
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)
#define FLAG_ENFORCE_ALL_CONTRACTS
Weak Memory Instrumentation for Threaded Goto Programs.
Insert final assert false into a function.
#define HELP_ENFORCE_CONTRACT
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
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.
Single-entry, single-exit region analysis.
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
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
bool enforce_contracts(const std::set< std::string > &)
Turn requires & ensures into assumptions and assertions for each of the named functions.
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.
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)
virtual int doit()
invoke main modules
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 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
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.
#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)
#define FLAG_ENFORCE_CONTRACT
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Local safe pointer analysis.
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)
Inline all function calls made from a particular function.
Value Set Propagation (flow insensitive)
void register_languages()
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
#define HELP_REPLACE_ALL_CALLS
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
#define HELP_REPLACE_CALL
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 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 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.
#define forall_goto_functions(it, functions)
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.
bool replace_calls(const std::set< std::string > &)
Replace all calls to each function in the list with that function's contract.
Initialize command line arguments.
void function_exit(goto_modelt &goto_model, const irep_idt &id)
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.
Goto Programs with Functions.
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)
#define HELP_ENFORCE_ALL_CONTRACTS
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
#define FLAG_REPLACE_CALL
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)
Field-insensitive, location-sensitive, over-approximative escape analysis.
#define HELP_NONDET_VOLATILE