44 std::map<irep_idt, goto_programt::targett> label_targets;
49 if(!it->labels.empty())
51 for(
auto label : it->labels)
53 label_targets.insert(std::make_pair(label, it));
61 instruction.is_catch() &&
62 instruction.code().get_statement() == ID_push_catch)
69 if(instruction.targets.empty())
71 bool handler_added =
true;
75 for(
const auto &handler : handler_list)
79 if(label_targets.find(handler.get_label()) == label_targets.end())
81 handler_added =
false;
89 for(
const auto &handler : handler_list)
90 instruction.targets.push_back(label_targets.at(handler.get_label()));
108 std::unordered_map<irep_idt, symbolt, irep_id_hash> &label_flags,
156 const auto flag = [&]() ->
symbolt {
157 const auto existing_flag = label_flags.find(inputs.
label);
158 if(existing_flag != label_flags.end())
159 return existing_flag->second;
162 label_location.set_hide();
170 label_flags.emplace(inputs.
label, new_flag);
180 flag_creation.
instructions.push_back(make_clear_flag());
184 auto clear_on_arrival = make_clear_flag();
192 auto goto_location = goto_instruction->source_location();
193 goto_location.set_hide();
195 flag.symbol_expr(),
true_exprt{}, goto_location);
211 bool add_if = declaration->accounted_flags.find(flag.name) ==
212 declaration->accounted_flags.end();
215 auto declaration_location = declaration->instruction->source_location();
216 declaration_location.set_hide();
218 target, flag.symbol_expr(), declaration_location);
220 std::next(declaration->instruction), std::move(if_goto));
221 declaration->accounted_flags.insert(flag.name);
223 target = declaration->instruction;
228 goto_instruction->set_target(target);
245 std::unordered_map<irep_idt, symbolt, irep_id_hash> label_flags;
259 "goto label \'" +
id2string(goto_label) +
"\' not found",
263 i.
targets.push_back(l_it->second.first);
273 "goto label \'" +
id2string(goto_label) +
"\' not found",
286 goto_target, label_target);
295 debug() <<
"adding goto-destructor code on jump to '" << goto_label
315 const bool variables_added_to_scope =
317 if(variables_added_to_scope)
322 debug() <<
"encountered goto '" << goto_label
323 <<
"' that enters one or more lexical blocks; "
324 <<
"adding declaration code on jump to '" << goto_label <<
"'"
329 inputs.
label = l_it->first;
362 label_expr.
set(ID_identifier, label.first);
392 i.get_target()->target_number = (++cnt);
399 auto it_goto_y = std::next(it);
402 it_goto_y == dest.
instructions.end() || !it_goto_y->is_goto() ||
403 !it_goto_y->condition().is_true() || it_goto_y->is_target())
408 auto it_z = std::next(it_goto_y);
414 if(it->get_target()->target_number == it_z->target_number)
416 it->set_target(it_goto_y->get_target());
418 it_goto_y->turn_into_skip();
472 "code() in magic thread creation label is null");
490 target->labels.push_front(label);
528 case_op_dest.push_back(code.
case_op());
532 case_op_dest.back().source_location().is_not_nil(),
533 "case operand should have a source location",
534 case_op_dest.back().pretty(),
544 const auto lb = numeric_cast<mp_integer>(code.
lower());
545 const auto ub = numeric_cast<mp_integer>(code.
upper());
548 lb.has_value() && ub.has_value(),
549 "GCC's switch-case-range statement requires constant bounds",
555 warning() <<
"GCC's switch-case-range statement with empty case range"
574 cases_entry->second->second.push_back(
and_exprt{
587 if(statement == ID_block)
589 else if(statement == ID_decl)
591 else if(statement == ID_decl_type)
593 else if(statement == ID_expression)
595 else if(statement == ID_assign)
597 else if(statement == ID_assert)
599 else if(statement == ID_assume)
601 else if(statement == ID_function_call)
603 else if(statement == ID_label)
605 else if(statement == ID_gcc_local_label)
607 else if(statement == ID_switch_case)
609 else if(statement == ID_gcc_switch_case_range)
612 else if(statement == ID_for)
614 else if(statement == ID_while)
616 else if(statement == ID_dowhile)
618 else if(statement == ID_switch)
620 else if(statement == ID_break)
622 else if(statement == ID_return)
624 else if(statement == ID_continue)
626 else if(statement == ID_goto)
628 else if(statement == ID_gcc_computed_goto)
630 else if(statement == ID_skip)
632 else if(statement == ID_ifthenelse)
634 else if(statement == ID_start_thread)
636 else if(statement == ID_end_thread)
638 else if(statement == ID_atomic_begin)
640 else if(statement == ID_atomic_end)
642 else if(statement == ID_cpp_delete || statement ==
"cpp_delete[]")
644 else if(statement == ID_msc_try_except)
646 else if(statement == ID_msc_try_finally)
648 else if(statement == ID_msc_leave)
650 else if(statement == ID_try_catch)
652 else if(statement == ID_CPROVER_try_catch)
654 else if(statement == ID_CPROVER_throw)
656 else if(statement == ID_CPROVER_try_finally)
658 else if(statement == ID_asm)
660 else if(statement == ID_static_assert)
671 else if(statement == ID_dead)
673 else if(statement == ID_decl_block)
675 for(
const auto &op : code.
operands())
679 statement == ID_push_catch || statement == ID_pop_catch ||
680 statement == ID_exception_landingpad)
728 if(expr.
id() == ID_if)
787 const auto declaration_iterator = std::prev(dest.
instructions.end());
800 return declaration_iterator;
821 destructor.
arguments().push_back(this_expr);
841 if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_function_call)
846 rhs.operands().size() == 2,
847 "function_call sideeffect takes two operands",
848 rhs.find_source_location());
855 rhs_function_call.function(),
856 rhs_function_call.arguments(),
861 rhs.id() == ID_side_effect && (rhs.get(ID_statement) == ID_cpp_new ||
862 rhs.get(ID_statement) == ID_cpp_new_array))
871 rhs.id() == ID_side_effect &&
872 (rhs.get(ID_statement) == ID_assign ||
873 rhs.get(ID_statement) == ID_postincrement ||
874 rhs.get(ID_statement) == ID_preincrement ||
875 rhs.get(ID_statement) == ID_statement_expression ||
876 rhs.get(ID_statement) == ID_gcc_conditional_expression))
882 new_assign.
lhs() = lhs;
883 new_assign.
rhs() = rhs;
887 else if(rhs.id() == ID_side_effect)
895 new_assign.
lhs() = lhs;
896 new_assign.
rhs() = rhs;
906 new_assign.
lhs() = lhs;
907 new_assign.
rhs() = rhs;
917 "cpp_delete statement takes one operand",
925 const exprt &destructor =
926 static_cast<const exprt &
>(code.
find(ID_destructor));
931 delete_identifier =
"__delete_array";
933 delete_identifier =
"__delete";
950 convert(tmp_code, dest, ID_cpp);
957 exprt delete_symbol =
ns.
lookup(delete_identifier).symbol_expr();
961 "delete statement takes 1 parameter");
970 convert(delete_call, dest, ID_cpp);
983 annotated_location.
set(
"user-provided",
true);
1010 auto assigns =
static_cast<const unary_exprt &
>(code.
find(ID_C_spec_assigns));
1011 if(assigns.is_not_nil())
1014 loop->condition_nonconst().add(ID_C_spec_assigns).swap(assigns.op());
1018 static_cast<const exprt &
>(code.
find(ID_C_spec_loop_invariant));
1019 if(!invariant.is_nil())
1028 loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant);
1031 auto decreases_clause =
1032 static_cast<const exprt &
>(code.
find(ID_C_spec_decreases));
1033 if(!decreases_clause.is_nil())
1038 "Decreases clause is not side-effect free.",
1043 loop->condition_nonconst().add(ID_C_spec_decreases).swap(decreases_clause);
1202 "dowhile takes two operands",
1250 y->complete_goto(w);
1271 disjuncts.reserve(case_op.size());
1273 for(
const auto &op : case_op)
1276 if(op.id() == ID_and)
1284 disjuncts.push_back(skeleton);
1347 convert(copy_value, sideeffects, mode);
1383 size_t case_number = 1;
1386 const caset &case_ops = case_pair.second;
1388 if(case_ops.empty())
1393 source_locationt source_location = case_ops.front().find_source_location();
1399 case_pair.first, std::move(guard_expr), source_location));
1444 "return takes none or one operand",
1466 "function must return value",
1478 "function must not return value",
1497 "continue without target",
1545 "end_thread expects no operands",
1555 "atomic_begin expects no operands",
1565 ": atomic_end expects no operands",
1636 std::list<exprt> &dest)
1640 dest.push_back(expr);
1645 for(
const auto &op : expr.
operands())
1683 true_case.
instructions.back().condition().is_false() &&
1701 false_case.
instructions.back().condition().is_false() &&
1721 true_case.
instructions.front().condition().is_false() &&
1747 bool has_else = !
is_empty(false_case);
1778 tmp_y.
swap(false_case);
1789 tmp_w.
swap(true_case);
1793 x->complete_goto(z);
1803 bool then_branch_returns = dest.
instructions.rbegin()->is_goto();
1808 if(!then_branch_returns)
1816 if(!has_else || !then_branch_returns)
1825 for(
const auto &op : expr.
operands())
1831 if(expr.
id() == ID_and || expr.
id() == ID_or)
1856 guard, target_true, target_false, source_location, dest, mode);
1901 std::list<exprt> op;
1904 for(
const auto &expr : op)
1906 boolean_negate(expr), target_false, source_location, dest, mode);
1921 std::list<exprt> op;
1925 for(
const auto &expr : op)
1927 expr, target_true, source_location, dest, mode);
1947 if(expr.
id() == ID_typecast)
1951 expr.
id() == ID_address_of &&
1958 if(index_op.
id() == ID_string_constant)
1963 else if(index_op.
id() == ID_array)
1966 for(
const auto &op :
as_const(index_op).operands())
1968 if(op.is_constant())
1970 const auto i = numeric_cast<std::size_t>(op);
1975 result +=
static_cast<char>(i.value());
1979 return value =
result,
false;
1983 if(expr.
id() == ID_string_constant)
1999 "expected string constant",
2008 if(expr.
id() == ID_symbol)
2012 return symbol.
value;
2014 else if(expr.
id() == ID_member)
2018 return std::move(tmp);
2020 else if(expr.
id() == ID_index)
2025 return std::move(tmp);
2033 const std::string &suffix,
2056 const std::string &suffix,
2067 assignment.
rhs() = expr;
2070 convert(assignment, dest, mode);
2094 const symbol_table_baset::symbolst::const_iterator s_it =
2095 symbol_table.
symbols.find(
"main");
2098 s_it != symbol_table.
symbols.end(),
"failed to find main symbol");
2100 const symbolt &symbol = s_it->second;
2128 convert(thread_body, body, mode);
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
static exprt guard(const exprt::operandst &guards, exprt cond)
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
Result of an attempt to find ancestor information about two nodes.
std::size_t right_depth_below_common_ancestor
node_indext common_ancestor
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 goto_instruction_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.
source_locationt end_location() const
void add(const codet &code)
code_operandst & statements()
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 goto_instruction_codet representing the removal of a local variable going out of scope.
codet representation of a do while statement.
const exprt & cond() const
const codet & body() const
codet representation of an expression statement.
const exprt & expression() const
codet representation of a for statement.
const exprt & init() const
const exprt & iter() const
const exprt & cond() const
const codet & body() 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
goto_instruction_codet representation of a function call statement.
codet representation of a switch-case, i.e. a case statement within a switch.
codet & code()
the statement to be executed when the case applies
const exprt & lower() const
lower bound of range
const exprt & upper() const
upper bound of range
codet representation of a goto statement.
codet representation of an if-then-else statement.
const codet & then_case() const
const exprt & cond() const
const codet & else_case() const
codet representation of a label for branch targets.
const irep_idt & get_label() const
std::vector< exception_list_entryt > exception_listt
exception_listt & exception_list()
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 exprt & value() const
const codet & body() 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.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
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
source_locationt & add_source_location()
const source_locationt & source_location() const
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
The Boolean constant false.
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 generate_ifthenelse(const exprt &cond, const source_locationt &, goto_programt &true_case, const source_locationt &, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
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)
void unwind_destructor_stack(const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, std::optional< node_indext > destructor_end_point={}, std::optional< node_indext > destructor_start_point={})
Unwinds the destructor stack and creates destructors for each node between destructor_start_point and...
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 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 build_declaration_hops(goto_programt &dest, std::unordered_map< irep_idt, symbolt, irep_id_hash > &label_flags, const build_declaration_hops_inputst &inputs)
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
static bool needs_cleaning(const exprt &expr)
Returns 'true' for expressions that may change the program state.
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)
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.
void complete_goto(targett _target)
targetst targets
The list of successor instructions.
const goto_instruction_codet & code() const
Get the code represented by this instruction.
bool is_start_thread() const
static const unsigned nil_target
Uniquely identify an invalid target or location.
const source_locationt & source_location() const
bool is_incomplete_goto() const
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())
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
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_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
void swap(goto_programt &program)
Swap the goto program.
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())
bool empty() const
Is the program empty?
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, 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 & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
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().
std::optional< declaration_statet > & get_declaration(node_indext index)
Fetches the declaration value for the passed-in node index.
void add(const codet &destructor, std::optional< goto_programt::targett > declaration)
Adds a destructor/declaration pair to the current stack, attaching it to the current node.
void descend_tree()
Walks the current node down to its child.
void set_current_node(std::optional< node_indext > val)
Sets the current node.
node_indext get_current_node() const
Gets the node that the next addition will be added to as a child.
const ancestry_resultt get_nearest_common_ancestor_info(node_indext left_index, node_indext right_index)
Finds the nearest common ancestor of two nodes and then returns it.
void set_case_number(const irep_idt &number)
void value(const irep_idt &)
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.
code_function_callt get_destructor(const namespacet &ns, const typet &type)
#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_assignt & to_code_assign(const goto_instruction_codet &code)
const code_function_callt & to_code_function_call(const goto_instruction_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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_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...
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
const code_gotot & to_code_goto(const codet &code)
const code_whilet & to_code_while(const codet &code)
const code_continuet & to_code_continue(const codet &code)
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_assumet & to_code_assume(const codet &code)
const code_switch_caset & to_code_switch_case(const codet &code)
const code_labelt & to_code_label(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_switcht & to_code_switch(const codet &code)
code_expressiont & to_code_expression(codet &code)
const code_frontend_declt & to_code_frontend_decl(const codet &code)
const code_breakt & to_code_break(const codet &code)
static code_push_catcht & to_code_push_catch(codet &code)
const code_blockt & to_code_block(const codet &code)
const code_frontend_returnt & to_code_frontend_return(const codet &code)
const code_assertt & to_code_assert(const codet &code)
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
const code_fort & to_code_for(const codet &code)
code_asmt & to_code_asm(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 if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_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)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void restore(targetst &targets)
void restore(targetst &targets)
computed_gotost computed_gotos
goto_programt::targett continue_target
node_indext continue_stack_node
node_indext break_stack_node
void set_break(goto_programt::targett _break_target)
goto_programt::targett default_target
goto_programt::targett return_target
void set_default(goto_programt::targett _default_target)
void set_continue(goto_programt::targett _continue_target)
goto_programt::targett break_target