136 const bool validate_only =
cmdline.
isset(
"validate-goto-binary");
138 if(validate_only ||
cmdline.
isset(
"validate-goto-model"))
159 bool unwindset_file_given=
cmdline.
isset(
"unwindset-file");
161 if(unwindset_given && unwindset_file_given)
162 throw "only one of --unwindset and --unwindset-file supported at a "
165 if(unwind_given || unwindset_given || unwindset_file_given)
172 if(unwindset_file_given)
174 unwindset.parse_unwindset_file(
180 unwindset.parse_unwindset(
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: " << gf_entry.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 <<
">>>> " << gf_entry.first <<
'\n';
329 std::cout <<
">>>>\n";
330 local_bitvector_analysis.
output(std::cout, gf_entry.second, ns);
348 local_safe_pointers(gf_entry.second.body);
349 std::cout <<
">>>>\n";
350 std::cout <<
">>>> " << gf_entry.first <<
'\n';
351 std::cout <<
">>>>\n";
353 local_safe_pointers.
output(std::cout, gf_entry.second.body, ns);
357 std::cout, gf_entry.second.body, ns);
375 sese_region_analysis(gf_entry.second.body);
376 std::cout <<
">>>>\n";
377 std::cout <<
">>>> " << gf_entry.first <<
'\n';
378 std::cout <<
">>>>\n";
379 sese_region_analysis.
output(std::cout, gf_entry.second.body, ns);
447 custom_bitvector_analysis.
check(
467 points_to.
output(std::cout);
652 for(
auto const &ins : pair.second.body.instructions)
654 if(ins.get_code().is_not_nil())
656 if(ins.has_condition())
658 log.
status() <<
"[guard] " << ins.get_condition().pretty()
698 const bool is_header =
cmdline.
isset(
"dump-c-type-header");
774 call_graph.
output(std::cout);
790 call_graph.
output(std::cout);
841 log.
status() <<
"Removing calls to functions without a body"
909 "Invalid number of positional arguments passed",
911 "goto-instrument needs one input and one output file, aside from other "
992 if(!result.has_value())
1052 std::list<std::string> argv;
1053 argv.resize(max_argc);
1055 log.
status() <<
"Adding up to " << max_argc <<
" command line arguments"
1068 std::stringstream ss;
1070 std::string sep =
"";
1071 for(
auto const &arg : argv)
1073 ss << sep <<
"\"" << arg <<
"\"";
1079 log.
status() <<
"Adding " << argc <<
" arguments: " << ss.str()
1168 std::set<std::string> to_replace(
1172 std::set<std::string> to_enforce(
1198 else if(
cmdline.
isset(
"remove-const-function-pointers"))
1220 log.
status() <<
"Inlining calls of function '" <<
function <<
"'"
1231 bool have_file=!filename.empty() && filename!=
"-";
1239 std::ofstream of(
widen(filename));
1241 std::ofstream of(filename);
1244 throw "failed to open file "+filename;
1251 std::cout << result <<
'\n';
1272 log.
status() <<
"Removing calls to functions without a body"
1297 c_object_factory_options);
1301 object_factory_parameters,
1306 *generate_implementation,
1316 c_object_factory_options);
1318 auto options_split =
1320 if(options_split.size() < 2)
1322 "not enough arguments for this option",
"--generate-havocing-body"};
1324 if(options_split.size() == 2)
1327 std::string{
"havoc,"} + options_split.back(),
1328 object_factory_parameters,
1332 std::regex(options_split[0]),
1333 *generate_implementation,
1340 for(
size_t i = 1; i + 1 < options_split.size(); i += 2)
1343 std::string{
"havoc,"} + options_split[i + 1],
1344 object_factory_parameters,
1350 *generate_implementation,
1363 log.
status() <<
"Adding checks for uninitialized local variables"
1382 log.
status() <<
"Adding nondeterministic initialization "
1383 "of static/global variables except for "
1384 "the specified ones."
1391 log.
status() <<
"Adding nondeterministic initialization "
1392 "of static/global variables"
1399 log.
status() <<
"Slicing away initializations of unused global variables"
1461 const unsigned max_var=
1464 const unsigned max_po_trans=
1470 log.
status() <<
"Adding weak memory (TSO) Instrumentation"
1476 log.
status() <<
"Adding weak memory (PSO) Instrumentation"
1482 log.
status() <<
"Adding weak memory (RMO) Instrumentation"
1486 else if(mm==
"power")
1488 log.
status() <<
"Adding weak memory (Power) Instrumentation"
1494 log.
error() <<
"Unknown weak memory model '" << mm <<
"'"
1568 if(step_case && base_case)
1569 throw "please specify only one of --step-case and --base-case";
1570 else if(!step_case && !base_case)
1571 throw "please specify one of --step-case and --base-case";
1576 throw "please give k>=1";
1578 log.
status() <<
"Instrumenting k-induction for k=" << k <<
", "
1579 << (base_case ?
"base case" :
"step case") <<
messaget::eom;
1642 log.
status() <<
"Performing a function pointer reachability slice"
1686 log.
status() <<
"Slicing away initializations of unused global variables"
1697 if(
cmdline.
isset(
"aggressive-slice-preserve-function"))
1705 if(
cmdline.
isset(
"aggressive-slice-preserve-functions-containing"))
1710 cmdline.
isset(
"aggressive-slice-preserve-all-direct-paths");
1712 aggressive_slicer.
doit();
1745 " goto-instrument [-?] [-h] [--help] show help\n"
1746 " goto-instrument in out perform instrumentation\n"
1750 " --dot generate CFG graph in DOT format\n"
1751 " --interpreter do concrete execution\n"
1758 " --show-symbol-table show loaded symbol table\n"
1759 " --list-symbols list symbols with type information\n"
1762 " --drop-unused-functions drop functions trivially unreachable from main function\n"
1763 " --print-internal-representation\n"
1764 " show verbose internal representation of the program\n"
1765 " --list-undefined-functions list functions without body\n"
1766 " --show-struct-alignment show struct members that might be concurrently accessed\n"
1767 " --show-natural-loops show natural loop heads\n"
1769 " --list-calls-args list all function calls with their arguments\n"
1770 " --call-graph show graph of function calls\n"
1772 " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1775 " --show-threaded show instructions that may be executed by more than one thread\n"
1776 " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n"
1777 " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n"
1778 " *and* used as a dereference operand\n"
1781 " --validate-goto-binary check the well-formedness of the passed in goto\n"
1782 " binary and then exit\n"
1785 " --no-assertions ignore user assertions\n"
1788 " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n"
1789 " --race-check add floating-point data race checks\n"
1791 "Semantic transformations:\n"
1794 " --unwindset-file <file> read unwindset from file\n"
1795 " --partial-loops permit paths with partial loops\n"
1796 " --unwinding-assertions generate unwinding assertions\n"
1797 " --continue-as-loops add loop for remaining iterations after unwound part\n"
1798 " --isr <function> instruments an interrupt service routine\n"
1799 " --mmio instruments memory-mapped I/O\n"
1800 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1801 " --nondet-static-exclude e same as nondet-static except for the variable e\n"
1802 " (use multiple times if required)\n"
1803 " --check-invariant function instruments invariant checking function\n"
1805 " --splice-call caller,callee prepends a call to callee in the body of caller\n"
1806 " --undefined-function-is-assume-false\n"
1808 " convert each call to an undefined function to assume(false)\n"
1813 "Loop transformations:\n"
1814 " --k-induction <k> check loops with k-induction\n"
1815 " --step-case k-induction: do step-case\n"
1816 " --base-case k-induction: do base-case\n"
1817 " --havoc-loops over-approximate all loops\n"
1818 " --accelerate add loop accelerators\n"
1819 " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n"
1821 "Memory model instrumentations:\n"
1826 " --full-slice slice away instructions that don't affect assertions\n"
1827 " --property id slice with respect to specific property only\n"
1828 " --slice-global-inits slice away initializations of unused global variables\n"
1829 " --aggressive-slice remove bodies of any functions not on the shortest path between\n"
1830 " the start function and the function containing the property(s)\n"
1831 " --aggressive-slice-call-depth <n>\n"
1832 " used with aggressive-slice, preserves all functions within <n> function calls\n"
1833 " of the functions on the shortest path\n"
1834 " --aggressive-slice-preserve-function <f>\n"
1835 " force the aggressive slicer to preserve function <f>\n"
1836 " --aggressive-slice-preserve-function containing <f>\n"
1837 " force the aggressive slicer to preserve all functions with names containing <f>\n"
1838 "--aggressive-slice-preserve-all-direct-paths \n"
1839 " force aggressive slicer to preserve all direct paths\n"
1841 "Further transformations:\n"
1842 " --constant-propagator propagate constants and simplify expressions\n"
1843 " --inline perform full inlining\n"
1844 " --partial-inline perform partial inlining\n"
1845 " --function-inline <function> transitively inline all calls <function> makes\n"
1846 " --no-caching disable caching of intermediate results during transitive function inlining\n"
1847 " --log <file> log in json format which code segments were inlined, use with --function-inline\n"
1848 " --remove-function-pointers replace function pointers by case statement over function calls\n"
1849 " --value-set-fi-fp-removal build flow-insensitive value set and replace function pointers by a case statement\n"
1850 " over the possible assignments. If the set of possible assignments is empty the function pointer\n"
1851 " is removed using the standard remove-function-pointers pass. \n"
1855 " --add-library add models of C library functions\n"
1859 " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1868 " --version show version and exit\n"
1870 " --xml output files in XML where supported\n"
1871 " --xml-ui use XML-formatted output\n"
1872 " --json-ui use JSON-formatted output\n"
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
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 print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
#define HELP_ANSI_C_LANGUAGE
void branch(goto_modelt &goto_model, const irep_idt &id)
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
void check_call_sequence(const goto_modelt &goto_model)
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
Memory-mapped I/O Instrumentation for Goto Programs.
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
#define HELP_SHOW_CLASS_HIERARCHY
The aggressive slicer removes the body of all the functions except those on the shortest path,...
std::list< std::string > user_specified_properties
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
std::list< std::string > name_snippets
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.
bool preserve_all_direct_paths
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
void output_dot(std::ostream &out) const
void output(std::ostream &out) const
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
void output_xml(std::ostream &out) const
Non-graph-based representation of the class hierarchy.
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
std::string get_value(char option) const
virtual bool isset(char option) const
std::list< std::string > get_comma_separated_values(const char *option) const
Collect all occurrences of option option and split their values on each comma, merging them into a si...
const std::list< std::string > & get_values(const std::string &option) const
bool replace_calls(const std::set< std::string > &)
Replace all calls to each function in the list with that function's contract.
void apply_loop_contracts()
bool enforce_contracts(const std::set< std::string > &functions)
Turn requires & ensures into assumptions and assertions for each of the named functions.
void set_from_symbol_table(const symbol_tablet &)
bool set(const cmdlinet &cmdline)
struct configt::ansi_ct ansi_c
void check(const goto_modelt &, bool xml, std::ostream &)
void instrument(goto_modelt &)
This is a may analysis (i.e.
void compute_loop_numbers()
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void register_languages() override
void help() override
display command line help
void instrument_goto_program()
void do_indirect_call_and_rtti_removal(bool force=false)
bool partial_inlining_done
bool function_pointer_removal_done
void do_partial_inlining()
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
int doit() override
invoke main modules
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.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
jsont output_log_json() const
void output_dot(std::ostream &out) const
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
void output_safe_dereferences(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output safely dereferenced expressions per instruction in human-readable format.
void output(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output non-null expressions per instruction in human-readable format.
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.
mstreamt & status() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
void set_option(const std::string &option, const bool value)
ui_message_handlert ui_message_handler
void output(std::ostream &out) const
void output(std::ostream &out, const goto_programt &goto_program, const namespacet &ns) const
Expression to hold a symbol (variable)
typet type
Type of symbol.
irep_idt name
The unique identifier.
virtual uit get_ui() const
This template class implements a data-flow analysis which keeps track of what values different variab...
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Encoding for Threaded Goto Programs.
#define HELP_CONFIG_LIBRARY
#define HELP_REPLACE_CALL
#define FLAG_REPLACE_CALL
#define FLAG_ENFORCE_CONTRACT
#define HELP_LOOP_CONTRACTS
#define FLAG_LOOP_CONTRACTS
#define HELP_ENFORCE_CONTRACT
void count_eloc(const goto_modelt &goto_model)
void print_global_state_size(const goto_modelt &goto_model)
void print_path_lengths(const goto_modelt &goto_model)
void list_eloc(const goto_modelt &goto_model)
#define HELP_GOTO_PROGRAM_STATS
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Field-insensitive, location-sensitive bitvector analysis.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
#define HELP_DOCUMENT_PROPERTIES
void dot(const goto_modelt &src, std::ostream &out)
Dump Goto-Program as DOT Graph.
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
void 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 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)
bool ensure_one_backedge_per_target(goto_programt::targett &it, goto_programt &goto_program)
Ensure one backedge per target.
Field-insensitive, location-sensitive, over-approximative escape analysis.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_CONVERSION_FAILED
Failure to convert / write to another format.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void function_exit(goto_modelt &goto_model, const irep_idt &id)
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Function Entering and Exiting.
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 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-...
#define HELP_REPLACE_FUNCTION_BODY
Field-insensitive, location-sensitive, over-approximative escape analysis.
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Inline every function call into the entry_point() function.
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 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...
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
#define forall_goto_program_instructions(it, program)
void remove_pointers(goto_modelt &goto_model, value_setst &value_sets)
Remove dereferences in all expressions contained in the program goto_model.
#define HELP_REMOVE_POINTERS
void havoc_loops(goto_modelt &goto_model)
void horn_encoding(const goto_modelt &, std::ostream &)
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...
Insert final assert false into a function.
#define HELP_INSERT_FINAL_ASSERT_FALSE
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
Interpreter for GOTO Programs.
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)
Interrupt Instrumentation for Goto Programs.
void interval_analysis(goto_modelt &goto_model)
Initialises the abstract interpretation over interval domain and instruments instructions using inter...
Over-approximate Concurrency for Threaded Goto Programs.
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
void label_function_pointer_call_sites(goto_modelt &goto_model)
This ensures that call instructions can be only one of two things:
Label function pointer call sites across a goto model.
Compute lexical loops in a goto_function.
void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
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.
Field-insensitive, location-sensitive bitvector analysis.
Local safe pointer analysis.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
static void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program)
Memory-mapped I/O Instrumentation for Goto Programs.
bool model_argc_argv(goto_modelt &goto_model, const std::list< std::string > &argv_args, bool model_argv, message_handlert &message_handler)
Set up argv to user-specified values (when model_argv is FALSE) or (when model_argv is TRUE) set up a...
Compute natural loops in a goto_function.
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
static void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
void nondet_volatile(goto_modelt &goto_model, const optionst &options)
Havoc reads from volatile expressions, if enabled in the options.
#define HELP_NONDET_VOLATILE
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
Add parameter assignments.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
Field-sensitive, location-insensitive points-to analysis.
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)
Race Detection for Threaded Goto Programs.
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 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.
#define HELP_REACHABILITY_SLICER
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
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 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...
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
Remove calls to functions without a body.
#define HELP_REMOVE_CALLS_NO_BODY
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
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...
Remove function definition.
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)
Remove Indirect Function Calls.
void restore_returns(goto_modelt &goto_model)
restores return statements
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Replace function returns by assignments to global variables.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
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...
Functions for replacing virtual function call with a static function calls in functions,...
#define HELP_REPLACE_CALLS
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
void restrict_function_pointers(message_handlert &message_handler, goto_modelt &goto_model, const optionst &options)
Apply function pointer restrictions to a goto_model.
Given goto functions and a list of function parameters or globals that are function pointers with lis...
#define RESTRICT_FUNCTION_POINTER_OPT
#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
#define HELP_RESTRICT_FUNCTION_POINTER
#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Race Detection for Threaded Goto Programs.
Single-entry, single-exit region analysis.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
#define HELP_SHOW_GOTO_FUNCTIONS
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)
void show_value_sets(ui_message_handlert::uit ui, const goto_modelt &goto_model, const value_set_analysist &value_set_analysis)
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
Skip over selected loops by adding gotos.
void slice_global_inits(goto_modelt &goto_model, message_handlert &message_handler)
Remove initialization of global variables that are not used in any function reachable from the entry ...
Remove initializations of unused global variables.
bool splice_call(goto_functionst &goto_functions, const std::string &callercallee, const symbol_tablet &symbol_table, message_handlert &message_handler)
Harnessing for goto functions.
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
static void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
unsigned safe_string2unsigned(const std::string &str, int base)
unsigned unsafe_string2unsigned(const std::string &str, int base)
std::size_t safe_string2size_t(const std::string &str, int base)
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_functionst &dest)
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
std::list< std::string > defines
This is unused by this implementation of guards, but can be used by other implementations of the same...
void thread_exit_instrumentation(goto_programt &goto_program)
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
void list_undefined_functions(const goto_modelt &goto_model, std::ostream &os)
void undefined_function_abort_path(goto_modelt &goto_model)
Handling of functions without body.
std::wstring widen(const char *s)
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
#define HELP_UNINITIALIZED_CHECK
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...
flow insensitive value set function pointer removal
const char * CBMC_VERSION
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)
instrumentation_strategyt
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.