Go to the documentation of this file.
139 const bool validate_only =
cmdline.
isset(
"validate-goto-binary");
141 if(validate_only ||
cmdline.
isset(
"validate-goto-model"))
162 bool unwindset_file_given=
cmdline.
isset(
"unwindset-file");
164 if(unwindset_given && unwindset_file_given)
165 throw "only one of --unwindset and --unwindset-file supported at a "
168 if(unwind_given || unwindset_given || unwindset_file_given)
175 if(unwindset_file_given)
181 bool unwinding_assertions=
cmdline.
isset(
"unwinding-assertions");
183 bool continue_as_loops=
cmdline.
isset(
"continue-as-loops");
185 if(unwinding_assertions+partial_loops+continue_as_loops>1)
186 throw "more than one of --unwinding-assertions,--partial-loops,"
187 "--continue-as-loops selected";
192 if(unwinding_assertions)
196 else if(partial_loops)
200 else if(continue_as_loops)
206 goto_unwind(
goto_model, unwindset, unwind_strategy);
211 bool have_file=!filename.empty() && filename!=
"-";
218 std::ofstream of(
widen(filename));
220 std::ofstream of(filename);
223 throw "failed to open file "+filename;
230 std::cout << result <<
'\n';
248 std::cout <<
"////\n";
249 std::cout <<
"//// Function: " << f_it->first <<
'\n';
250 std::cout <<
"////\n\n";
257 std::cout <<
"Is threaded: " << (is_threaded(i_it)?
"True":
"False")
324 std::cout <<
">>>>\n";
325 std::cout <<
">>>> " << it->first <<
'\n';
326 std::cout <<
">>>>\n";
327 local_bitvector_analysis.
output(std::cout, it->second, ns);
345 local_safe_pointers(it->second.body);
346 std::cout <<
">>>>\n";
347 std::cout <<
">>>> " << it->first <<
'\n';
348 std::cout <<
">>>>\n";
350 local_safe_pointers.
output(std::cout, it->second.body, ns);
354 std::cout, it->second.body, ns);
372 sese_region_analysis(it->second.body);
373 std::cout <<
">>>>\n";
374 std::cout <<
">>>> " << it->first <<
'\n';
375 std::cout <<
">>>>\n";
376 sese_region_analysis.
output(std::cout, it->second.body, ns);
444 custom_bitvector_analysis.
check(
464 points_to.
output(std::cout);
646 for(
auto const &ins : pair.second.body.instructions)
648 if(ins.code.is_not_nil())
650 if(ins.has_condition())
652 log.
status() <<
"[guard] " << ins.get_condition().pretty()
692 const bool is_header =
cmdline.
isset(
"dump-c-type-header");
768 call_graph.
output(std::cout);
784 call_graph.
output(std::cout);
835 log.
status() <<
"Removing calls to functions without a body"
903 "Invalid number of positional arguments passed",
905 "goto-instrument needs one input and one output file, aside from other "
986 if(!result.has_value())
1006 options.
set_option(
"assert-to-assume",
true);
1008 options.
set_option(
"assert-to-assume",
false);
1053 log.
status() <<
"Adding up to " << max_argc <<
" command line arguments"
1145 else if(
cmdline.
isset(
"remove-const-function-pointers"))
1167 log.
status() <<
"Inlining calls of function '" <<
function <<
"'"
1178 bool have_file=!filename.empty() && filename!=
"-";
1186 std::ofstream of(
widen(filename));
1188 std::ofstream of(filename);
1191 throw "failed to open file "+filename;
1198 std::cout << result <<
'\n';
1219 log.
status() <<
"Removing calls to functions without a body"
1244 c_object_factory_options);
1248 object_factory_parameters,
1253 *generate_implementation,
1263 c_object_factory_options);
1265 auto options_split =
1267 if(options_split.size() < 2)
1269 "not enough arguments for this option",
"--generate-havocing-body"};
1271 if(options_split.size() == 2)
1274 std::string{
"havoc,"} + options_split.back(),
1275 object_factory_parameters,
1279 std::regex(options_split[0]),
1280 *generate_implementation,
1287 for(
size_t i = 1; i + 1 < options_split.size(); i += 2)
1290 std::string{
"havoc,"} + options_split[i + 1],
1291 object_factory_parameters,
1297 *generate_implementation,
1310 log.
status() <<
"Adding checks for uninitialized local variables"
1328 log.
status() <<
"Adding nondeterministic initialization "
1329 "of static/global variables except for "
1330 "the specified ones."
1337 log.
status() <<
"Adding nondeterministic initialization "
1338 "of static/global variables"
1345 log.
status() <<
"Slicing away initializations of unused global variables"
1407 const unsigned max_var=
1410 const unsigned max_po_trans=
1416 log.
status() <<
"Adding weak memory (TSO) Instrumentation"
1422 log.
status() <<
"Adding weak memory (PSO) Instrumentation"
1428 log.
status() <<
"Adding weak memory (RMO) Instrumentation"
1432 else if(mm==
"power")
1434 log.
status() <<
"Adding weak memory (Power) Instrumentation"
1440 log.
error() <<
"Unknown weak memory model '" << mm <<
"'"
1514 if(step_case && base_case)
1515 throw "please specify only one of --step-case and --base-case";
1516 else if(!step_case && !base_case)
1517 throw "please specify one of --step-case and --base-case";
1522 throw "please give k>=1";
1524 log.
status() <<
"Instrumenting k-induction for k=" << k <<
", "
1525 << (base_case ?
"base case" :
"step case") <<
messaget::eom;
1569 log.
status() <<
"Making volatile variables non-deterministic"
1594 log.
status() <<
"Performing a function pointer reachability slice"
1638 log.
status() <<
"Slicing away initializations of unused global variables"
1649 if(
cmdline.
isset(
"aggressive-slice-preserve-function"))
1657 if(
cmdline.
isset(
"aggressive-slice-preserve-functions-containing"))
1662 cmdline.
isset(
"aggressive-slice-preserve-all-direct-paths");
1664 aggressive_slicer.
doit();
1697 " goto-instrument [-?] [-h] [--help] show help\n"
1698 " goto-instrument in out perform instrumentation\n"
1701 " --document-properties-html generate HTML property documentation\n"
1702 " --document-properties-latex generate Latex property documentation\n"
1703 " --dump-c generate C source\n"
1704 " --dump-c-type-header m generate a C header for types local in m\n"
1705 " --dump-cpp generate C++ source\n"
1706 " --dot generate CFG graph in DOT format\n"
1707 " --interpreter do concrete execution\n"
1710 " --show-loops show the loops in the program\n"
1712 " --show-symbol-table show loaded symbol table\n"
1713 " --list-symbols list symbols with type information\n"
1716 " --drop-unused-functions drop functions trivially unreachable from main function\n"
1717 " --print-internal-representation\n"
1718 " show verbose internal representation of the program\n"
1719 " --list-undefined-functions list functions without body\n"
1720 " --show-struct-alignment show struct members that might be concurrently accessed\n"
1721 " --show-natural-loops show natural loop heads\n"
1723 " --list-calls-args list all function calls with their arguments\n"
1724 " --call-graph show graph of function calls\n"
1726 " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1729 " --show-threaded show instructions that may be executed by more than one thread\n"
1730 " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n"
1731 " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n"
1732 " *and* used as a dereference operand\n"
1735 " --validate-goto-binary check the well-formedness of the passed in goto\n"
1736 " binary and then exit\n"
1739 " --no-assertions ignore user assertions\n"
1741 " --uninitialized-check add checks for uninitialized locals (experimental)\n"
1742 " --error-label label check that label is unreachable\n"
1743 " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n"
1744 " --race-check add floating-point data race checks\n"
1746 "Semantic transformations:\n"
1747 " --nondet-volatile makes reads from volatile variables non-deterministic\n"
1748 " --unwind <n> unwinds the loops <n> times\n"
1749 " --unwindset L:B,... unwind loop L with a bound of B\n"
1750 " --unwindset-file <file> read unwindset from file\n"
1751 " --partial-loops permit paths with partial loops\n"
1752 " --unwinding-assertions generate unwinding assertions\n"
1753 " --continue-as-loops add loop for remaining iterations after unwound part\n"
1754 " --isr <function> instruments an interrupt service routine\n"
1755 " --mmio instruments memory-mapped I/O\n"
1756 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1757 " --nondet-static-exclude e same as nondet-static except for the variable e\n"
1758 " (use multiple times if required)\n"
1759 " --check-invariant function instruments invariant checking function\n"
1760 " --remove-pointers converts pointer arithmetic to base+offset expressions\n"
1761 " --splice-call caller,callee prepends a call to callee in the body of caller\n"
1762 " --undefined-function-is-assume-false\n"
1764 " convert each call to an undefined function to assume(false)\n"
1769 "Loop transformations:\n"
1770 " --k-induction <k> check loops with k-induction\n"
1771 " --step-case k-induction: do step-case\n"
1772 " --base-case k-induction: do base-case\n"
1773 " --havoc-loops over-approximate all loops\n"
1774 " --accelerate add loop accelerators\n"
1775 " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n"
1777 "Memory model instrumentations:\n"
1778 " --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1779 " --scc detects critical cycles per SCC (one thread per SCC)\n"
1780 " --one-event-per-cycle only instruments one event per cycle\n"
1781 " --minimum-interference instruments an optimal number of events\n"
1782 " --my-events only instruments events whose ids appear in inst.evt\n"
1783 " --cfg-kill enables symbolic execution used to reduce spurious cycles\n"
1784 " --no-dependencies no dependency analysis\n"
1786 " --no-po-rendering no representation of the threads in the dot\n"
1787 " --render-cluster-file clusterises the dot by files\n"
1788 " --render-cluster-function clusterises the dot by functions\n"
1792 " --full-slice slice away instructions that don't affect assertions\n"
1793 " --property id slice with respect to specific property only\n"
1794 " --slice-global-inits slice away initializations of unused global variables\n"
1795 " --aggressive-slice remove bodies of any functions not on the shortest path between\n"
1796 " the start function and the function containing the property(s)\n"
1797 " --aggressive-slice-call-depth <n>\n"
1798 " used with aggressive-slice, preserves all functions within <n> function calls\n"
1799 " of the functions on the shortest path\n"
1800 " --aggressive-slice-preserve-function <f>\n"
1801 " force the aggressive slicer to preserve function <f>\n"
1802 " --aggressive-slice-preserve-function containing <f>\n"
1803 " force the aggressive slicer to preserve all functions with names containing <f>\n"
1804 "--aggressive-slice-preserve-all-direct-paths \n"
1805 " force aggressive slicer to preserve all direct paths\n"
1807 "Further transformations:\n"
1808 " --constant-propagator propagate constants and simplify expressions\n"
1809 " --inline perform full inlining\n"
1810 " --partial-inline perform partial inlining\n"
1811 " --function-inline <function> transitively inline all calls <function> makes\n"
1812 " --no-caching disable caching of intermediate results during transitive function inlining\n"
1813 " --log <file> log in json format which code segments were inlined, use with --function-inline\n"
1814 " --remove-function-pointers replace function pointers by case statement over function calls\n"
1817 " --add-library add models of C library functions\n"
1818 " --model-argc-argv <n> model up to <n> command line arguments\n"
1820 " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1824 " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n"
1825 " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n"
1826 " --harness with --dump-c/--dump-cpp: include input generator in output\n"
1827 " --version show version and exit\n"
1829 " --xml-ui use XML-formatted output\n"
1830 " --json-ui use JSON-formatted output\n"
const char * CBMC_VERSION
#define HELP_REACHABILITY_SLICER
std::list< std::string > defines
#define HELP_SHOW_GOTO_FUNCTIONS
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.
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)
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)
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
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)
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)
#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...
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...
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
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)
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
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
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)
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)
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)
Given a string s, split into a sequence of substrings when separated by specified delimiter.
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 full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
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)
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)
#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.
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
#define HELP_SHOW_PROPERTIES
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)
void instrument(goto_modelt &)
void slice_global_inits(goto_modelt &goto_model)
void set_from_symbol_table(const symbol_tablet &)
void code_contracts(goto_modelt &goto_model)
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 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)
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.
void remove_functions(goto_modelt &goto_model, const std::list< std::string > &names, message_handlert &message_handler)
Remove the body of all functions listed in "names" such that an analysis will treat it as a side-effe...
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
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,...
goto_functionst goto_functions
GOTO functions.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
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)
void output(std::ostream &out) const
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)
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.
void function_exit(goto_modelt &goto_model, const irep_idt &id)
instrumentation_strategyt
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....
void havoc_loops(goto_modelt &goto_model)
#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)
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)
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
void thread_exit_instrumentation(goto_programt &goto_program)
const std::list< std::string > & get_values(const std::string &option) const
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)
jsont output_log_json() const
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)