24 const irep_idt identifier=
"$stack_depth";
28 new_symbol.
name=identifier;
38 symbol_table.
insert(std::move(new_symbol));
47 const exprt &max_depth)
55 assert_ins->make_assertion(guard);
56 assert_ins->source_location=first->source_location;
57 assert_ins->function=first->function;
59 assert_ins->source_location.set_comment(
61 assert_ins->source_location.set_property_class(
"stack-depth");
64 plus_ins->make_assignment();
68 plus_ins->function=first->function;
71 assert(last->is_end_function());
78 minus_ins.function=last->function;
93 if(f_it->second.body_available() &&
96 stack_depth(f_it->second.body, sym, depth, depth_expr);
99 goto_functionst::function_mapt::iterator i_it =
108 it->make_assignment();
irep_idt name
The unique identifier.
A generic base class for relations, i.e., binary predicates.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
targett insert_before(const_targett target)
Insertion before the given target.
irep_idt mode
Language mode.
exprt value
Initial value of symbol.
function_mapt function_map
irep_idt pretty_name
Language-specific display name.
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...
This class represents an instruction in the GOTO intermediate representation.
instructionst::iterator targett
Fixed-width bit-vector with two's complement interpretation.
#define INITIALIZE_FUNCTION
instructionst instructions
The list of instructions in the goto program.
symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table)
A generic container class for the GOTO intermediate representation of one function.
typet type
Type of symbol.
static irep_idt entry_point()
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
goto_programt & goto_program
Expression to hold a symbol (variable)
#define DATA_INVARIANT(CONDITION, REASON)
goto_functionst goto_functions
GOTO functions.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const int i_depth, const exprt &max_depth)