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)
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;
85 const std::size_t depth)
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.
Fixed-width bit-vector with unsigned binary interpretation.
A 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 instruction pointed-to by the given instruction iterator target.
irep_idt mode
Language mode.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
exprt value
Initial value of symbol.
function_mapt function_map
irep_idt pretty_name
Language-specific display name.
typet & type()
Return the type of the expression.
symbol_tablet symbol_table
Symbol table.
This class represents an instruction in the GOTO intermediate representation.
instructionst::iterator targett
#define INITIALIZE_FUNCTION
instructionst instructions
The list of instructions in the goto program.
The plus expression Associativity is not specified.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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()
Get the identifier of the entry point to a goto model.
Base class for all expressions.
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
irep_idt base_name
Base (non-scoped) name.
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Expression to hold a symbol (variable)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
goto_functionst goto_functions
GOTO functions.
A codet representing an assignment in the program.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.