50 if(!it->labels.empty())
52 for(
auto label : it->labels)
59 for(
auto &instruction :
dest.instructions)
62 instruction.is_catch() &&
70 if(instruction.targets.empty())
115 if(
i.is_start_thread())
119 labelst::const_iterator
l_it=
126 i.get_code().find_source_location());
129 i.targets.push_back(
l_it->second.first);
131 else if(
i.is_incomplete_goto())
141 i.get_code().find_source_location());
144 i.complete_goto(
l_it->second.first);
152 targets.destructor_stack.get_nearest_common_ancestor_info(
169 <<
"' that enters one or more lexical blocks; "
170 <<
"omitting constructors and destructors" <<
eom;
215 for(
const auto &label :
targets.labels)
225 label.second.first, guard,
i.source_location()));
241 for(
auto &
i :
dest.instructions)
246 for(
const auto &
i :
dest.instructions)
248 i.get_target()->target_number = (++
cnt);
250 for(
auto it =
dest.instructions.begin(); it !=
dest.instructions.end(); it++)
270 if(it->get_target()->target_number ==
it_z->target_number)
328 "code() in magic thread creation label is null");
345 {label, {target,
targets.destructor_stack.get_current_node()}});
346 target->labels.push_front(label);
379 targets.cases.push_back(std::make_pair(target,
caset()));
381 target, --
targets.cases.end())).first;
398 lb.has_value() && ub.has_value(),
399 "GCC's switch-case-range statement requires constant bounds",
405 warning() <<
"GCC's switch-case-range statement with empty case range"
462 else if(statement==
ID_for)
493 statement==
"cpp_delete[]")
509 else if(statement==
ID_asm)
537 if(
dest.instructions.empty())
552 targets.destructor_stack.get_current_node();
561 !
dest.empty() &&
dest.instructions.back().is_goto() &&
562 dest.instructions.back().get_condition().is_true())
633 initializer=code.
op1();
634 tmp.operands().resize(1);
668 destructor.
arguments().push_back(this_expr);
670 targets.destructor_stack.add(destructor);
697 rhs.operands().size() == 2,
698 "function_call sideeffect takes two operands",
699 rhs.find_source_location());
770 "cpp_delete statement takes one operand",
778 const exprt &destructor=
814 "delete statement takes 1 parameter");
838 t->source_location_nonconst().set(
"user-provided",
true);
867 if(assigns.is_not_nil())
875 if(!invariant.is_nil())
894 "Decreases clause is not side-effect free.",
956 if(
tmp_x.instructions.empty())
1058 "dowhile takes two operands",
1106 y->complete_goto(
w);
1129 for(
const auto &op : case_op)
1255 case_pair.first, std::move(guard_expr), source_location));
1259 targets.default_target,
targets.default_target->source_location()));
1300 "return takes none or one operand",
1323 "function must return value",
1335 "function must not return value",
1354 "continue without target",
1373 targets.gotos.emplace_back(t,
targets.destructor_stack.get_current_node());
1385 targets.computed_gotos.push_back(t);
1406 "end_thread expects no operands",
1418 "atomic_begin expects no operands",
1430 ": atomic_end expects no operands",
1459 new_if1.add_source_location() = source_location;
1462 new_if0.add_source_location() = source_location;
1485 std::list<exprt> &
dest)
1489 dest.push_back(expr);
1504 return (!
g.instructions.empty()) &&
1505 ++
g.instructions.begin()==
g.instructions.end();
1531 true_case.
instructions.back().get_condition().is_false() &&
1537 dest.destructive_append(true_case);
1549 false_case.
instructions.back().get_condition().is_false() &&
1555 dest.destructive_append(false_case);
1569 true_case.
instructions.front().get_condition().is_false() &&
1575 dest.destructive_append(true_case);
1623 tmp_y.swap(false_case);
1624 y=
tmp_y.instructions.begin();
1634 tmp_w.swap(true_case);
1638 x->complete_goto(
z);
1639 x->source_location_nonconst() =
tmp_w.instructions.back().source_location();
1730 std::list<exprt> op;
1733 for(
const auto &expr : op)
1750 std::list<exprt> op;
1754 for(
const auto &expr : op)
1798 if(it->is_constant())
1805 result +=
static_cast<char>(
i.value());
1808 return value=
result,
false;
1828 "expected string constant",
1842 return symbol.
value;
1848 return std::move(
tmp);
1855 return std::move(
tmp);
1863 const std::string &suffix,
1886 const std::string &suffix,
1897 assignment.
rhs()=expr;
1924 const symbol_tablet::symbolst::const_iterator
s_it=
1925 symbol_table.
symbols.find(
"main");
1928 s_it != symbol_table.
symbols.end(),
"failed to find main symbol");
1966 e->source_location_nonconst() =
thread_body.source_location();
1978 dest.destructive_append(body);
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Result of an attempt to find ancestor information about two nodes.
A base class for binary expressions.
A base class for relations, i.e., binary predicates whose two operands have the same type.
A non-fatal assertion, which checks a condition then permits execution to continue.
const exprt & assertion() const
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
const exprt & assumption() const
A codet representing sequential composition of program statements.
code_operandst & statements()
source_locationt end_location() const
codet representation of a break statement (within a for or while loop).
codet representation of a continue statement (within a for or while loop).
A codet representing the removal of a local variable going out of scope.
codet representation of a do while statement.
const codet & body() const
const exprt & cond() const
codet representation of an expression statement.
const exprt & expression() const
codet representation of a for statement.
const exprt & cond() const
const exprt & iter() const
const codet & body() const
const exprt & init() const
A codet representing the declaration of a local variable.
const irep_idt & get_identifier() const
codet representation of a "return from a function" statement.
const exprt & return_value() const
bool has_return_value() const
codet representation of a function call statement.
codet representation of a switch-case, i.e. a case statement within a switch.
const exprt & upper() const
upper bound of range
const exprt & lower() const
lower bound of range
codet & code()
the statement to be executed when the case applies
codet representation of a goto statement.
codet representation of an if-then-else statement.
const exprt & cond() const
const codet & else_case() const
const codet & then_case() const
codet representation of a label for branch targets.
const irep_idt & get_label() const
std::vector< exception_list_entryt > exception_listt
codet representation of a switch-case, i.e. a case statement within a switch.
const exprt & case_op() const
codet representing a switch statement.
const codet & body() const
const exprt & value() const
const parameterst & parameters() const
codet representing a while statement.
const exprt & cond() const
const codet & body() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
Operator to dereference a pointer.
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 & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
std::vector< exprt > operandst
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
void convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode)
void convert_assume(const code_assumet &code, goto_programt &dest, const irep_idt &mode)
symbol_table_baset & symbol_table
void convert_expression(const code_expressiont &code, goto_programt &dest, const irep_idt &mode)
void convert_while(const code_whilet &code, goto_programt &dest, const irep_idt &mode)
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
void optimize_guarded_gotos(goto_programt &dest)
Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" This only works if the "goto y" is not a bra...
void convert_atomic_begin(const codet &code, goto_programt &dest)
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_msc_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_gcc_switch_case_range(const code_gcc_switch_case_ranget &, goto_programt &dest, const irep_idt &mode)
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
irep_idt get_string_constant(const exprt &expr)
void convert_label(const code_labelt &code, goto_programt &dest, const irep_idt &mode)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
exprt get_constant(const exprt &expr)
void convert_start_thread(const codet &code, goto_programt &dest)
void finish_gotos(goto_programt &dest, const irep_idt &mode)
void generate_conditional_branch(const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) goto target_true; else goto target_false;
void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode)
void convert_atomic_end(const codet &code, goto_programt &dest)
std::string tmp_symbol_prefix
void convert_frontend_decl(const code_frontend_declt &, goto_programt &, const irep_idt &mode)
void convert_gcc_local_label(const codet &code, goto_programt &dest)
struct goto_convertt::targetst targets
void convert_break(const code_breakt &code, goto_programt &dest, const irep_idt &mode)
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
void convert_goto(const code_gotot &code, goto_programt &dest)
exprt case_guard(const exprt &value, const caset &case_op)
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_cpp_delete(const codet &code, goto_programt &dest)
void convert_switch(const code_switcht &code, goto_programt &dest, const irep_idt &mode)
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
void convert_decl_type(const codet &code, goto_programt &dest)
void convert_dowhile(const code_dowhilet &code, goto_programt &dest, const irep_idt &mode)
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
void convert_loop_contracts(const codet &code, goto_programt::targett loop, const irep_idt &mode)
void convert_skip(const codet &code, goto_programt &dest)
void convert_asm(const code_asmt &code, goto_programt &dest)
void convert_switch_case(const code_switch_caset &code, goto_programt &dest, const irep_idt &mode)
void unwind_destructor_stack(const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, optionalt< node_indext > destructor_start_point={}, optionalt< node_indext > destructor_end_point={})
Unwinds the destructor stack and creates destructors for each node between destructor_start_point and...
void convert_msc_try_except(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_continue(const code_continuet &code, goto_programt &dest, const irep_idt &mode)
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
static bool needs_cleaning(const exprt &expr)
void finish_computed_gotos(goto_programt &dest)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
static void replace_new_object(const exprt &object, exprt &dest)
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
void convert_return(const code_frontend_returnt &, goto_programt &dest, const irep_idt &mode)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void convert_block(const code_blockt &code, goto_programt &dest, const irep_idt &mode)
void generate_thread_block(const code_blockt &thread_body, goto_programt &dest, const irep_idt &mode)
Generates the necessary goto-instructions to represent a thread-block.
void convert_end_thread(const codet &code, goto_programt &dest)
This class represents an instruction in the GOTO intermediate representation.
static const unsigned nil_target
Uniquely identify an invalid target or location.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_location(const source_locationt &l)
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
The trinary if-then-else operator.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const irep_idt & id() const
source_locationt source_location
mstreamt & warning() const
mstreamt & result() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void set_case_number(const irep_idt &number)
const irep_idt & get_value() const
Expression to hold a symbol (variable)
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Generic base class for unary expressions.
bool has_prefix(const std::string &s, const std::string &prefix)
code_function_callt get_destructor(const namespacet &ns, const typet &type)
bool is_empty(const std::string &s)
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
static bool has_and_or(const exprt &expr)
if(guard) goto target;
static bool is_size_one(const goto_programt &g)
This is (believed to be) faster than using std::list.size.
static void finish_catch_push_targets(goto_programt &dest)
Populate the CATCH instructions with the targets corresponding to their associated labels.
static bool is_empty(const goto_programt &goto_program)
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
const irept & get_nil_irep()
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool is_skip(const goto_programt &body, goto_programt::const_targett it, bool ignore_labels)
Determine whether the instruction is semantically equivalent to a skip (no-op).
bool simplify(exprt &expr, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_breakt & to_code_break(const codet &code)
const code_switch_caset & to_code_switch_case(const codet &code)
const code_gotot & to_code_goto(const codet &code)
const code_assertt & to_code_assert(const codet &code)
static code_push_catcht & to_code_push_catch(codet &code)
const code_frontend_returnt & to_code_frontend_return(const codet &code)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
const code_dowhilet & to_code_dowhile(const codet &code)
const code_assumet & to_code_assume(const codet &code)
const code_whilet & to_code_while(const codet &code)
const code_labelt & to_code_label(const codet &code)
const code_blockt & to_code_block(const codet &code)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
code_asmt & to_code_asm(codet &code)
const code_fort & to_code_for(const codet &code)
const code_switcht & to_code_switch(const codet &code)
const code_frontend_declt & to_code_frontend_decl(const codet &code)
code_expressiont & to_code_expression(codet &code)
const code_continuet & to_code_continue(const codet &code)
const codet & to_code(const exprt &expr)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
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.
const string_constantt & to_string_constant(const exprt &expr)