Go to the documentation of this file.
24 const irep_idt identifier=
"$stack_depth";
28 new_symbol.
name=identifier;
38 symbol_table.
insert(std::move(new_symbol));
46 const std::size_t i_depth,
47 const exprt &max_depth)
57 assert_ins->source_location.set_comment(
59 assert_ins->source_location.set_property_class(
"stack-depth");
68 assert(last->is_end_function());
79 const std::size_t depth)
87 if(f_it->second.body_available() &&
90 stack_depth(f_it->second.body, sym, depth, depth_expr);
93 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,...
#define INITIALIZE_FUNCTION
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
#define Forall_goto_functions(it, functions)
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