26 const irep_idt identifier=
"$stack_depth";
30 new_symbol.
name=identifier;
40 symbol_table.
move(new_symbol);
49 const exprt &max_depth)
57 assert_ins->make_assertion(guard);
58 assert_ins->source_location=first->source_location;
59 assert_ins->function=first->function;
61 assert_ins->source_location.set_comment(
62 "Stack depth exceeds "+std::to_string(i_depth));
63 assert_ins->source_location.set_property_class(
"stack-depth");
66 plus_ins->make_assignment();
70 plus_ins->function=first->function;
73 assert(last->is_end_function());
75 goto_programt::instructiont minus_ins;
76 minus_ins.make_assignment();
80 minus_ins.function=last->function;
94 if(f_it->second.body_available() &&
97 stack_depth(f_it->second.body, sym, depth, depth_expr);
100 goto_functionst::function_mapt::iterator
107 it->make_assignment();
109 it->source_location=first->source_location;
110 it->function=first->function;
irep_idt name
The unique identifier.
A generic base class for relations, i.e., binary predicates.
irep_idt mode
Language mode.
instructionst instructions
The list of instructions in the goto program.
Goto Programs with Functions.
exprt value
Initial value of symbol.
irep_idt pretty_name
Language-specific display name.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Fixed-width bit-vector with two's complement interpretation.
static irep_idt entry_point()
API to expression classes.
symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table)
function_mapt function_map
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
targett insert_before(const_targett target)
Insertion before the given target.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Expression to hold a symbol (variable)
instructionst::iterator targett
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const int i_depth, const exprt &max_depth)