Go to the documentation of this file.
25 const irep_idt identifier=
"$stack_depth";
29 new_symbol.
name=identifier;
39 symbol_table.
insert(std::move(new_symbol));
47 const std::size_t i_depth,
48 const exprt &max_depth)
58 assert_ins->source_location.set_comment(
60 assert_ins->source_location.set_property_class(
"stack-depth");
69 assert(last->is_end_function());
80 const std::size_t depth)
90 gf_entry.second.body_available() &&
94 stack_depth(gf_entry.second.body, sym, depth, depth_expr);
99 goto_functionst::function_mapt::iterator i_it =
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
typet type
Type of symbol.
The plus expression Associativity is not specified.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
function_mapt function_map
Expression to hold a symbol (variable)
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Fixed-width bit-vector with unsigned binary interpretation.
irep_idt pretty_name
Language-specific display name.
typet & type()
Return the type of the expression.
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
irep_idt mode
Language mode.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Pre-defined bitvector types.
#define INITIALIZE_FUNCTION
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
instructionst instructions
The list of instructions in the goto program.
exprt value
Initial value of symbol.
goto_functionst goto_functions
GOTO functions.
A base class for relations, i.e., binary predicates whose two operands have the same type.
A generic container class for the GOTO intermediate representation of one function.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
A codet representing an assignment in the program.
symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table)
This class represents an instruction in the GOTO intermediate representation.
const source_locationt & source_location() const
symbol_tablet symbol_table
Symbol table.
irep_idt name
The unique identifier.
instructionst::iterator targett