107 std::cout << CBMC_VERSION <<
'\n';
131 bool unwindset_file_given=
cmdline.
isset(
"unwindset-file");
133 if(unwindset_given && unwindset_file_given)
134 throw "only one of --unwindset and --unwindset-file supported at a " 137 if(unwind_given || unwindset_given || unwindset_file_given)
144 if(unwindset_file_given)
150 bool unwinding_assertions=
cmdline.
isset(
"unwinding-assertions");
152 bool continue_as_loops=
cmdline.
isset(
"continue-as-loops");
154 if(unwinding_assertions+partial_loops+continue_as_loops>1)
155 throw "more than one of --unwinding-assertions,--partial-loops," 156 "--continue-as-loops selected";
161 if(unwinding_assertions)
165 else if(partial_loops)
169 else if(continue_as_loops)
175 goto_unwind(
goto_model, unwindset, unwind_strategy);
180 bool have_file=!filename.empty() && filename!=
"-";
187 std::ofstream of(
widen(filename));
189 std::ofstream of(filename);
192 throw "failed to open file "+filename;
199 std::cout <<
result <<
'\n';
217 std::cout <<
"////\n";
218 std::cout <<
"//// Function: " << f_it->first <<
'\n';
219 std::cout <<
"////\n\n";
226 std::cout <<
"Is threaded: " << (is_threaded(i_it)?
"True":
"False")
278 std::cout <<
">>>>\n";
279 std::cout <<
">>>> " << it->first <<
'\n';
280 std::cout <<
">>>>\n";
281 local_bitvector_analysis.
output(std::cout, it->second, ns);
349 custom_bitvector_analysis.
check(
369 points_to.
output(std::cout);
504 status() <<
"Starting interpreter" <<
eom;
546 for(
auto const &ins : pair.second.body.instructions)
548 if(ins.code.is_not_nil())
550 if(ins.guard.is_not_nil())
551 status() <<
"[guard] " << ins.guard.pretty() <<
eom;
641 call_graph.
output(std::cout);
657 call_graph.
output(std::cout);
706 status() <<
"Performing full inlining" <<
eom;
709 status() <<
"Removing calls to functions without a body" <<
eom;
721 status() <<
"Horn-clause encoding" <<
eom;
734 error() <<
"Failed to open output file " 751 status() <<
"Removing unused functions" <<
eom;
783 catch(
const std::string &e)
791 error() <<
"Numeric exception : " << e <<
eom;
795 catch(
const std::bad_alloc &)
811 status() <<
"Function Pointer Removal" <<
eom;
816 status() <<
"Virtual function removal" <<
eom;
818 status() <<
"Cleaning inline assembler statements" <<
eom;
834 status() <<
"Removing const function pointers only" <<
eom;
892 options.
set_option(
"assert-to-assume",
false);
923 status() <<
"Adding gotos to skip loops" <<
eom;
939 status() <<
"Adding up to " << max_argc
940 <<
" command line arguments" <<
eom;
986 status() <<
"Performing full inlining" <<
eom;
993 status() <<
"Propagating Constants" <<
eom;
1022 status() <<
"Applying Code Contracts" <<
eom;
1031 else if(
cmdline.
isset(
"remove-const-function-pointers"))
1045 status() <<
"Inlining calls of function `" <<
function <<
"'" <<
eom;
1059 bool have_file=!filename.empty() && filename!=
"-";
1072 std::ofstream of(
widen(filename));
1074 std::ofstream of(filename);
1077 throw "failed to open file "+filename;
1084 std::cout <<
result <<
'\n';
1105 status() <<
"Removing calls to functions without a body" <<
eom;
1118 status() <<
"Propagating Constants" <<
eom;
1130 status() <<
"Adding checks for uninitialized local variables" <<
eom;
1137 status() <<
"Adding check for maximum call stack size" <<
eom;
1147 status() <<
"Adding nondeterministic initialization of static/global " 1154 status() <<
"Slicing away initializations of unused global variables" 1164 status() <<
"String Abstraction" <<
eom;
1193 status() <<
"Adding Race Checks" <<
eom;
1218 const unsigned unwind_loops=
1221 const unsigned max_var=
1224 const unsigned max_po_trans=
1230 status() <<
"Adding weak memory (TSO) Instrumentation" <<
eom;
1235 status() <<
"Adding weak memory (PSO) Instrumentation" <<
eom;
1240 status() <<
"Adding weak memory (RMO) Instrumentation" <<
eom;
1243 else if(mm==
"power")
1245 status() <<
"Adding weak memory (Power) Instrumentation" <<
eom;
1250 error() <<
"Unknown weak memory model `" << mm <<
"'" <<
eom;
1286 status() <<
"Instrumenting interrupt handler" <<
eom;
1296 status() <<
"Instrumenting memory-mapped I/O" <<
eom;
1302 status() <<
"Sequentializing concurrency" <<
eom;
1324 if(step_case && base_case)
1325 throw "please specify only one of --step-case and --base-case";
1326 else if(!step_case && !base_case)
1327 throw "please specify one of --step-case and --base-case";
1332 throw "please give k>=1";
1334 status() <<
"Instrumenting k-induction for k=" << k <<
", " 1335 << (base_case?
"base case":
"step case") <<
eom;
1342 status() <<
"Function enter instrumentation" <<
eom;
1350 status() <<
"Function exit instrumentation" <<
eom;
1358 status() <<
"Branch instrumentation" <<
eom;
1379 status() <<
"Making volatile variables non-deterministic" <<
eom;
1388 status() <<
"Performing a reachability slice" <<
eom;
1401 status() <<
"Performing a full slice" <<
eom;
1411 status() <<
"Performing call splicing" <<
eom;
1429 *generate_implementation,
1442 std::cout <<
'\n' <<
banner_string(
"Goto-Instrument", CBMC_VERSION) <<
'\n' 1444 "* * Copyright (C) 2008-2013 * *\n" 1445 "* * Daniel Kroening * *\n" 1446 "* * kroening@kroening.com * *\n" 1450 " goto-instrument [-?] [-h] [--help] show help\n" 1451 " goto-instrument in out perform instrumentation\n" 1454 " --document-properties-html generate HTML property documentation\n" 1455 " --document-properties-latex generate Latex property documentation\n" 1456 " --dump-c generate C source\n" 1457 " --dump-cpp generate C++ source\n" 1458 " --dot generate CFG graph in DOT format\n" 1459 " --interpreter do concrete execution\n" 1462 " --show-loops show the loops in the program\n" 1464 " --show-symbol-table show loaded symbol table\n" 1465 " --list-symbols list symbols with type information\n" 1468 " --drop-unused-functions drop functions trivially unreachable from main function\n" 1469 " --print-internal-representation\n" 1470 " show verbose internal representation of the program\n" 1471 " --list-undefined-functions list functions without body\n" 1472 " --show-struct-alignment show struct members that might be concurrently accessed\n" 1473 " --show-natural-loops show natural loop heads\n" 1475 " --list-calls-args list all function calls with their arguments\n" 1476 " --call-graph show graph of function calls\n" 1478 " --reachable-call-graph show graph of function calls potentially reachable from main function\n" 1481 " --show-threaded show instructions that may be executed by more than one thread\n" 1484 " --no-assertions ignore user assertions\n" 1486 " --uninitialized-check add checks for uninitialized locals (experimental)\n" 1487 " --error-label label check that label is unreachable\n" 1488 " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" 1489 " --race-check add floating-point data race checks\n" 1491 "Semantic transformations:\n" 1492 " --nondet-volatile makes reads from volatile variables non-deterministic\n" 1493 " --unwind <n> unwinds the loops <n> times\n" 1494 " --unwindset L:B,... unwind loop L with a bound of B\n" 1495 " --unwindset-file <file> read unwindset from file\n" 1496 " --partial-loops permit paths with partial loops\n" 1497 " --unwinding-assertions generate unwinding assertions\n" 1498 " --continue-as-loops add loop for remaining iterations after unwound part\n" 1499 " --isr <function> instruments an interrupt service routine\n" 1500 " --mmio instruments memory-mapped I/O\n" 1501 " --nondet-static add nondeterministic initialization of variables with static lifetime\n" 1502 " --check-invariant function instruments invariant checking function\n" 1503 " --remove-pointers converts pointer arithmetic to base+offset expressions\n" 1504 " --splice-call caller,callee prepends a call to callee in the body of caller\n" 1505 " --undefined-function-is-assume-false\n" 1507 " convert each call to an undefined function to assume(false)\n" 1510 "Loop transformations:\n" 1511 " --k-induction <k> check loops with k-induction\n" 1512 " --step-case k-induction: do step-case\n" 1513 " --base-case k-induction: do base-case\n" 1514 " --havoc-loops over-approximate all loops\n" 1515 " --accelerate add loop accelerators\n" 1516 " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" 1518 "Memory model instrumentations:\n" 1519 " --mm <tso,pso,rmo,power> instruments a weak memory model\n" 1520 " --scc detects critical cycles per SCC (one thread per SCC)\n" 1521 " --one-event-per-cycle only instruments one event per cycle\n" 1522 " --minimum-interference instruments an optimal number of events\n" 1523 " --my-events only instruments events whose ids appear in inst.evt\n" 1524 " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" 1525 " --no-dependencies no dependency analysis\n" 1527 " --no-po-rendering no representation of the threads in the dot\n" 1528 " --render-cluster-file clusterises the dot by files\n" 1529 " --render-cluster-function clusterises the dot by functions\n" 1532 " --reachability-slice slice away instructions that can't reach assertions\n" 1533 " --full-slice slice away instructions that don't affect assertions\n" 1534 " --property id slice with respect to specific property only\n" 1535 " --slice-global-inits slice away initializations of unused global variables\n" 1537 "Further transformations:\n" 1538 " --constant-propagator propagate constants and simplify expressions\n" 1539 " --inline perform full inlining\n" 1540 " --partial-inline perform partial inlining\n" 1541 " --function-inline <function> transitively inline all calls <function> makes\n" 1542 " --no-caching disable caching of intermediate results during transitive function inlining\n" 1543 " --log <file> log in json format which code segments were inlined, use with --function-inline\n" 1544 " --remove-function-pointers replace function pointers by case statement over function calls\n" 1547 " --add-library add models of C library functions\n" 1548 " --model-argc-argv <n> model up to <n> command line arguments\n" 1550 " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n" 1553 " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" 1554 " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" 1555 " --harness with --dump-c/--dump-cpp: include input generator in output\n" 1556 " --version show version and exit\n" 1558 " --xml-ui use XML-formatted output\n" 1559 " --json-ui use JSON-formatted output\n"
void do_indirect_call_and_rtti_removal(bool force=false)
irep_idt name
The unique identifier.
const std::list< std::string > & get_values(const std::string &option) const
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.
Detection for Uninitialized Local Variables.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
struct configt::ansi_ct ansi_c
jsont output_log_json() const
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...
Field-insensitive, location-sensitive bitvector analysis.
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
Function Entering and Exiting.
Over-approximate Concurrency for Threaded Goto Programs.
void undefined_function_abort_path(goto_modelt &goto_model)
Skip over selected loops by adding gotos.
Remove initializations of unused global variables.
Initialize command line arguments.
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
Remove Indirect Function Calls.
std::wstring widen(const char *s)
instrumentation_strategyt
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Remove Virtual Function (Method) Calls.
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
void remove_pointers(goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)
void list_undefined_functions(const goto_modelt &goto_model, std::ostream &os)
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
Field-sensitive, location-insensitive points-to analysis.
unsigned unsafe_string2unsigned(const std::string &str, int base)
void compute_loop_numbers()
Remove function definition.
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 print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
std::list< std::string > defines
#define HELP_SHOW_CLASS_HIERARCHY
void weak_memory(memory_modelt model, value_setst &value_sets, goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, 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)
Remove calls to functions without a body.
Dump C from Goto Program.
std::string get_value(char option) const
ui_message_handlert ui_message_handler
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 remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
function_mapt function_map
Race Detection for Threaded Goto Programs.
Field-insensitive, location-sensitive bitvector analysis.
Memory-mapped I/O Instrumentation for Goto Programs.
void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program)
Interpreter for GOTO Programs.
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
static mstreamt & eom(mstreamt &m)
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
Weak Memory Instrumentation for Threaded Goto Programs.
virtual int doit()
invoke main modules
Remove 'asm' statements by compiling into suitable standard code.
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
void remove_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
void print_path_lengths(const goto_modelt &goto_model)
Documentation of Properties.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
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...
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.
Set the properties to check.
bool function_pointer_removal_done
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
bool set(const cmdlinet &cmdline)
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 dot(const goto_modelt &src, std::ostream &out)
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert::uit ui)
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3)
void check(const goto_modelt &, bool xml, std::ostream &)
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert::uit ui)
virtual bool isset(char option) const
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
bool partial_inlining_done
#define HELP_SHOW_PROPERTIES
void output_xml(std::ostream &out) const
Nondeterministic initialization of certain global scope variables.
void list_eloc(const goto_modelt &goto_model)
void output_dot(std::ostream &out) const
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Dump Goto-Program as DOT Graph.
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...
#define PRECONDITION(CONDITION)
void slice_global_inits(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, bool add_safety_assertion, bool only_remove_const_fps)
Field-insensitive, location-sensitive, over-approximative escape analysis.
void parse_unwindset_file(const std::string &file_name)
void restore_returns(goto_modelt &goto_model)
restores return statements
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void do_partial_inlining()
void show_value_sets(ui_message_handlert::uit ui, const goto_modelt &goto_model, const value_set_analysist &value_set_analysis)
void instrument_goto_program()
std::string banner_string(const std::string &front_end, const std::string &version)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
void output_dot(std::ostream &out) const
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void output(std::ostream &out) const
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
void parse_unwindset(const std::string &unwindset)
#define HELP_GOTO_PROGRAM_STATS
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
Interrupt Instrumentation for Goto Programs.
A generic container class for the GOTO intermediate representation of one function.
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
Verify and use annotated invariants and pre/post-conditions.
static void list_calls_and_arguments(const namespacet &ns, const irep_idt &function, const goto_programt &goto_program)
unsigned safe_string2unsigned(const std::string &str, int base)
#define HELP_REMOVE_CALLS_NO_BODY
void havoc_loops(goto_modelt &goto_model)
void output(std::ostream &out) const
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
typet type
Type of symbol.
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 A list of currently accepted command line argumen...
message_handlert & get_message_handler()
Goto Programs with Functions.
static irep_idt entry_point()
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & result() const
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
mstreamt & status() const
#define HELP_SHOW_GOTO_FUNCTIONS
virtual void help()
display command line help
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
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 remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Harnessing for goto functions.
#define CPROVER_EXIT_CONVERSION_FAILED
Failure to convert / write to another format.
void check_call_sequence(const goto_modelt &goto_model)
void show_class_hierarchy(const class_hierarchyt &hierarchy, message_handlert &message_handler, ui_message_handlert::uit ui, bool children_only)
Output the class hierarchy.
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
Handling of functions without body.
ui_message_handlert::uit get_ui()
#define HELP_REPLACE_FUNCTION_BODY
void count_eloc(const goto_modelt &goto_model)
goto_programt & goto_program
void interrupt(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program, const symbol_exprt &interrupt_handler, const rw_set_baset &isr_rw_set)
void race_check(value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program, w_guardst &w_guards)
void interval_analysis(goto_modelt &goto_model)
Expression to hold a symbol (variable)
void code_contracts(goto_modelt &goto_model)
#define CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
Compute natural loops in a goto_function.
void set_option(const std::string &option, const bool value)
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
Memory-mapped I/O Instrumentation for Goto Programs.
Encoding for Threaded Goto Programs.
void parse_unwind(const std::string &unwind)
void instrument(goto_modelt &)
#define forall_goto_functions(it, functions)
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
void function_exit(goto_modelt &goto_model, const irep_idt &id)
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Field-insensitive, location-sensitive, over-approximative escape analysis.
#define forall_goto_program_instructions(it, program)
Add parameter assignments.
message_handlert * message_handler
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void print_global_state_size(const goto_modelt &goto_model)
virtual void register_languages()
void horn_encoding(const goto_modelt &, std::ostream &out)
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
void remove_asm(goto_functionst::goto_functiont &goto_function, symbol_tablet &symbol_table)
removes assembler
void branch(goto_modelt &goto_model, const irep_idt &id)
void thread_exit_instrumentation(goto_programt &goto_program)
Race Detection for Threaded Goto Programs.
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
bool splice_call(goto_functionst &goto_functions, const std::string &callercallee, const symbol_tablet &symbol_table, message_handlert &message_handler)
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 stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const int i_depth, const exprt &max_depth)