143 const bool validate_only =
cmdline.
isset(
"validate-goto-binary");
145 if(validate_only ||
cmdline.
isset(
"validate-goto-model"))
166 bool unwindset_file_given=
cmdline.
isset(
"unwindset-file");
168 if(unwindset_given && unwindset_file_given)
169 throw "only one of --unwindset and --unwindset-file supported at a "
172 if(unwind_given || unwindset_given || unwindset_file_given)
179 if(unwindset_file_given)
185 bool unwinding_assertions=
cmdline.
isset(
"unwinding-assertions");
187 bool continue_as_loops=
cmdline.
isset(
"continue-as-loops");
189 if(unwinding_assertions+partial_loops+continue_as_loops>1)
190 throw "more than one of --unwinding-assertions,--partial-loops,"
191 "--continue-as-loops selected";
196 if(unwinding_assertions)
200 else if(partial_loops)
204 else if(continue_as_loops)
210 goto_unwind(
goto_model, unwindset, unwind_strategy);
215 bool have_file=!filename.empty() && filename!=
"-";
222 std::ofstream of(
widen(filename));
224 std::ofstream of(filename);
227 throw "failed to open file "+filename;
234 std::cout << result <<
'\n';
252 std::cout <<
"////\n";
253 std::cout <<
"//// Function: " << gf_entry.first <<
'\n';
254 std::cout <<
"////\n\n";
261 std::cout <<
"Is threaded: " << (is_threaded(i_it)?
"True":
"False")
328 std::cout <<
">>>>\n";
329 std::cout <<
">>>> " << gf_entry.first <<
'\n';
330 std::cout <<
">>>>\n";
331 local_bitvector_analysis.
output(std::cout, gf_entry.second, ns);
349 local_safe_pointers(gf_entry.second.body);
350 std::cout <<
">>>>\n";
351 std::cout <<
">>>> " << gf_entry.first <<
'\n';
352 std::cout <<
">>>>\n";
354 local_safe_pointers.
output(std::cout, gf_entry.second.body, ns);
358 std::cout, gf_entry.second.body, ns);
376 sese_region_analysis(gf_entry.second.body);
377 std::cout <<
">>>>\n";
378 std::cout <<
">>>> " << gf_entry.first <<
'\n';
379 std::cout <<
">>>>\n";
380 sese_region_analysis.
output(std::cout, gf_entry.second.body, ns);
448 custom_bitvector_analysis.
check(
468 points_to.
output(std::cout);
653 for(
auto const &ins : pair.second.body.instructions)
655 if(ins.get_code().is_not_nil())
657 if(ins.has_condition())
659 log.
status() <<
"[guard] " << ins.get_condition().pretty()
699 const bool is_header =
cmdline.
isset(
"dump-c-type-header");
775 call_graph.
output(std::cout);
791 call_graph.
output(std::cout);
842 log.
status() <<
"Removing calls to functions without a body"
910 "Invalid number of positional arguments passed",
912 "goto-instrument needs one input and one output file, aside from other "
993 if(!result.has_value())
1033 const auto function_pointer_restrictions =
1058 log.
status() <<
"Adding up to " << max_argc <<
" command line arguments"
1138 const std::list<std::pair<std::string, std::string>> contract_flags(
1141 for(
const auto &pair : contract_flags)
1145 log.
error() <<
"Pass at most one of --" << pair.first <<
" and --"
1161 std::set<std::string> to_replace(
1174 std::set<std::string> to_enforce(
1200 else if(
cmdline.
isset(
"remove-const-function-pointers"))
1222 log.
status() <<
"Inlining calls of function '" <<
function <<
"'"
1233 bool have_file=!filename.empty() && filename!=
"-";
1241 std::ofstream of(
widen(filename));
1243 std::ofstream of(filename);
1246 throw "failed to open file "+filename;
1253 std::cout << result <<
'\n';
1274 log.
status() <<
"Removing calls to functions without a body"
1299 c_object_factory_options);
1303 object_factory_parameters,
1308 *generate_implementation,
1318 c_object_factory_options);
1320 auto options_split =
1322 if(options_split.size() < 2)
1324 "not enough arguments for this option",
"--generate-havocing-body"};
1326 if(options_split.size() == 2)
1329 std::string{
"havoc,"} + options_split.back(),
1330 object_factory_parameters,
1334 std::regex(options_split[0]),
1335 *generate_implementation,
1342 for(
size_t i = 1; i + 1 < options_split.size(); i += 2)
1345 std::string{
"havoc,"} + options_split[i + 1],
1346 object_factory_parameters,
1352 *generate_implementation,
1365 log.
status() <<
"Adding checks for uninitialized local variables"
1383 log.
status() <<
"Adding nondeterministic initialization "
1384 "of static/global variables except for "
1385 "the specified ones."
1392 log.
status() <<
"Adding nondeterministic initialization "
1393 "of static/global variables"
1400 log.
status() <<
"Slicing away initializations of unused global variables"
1462 const unsigned max_var=
1465 const unsigned max_po_trans=
1471 log.
status() <<
"Adding weak memory (TSO) Instrumentation"
1477 log.
status() <<
"Adding weak memory (PSO) Instrumentation"
1483 log.
status() <<
"Adding weak memory (RMO) Instrumentation"
1487 else if(mm==
"power")
1489 log.
status() <<
"Adding weak memory (Power) Instrumentation"
1495 log.
error() <<
"Unknown weak memory model '" << mm <<
"'"
1569 if(step_case && base_case)
1570 throw "please specify only one of --step-case and --base-case";
1571 else if(!step_case && !base_case)
1572 throw "please specify one of --step-case and --base-case";
1577 throw "please give k>=1";
1579 log.
status() <<
"Instrumenting k-induction for k=" << k <<
", "
1580 << (base_case ?
"base case" :
"step case") <<
messaget::eom;
1643 log.
status() <<
"Performing a function pointer reachability slice"
1687 log.
status() <<
"Slicing away initializations of unused global variables"
1698 if(
cmdline.
isset(
"aggressive-slice-preserve-function"))
1706 if(
cmdline.
isset(
"aggressive-slice-preserve-functions-containing"))
1711 cmdline.
isset(
"aggressive-slice-preserve-all-direct-paths");
1713 aggressive_slicer.
doit();
1746 " goto-instrument [-?] [-h] [--help] show help\n"
1747 " goto-instrument in out perform instrumentation\n"
1750 " --document-properties-html generate HTML property documentation\n"
1751 " --document-properties-latex generate Latex property documentation\n"
1752 " --dump-c generate C source\n"
1753 " --dump-c-type-header m generate a C header for types local in m\n"
1754 " --dump-cpp generate C++ source\n"
1755 " --dot generate CFG graph in DOT format\n"
1756 " --interpreter do concrete execution\n"
1759 " --show-loops show the loops in the program\n"
1761 " --show-symbol-table show loaded symbol table\n"
1762 " --list-symbols list symbols with type information\n"
1765 " --drop-unused-functions drop functions trivially unreachable from main function\n"
1766 " --print-internal-representation\n"
1767 " show verbose internal representation of the program\n"
1768 " --list-undefined-functions list functions without body\n"
1769 " --show-struct-alignment show struct members that might be concurrently accessed\n"
1770 " --show-natural-loops show natural loop heads\n"
1772 " --list-calls-args list all function calls with their arguments\n"
1773 " --call-graph show graph of function calls\n"
1775 " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1778 " --show-threaded show instructions that may be executed by more than one thread\n"
1779 " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n"
1780 " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n"
1781 " *and* used as a dereference operand\n"
1784 " --validate-goto-binary check the well-formedness of the passed in goto\n"
1785 " binary and then exit\n"
1788 " --no-assertions ignore user assertions\n"
1790 " --uninitialized-check add checks for uninitialized locals (experimental)\n"
1791 " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n"
1792 " --race-check add floating-point data race checks\n"
1794 "Semantic transformations:\n"
1796 " --unwind <n> unwinds the loops <n> times\n"
1797 " --unwindset L:B,... unwind loop L with a bound of B\n"
1798 " --unwindset-file <file> read unwindset from file\n"
1799 " --partial-loops permit paths with partial loops\n"
1800 " --unwinding-assertions generate unwinding assertions\n"
1801 " --continue-as-loops add loop for remaining iterations after unwound part\n"
1802 " --isr <function> instruments an interrupt service routine\n"
1803 " --mmio instruments memory-mapped I/O\n"
1804 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1805 " --nondet-static-exclude e same as nondet-static except for the variable e\n"
1806 " (use multiple times if required)\n"
1807 " --check-invariant function instruments invariant checking function\n"
1808 " --remove-pointers converts pointer arithmetic to base+offset expressions\n"
1809 " --splice-call caller,callee prepends a call to callee in the body of caller\n"
1810 " --undefined-function-is-assume-false\n"
1812 " convert each call to an undefined function to assume(false)\n"
1817 "Loop transformations:\n"
1818 " --k-induction <k> check loops with k-induction\n"
1819 " --step-case k-induction: do step-case\n"
1820 " --base-case k-induction: do base-case\n"
1821 " --havoc-loops over-approximate all loops\n"
1822 " --accelerate add loop accelerators\n"
1823 " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n"
1825 "Memory model instrumentations:\n"
1826 " --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1827 " --scc detects critical cycles per SCC (one thread per SCC)\n"
1828 " --one-event-per-cycle only instruments one event per cycle\n"
1829 " --minimum-interference instruments an optimal number of events\n"
1830 " --my-events only instruments events whose ids appear in inst.evt\n"
1831 " --cfg-kill enables symbolic execution used to reduce spurious cycles\n"
1832 " --no-dependencies no dependency analysis\n"
1834 " --no-po-rendering no representation of the threads in the dot\n"
1835 " --render-cluster-file clusterises the dot by files\n"
1836 " --render-cluster-function clusterises the dot by functions\n"
1840 " --full-slice slice away instructions that don't affect assertions\n"
1841 " --property id slice with respect to specific property only\n"
1842 " --slice-global-inits slice away initializations of unused global variables\n"
1843 " --aggressive-slice remove bodies of any functions not on the shortest path between\n"
1844 " the start function and the function containing the property(s)\n"
1845 " --aggressive-slice-call-depth <n>\n"
1846 " used with aggressive-slice, preserves all functions within <n> function calls\n"
1847 " of the functions on the shortest path\n"
1848 " --aggressive-slice-preserve-function <f>\n"
1849 " force the aggressive slicer to preserve function <f>\n"
1850 " --aggressive-slice-preserve-function containing <f>\n"
1851 " force the aggressive slicer to preserve all functions with names containing <f>\n"
1852 "--aggressive-slice-preserve-all-direct-paths \n"
1853 " force aggressive slicer to preserve all direct paths\n"
1855 "Further transformations:\n"
1856 " --constant-propagator propagate constants and simplify expressions\n"
1857 " --inline perform full inlining\n"
1858 " --partial-inline perform partial inlining\n"
1859 " --function-inline <function> transitively inline all calls <function> makes\n"
1860 " --no-caching disable caching of intermediate results during transitive function inlining\n"
1861 " --log <file> log in json format which code segments were inlined, use with --function-inline\n"
1862 " --remove-function-pointers replace function pointers by case statement over function calls\n"
1863 " --value-set-fi-fp-removal build flow-insensitive value set and replace function pointers by a case statement\n"
1864 " over the possible assignments. If the set of possible assignments is empty the function pointer\n"
1865 " is removed using the standard remove-function-pointers pass. \n"
1869 " --add-library add models of C library functions\n"
1870 " --model-argc-argv <n> model up to <n> command line arguments\n"
1872 " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1883 " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n"
1884 " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n"
1885 " --harness with --dump-c/--dump-cpp: include input generator in output\n"
1886 " --version show version and exit\n"
1888 " --xml-ui use XML-formatted output\n"
1889 " --json-ui use JSON-formatted output\n"
void 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
const std::list< std::string > & get_values(const std::string &option) const
bool replace_calls(const std::set< std::string > &functions)
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 &)
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.
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
message_handlert & get_message_handler()
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
void parse_unwind(const std::string &unwind)
void parse_unwindset(const std::list< std::string > &unwindset)
void parse_unwindset_file(const std::string &file_name)
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_REPLACE_CALL
#define FLAG_REPLACE_ALL_CALLS
#define FLAG_REPLACE_CALL
#define FLAG_ENFORCE_CONTRACT
#define HELP_ENFORCE_ALL_CONTRACTS
#define HELP_LOOP_CONTRACTS
#define FLAG_LOOP_CONTRACTS
#define HELP_ENFORCE_CONTRACT
#define HELP_REPLACE_ALL_CALLS
#define FLAG_ENFORCE_ALL_CONTRACTS
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)
Documentation of 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)
Dump C from Goto Program.
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)
#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.
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, unsigned max_argc, message_handlert &message_handler)
Set up argv with up to max_argc pointers into an array of 4096 bytes.
Initialize command line arguments.
Compute natural loops in a goto_function.
void show_natural_loops(const goto_modelt &goto_model, 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.
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 restrict_function_pointers(goto_modelt &goto_model, const function_pointer_restrictionst &restrictions)
Apply function pointer restrictions to a goto_model.
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
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)
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)
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)
Detection for Uninitialized Local Variables.
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)
Weak Memory Instrumentation for Threaded Goto Programs.
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.