75 throw "throw label "+
throws.get_string(
ID_label)+
" not found";
77 symbol.value.swap(code);
92 for(itemst::const_iterator
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A codet representing sequential composition of program statements.
code_operandst & statements()
codet representation of an expression statement.
codet representation of a "return from a function" statement.
codet representation of a label for branch targets.
const irep_idt & get_label() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void output(std::ostream &) const
symbolt to_symbol() const
void output(std::ostream &out) const
A side_effect_exprt representation of a side effect that throws an exception.
Expression to hold a symbol (variable)
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
const irep_idt & get_identifier() const
The type of an expression, extends irept.
static bool insert_at_label(const codet &code, const irep_idt &label, code_blockt &dest)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const code_labelt & to_code_label(const codet &code)
const code_blockt & to_code_block(const codet &code)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.