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