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()));
109 std::unordered_map<irep_idt, symbolt, irep_id_hash> &label_flags,
162 const auto flag = [&]() ->
symbolt {
163 const auto existing_flag = label_flags.find(inputs.
label);
164 if(existing_flag != label_flags.end())
165 return existing_flag->second;
168 label_location.set_hide();
176 label_flags.emplace(inputs.
label, new_flag);
179 instructions_to_add.emplace_back(
186 instructions_to_add.emplace_back(
190 auto clear_on_arrival = make_clear_flag();
191 instructions_to_add.emplace_back(
199 auto goto_location = goto_instruction->source_location();
200 goto_location.set_hide();
202 flag.symbol_expr(),
true_exprt{}, goto_location);
203 instructions_to_add.emplace_back(goto_instruction, set_flag);
216 bool add_if = declaration->accounted_flags.find(flag.name) ==
217 declaration->accounted_flags.end();
220 auto declaration_location = declaration->instruction->source_location();
221 declaration_location.set_hide();
223 target, flag.symbol_expr(), declaration_location);
227 std::next(declaration->instruction), std::move(if_goto));
228 declaration->accounted_flags.insert(flag.name);
230 target = declaration->instruction;
235 goto_instruction->set_target(target);
237 return instructions_to_add;
254 std::unordered_map<irep_idt, symbolt, irep_id_hash> label_flags;
269 "goto label \'" +
id2string(goto_label) +
"\' not found",
273 i.
targets.push_back(l_it->second.first);
283 "goto label \'" +
id2string(goto_label) +
"\' not found",
296 goto_target, label_target);
305 debug() <<
"adding goto-destructor code on jump to '" << goto_label
325 const bool variables_added_to_scope =
327 if(variables_added_to_scope)
332 debug() <<
"encountered goto '" << goto_label
333 <<
"' that enters one or more lexical blocks; "
334 <<
"adding declaration code on jump to '" << goto_label <<
"'"
339 inputs.
label = l_it->first;
344 instructions_to_insert.splice(
345 instructions_to_insert.end(),
355 for(
auto r_it = instructions_to_insert.rbegin();
356 r_it != instructions_to_insert.rend();
381 label_expr.
set(ID_identifier, label.first);
411 i.get_target()->target_number = (++cnt);
418 auto it_goto_y = std::next(it);
421 it_goto_y == dest.
instructions.end() || !it_goto_y->is_goto() ||
422 !it_goto_y->condition().is_true() || it_goto_y->is_target())
427 auto it_z = std::next(it_goto_y);
433 if(it->get_target()->target_number == it_z->target_number)
436 it->condition().find(ID_C_spec_assigns).is_nil() &&
437 it->condition().find(ID_C_spec_loop_invariant).is_nil() &&
438 it->condition().find(ID_C_spec_decreases).is_nil(),
439 "no loop invariant expected");
440 irept y_assigns = it_goto_y->condition().
find(ID_C_spec_assigns);
441 irept y_loop_invariant =
442 it_goto_y->condition().
find(ID_C_spec_loop_invariant);
443 irept y_decreases = it_goto_y->condition().
find(ID_C_spec_decreases);
445 it->set_target(it_goto_y->get_target());
448 updated_condition.
add(ID_C_spec_assigns).
swap(y_assigns);
450 updated_condition.
add(ID_C_spec_loop_invariant).
swap(y_loop_invariant);
452 updated_condition.
add(ID_C_spec_decreases).
swap(y_decreases);
453 it->condition_nonconst() = updated_condition;
454 it_goto_y->turn_into_skip();
508 "code() in magic thread creation label is null");
526 target->labels.push_front(label);
564 case_op_dest.push_back(code.
case_op());
568 case_op_dest.back().source_location().is_not_nil(),
569 "case operand should have a source location",
570 case_op_dest.back().pretty(),
580 const auto lb = numeric_cast<mp_integer>(code.
lower());
581 const auto ub = numeric_cast<mp_integer>(code.
upper());
584 lb.has_value() && ub.has_value(),
585 "GCC's switch-case-range statement requires constant bounds",
591 warning() <<
"GCC's switch-case-range statement with empty case range"
610 cases_entry->second->second.push_back(
and_exprt{
623 if(statement == ID_block)
625 else if(statement == ID_decl)
627 else if(statement == ID_decl_type)
629 else if(statement == ID_expression)
631 else if(statement == ID_assign)
633 else if(statement == ID_assert)
635 else if(statement == ID_assume)
637 else if(statement == ID_function_call)
639 else if(statement == ID_label)
641 else if(statement == ID_gcc_local_label)
643 else if(statement == ID_switch_case)
645 else if(statement == ID_gcc_switch_case_range)
648 else if(statement == ID_for)
650 else if(statement == ID_while)
652 else if(statement == ID_dowhile)
654 else if(statement == ID_switch)
656 else if(statement == ID_break)
658 else if(statement == ID_return)
660 else if(statement == ID_continue)
662 else if(statement == ID_goto)
664 else if(statement == ID_gcc_computed_goto)
666 else if(statement == ID_skip)
668 else if(statement == ID_ifthenelse)
670 else if(statement == ID_start_thread)
672 else if(statement == ID_end_thread)
674 else if(statement == ID_atomic_begin)
676 else if(statement == ID_atomic_end)
678 else if(statement == ID_cpp_delete || statement ==
"cpp_delete[]")
680 else if(statement == ID_msc_try_except)
682 else if(statement == ID_msc_try_finally)
684 else if(statement == ID_msc_leave)
686 else if(statement == ID_try_catch)
688 else if(statement == ID_CPROVER_try_catch)
690 else if(statement == ID_CPROVER_throw)
692 else if(statement == ID_CPROVER_try_finally)
694 else if(statement == ID_asm)
696 else if(statement == ID_static_assert)
707 else if(statement == ID_dead)
709 else if(statement == ID_decl_block)
711 for(
const auto &op : code.
operands())
715 statement == ID_push_catch || statement == ID_pop_catch ||
716 statement == ID_exception_landingpad)
764 if(expr.
id() == ID_if)
827 const auto declaration_iterator = std::prev(dest.
instructions.end());
843 return declaration_iterator;
864 destructor.
arguments().push_back(this_expr);
885 if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_function_call)
890 rhs.operands().size() == 2,
891 "function_call sideeffect takes two operands",
892 rhs.find_source_location());
902 rhs_function_call.function(),
903 rhs_function_call.arguments(),
908 rhs.id() == ID_side_effect && (rhs.get(ID_statement) == ID_cpp_new ||
909 rhs.get(ID_statement) == ID_cpp_new_array))
921 rhs.id() == ID_side_effect &&
922 (rhs.get(ID_statement) == ID_assign ||
923 rhs.get(ID_statement) == ID_postincrement ||
924 rhs.get(ID_statement) == ID_preincrement ||
925 rhs.get(ID_statement) == ID_statement_expression ||
926 rhs.get(ID_statement) == ID_gcc_conditional_expression))
933 new_assign.
lhs() = lhs;
934 new_assign.
rhs() = rhs;
938 else if(rhs.id() == ID_side_effect)
949 new_assign.
lhs() = lhs;
950 new_assign.
rhs() = rhs;
961 new_assign.
lhs() = lhs;
962 new_assign.
rhs() = rhs;
974 "cpp_delete statement takes one operand",
983 const exprt &destructor =
984 static_cast<const exprt &
>(code.
find(ID_destructor));
989 delete_identifier =
"__delete_array";
991 delete_identifier =
"__delete";
1008 convert(tmp_code, dest, ID_cpp);
1015 exprt delete_symbol =
ns.
lookup(delete_identifier).symbol_expr();
1019 "delete statement takes 1 parameter");
1028 convert(delete_call, dest, ID_cpp);
1044 annotated_location.
set(
"user-provided",
true);
1075 auto assigns =
static_cast<const unary_exprt &
>(code.
find(ID_C_spec_assigns));
1076 if(assigns.is_not_nil())
1078 PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
1079 loop->condition_nonconst().add(ID_C_spec_assigns).swap(assigns.op());
1083 static_cast<const exprt &
>(code.
find(ID_C_spec_loop_invariant));
1084 if(!invariant.is_nil())
1086 PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
1087 loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant);
1090 auto decreases_clause =
1091 static_cast<const exprt &
>(code.
find(ID_C_spec_decreases));
1092 if(!decreases_clause.is_nil())
1094 PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
1095 loop->condition_nonconst().add(ID_C_spec_decreases).swap(decreases_clause);
1260 "dowhile takes two operands",
1299 y->complete_goto(C);
1318 W->complete_goto(w);
1339 disjuncts.reserve(case_op.size());
1341 for(
const auto &op : case_op)
1344 if(op.id() == ID_and)
1352 disjuncts.push_back(skeleton);
1451 size_t case_number = 1;
1454 const caset &case_ops = case_pair.second;
1456 if(case_ops.empty())
1461 source_locationt source_location = case_ops.front().find_source_location();
1470 case_pair.first, std::move(guard_expr), source_location));
1479 std::move(guard_expr), source_location));
1482 case_pair.first,
true_exprt{}, source_location));
1485 try_next->complete_goto(next_case);
1531 "return takes none or one operand",
1553 "function must return value",
1566 "function must not return value",
1585 "continue without target",
1636 "end_thread expects no operands",
1646 "atomic_begin expects no operands",
1656 ": atomic_end expects no operands",
1730 std::list<exprt> &dest)
1734 dest.push_back(expr);
1739 for(
const auto &op : expr.
operands())
1777 true_case.
instructions.back().condition().is_false() &&
1795 false_case.
instructions.back().condition().is_false() &&
1818 true_case.
instructions.back().get_other().get_statement() ==
1844 bool has_else = !
is_empty(false_case);
1875 tmp_y.
swap(false_case);
1886 tmp_w.
swap(true_case);
1890 x->complete_goto(z);
1900 bool then_branch_returns = dest.
instructions.rbegin()->is_goto();
1905 if(!then_branch_returns)
1913 if(!has_else || !then_branch_returns)
1922 for(
const auto &op : expr.
operands())
1928 if(expr.
id() == ID_and || expr.
id() == ID_or)
1953 guard, target_true, target_false, source_location, dest, mode);
2003 std::list<exprt> op;
2006 for(
const auto &expr : op)
2008 boolean_negate(expr), target_false, source_location, dest, mode);
2023 std::list<exprt> op;
2027 for(
const auto &expr : op)
2029 expr, target_true, source_location, dest, mode);
2055 if(expr.
id() == ID_typecast)
2059 expr.
id() == ID_address_of &&
2066 if(index_op.
id() == ID_string_constant)
2071 else if(index_op.
id() == ID_array)
2074 for(
const auto &op :
as_const(index_op).operands())
2076 if(op.is_constant())
2078 const auto i = numeric_cast<std::size_t>(op);
2083 result +=
static_cast<char>(i.value());
2087 return value =
result,
false;
2091 if(expr.
id() == ID_string_constant)
2107 "expected string constant",
2116 if(expr.
id() == ID_symbol)
2120 return symbol.
value;
2122 else if(expr.
id() == ID_member)
2126 return std::move(tmp);
2128 else if(expr.
id() == ID_index)
2133 return std::move(tmp);
2141 const std::string &suffix,
2155 if(type.
id() != ID_code)
2166 const std::string &suffix,
2177 assignment.
rhs() = expr;
2180 convert(assignment, dest, mode);
2206 const symbol_table_baset::symbolst::const_iterator s_it =
2207 symbol_table.
symbols.find(
"main");
2210 s_it != symbol_table.
symbols.end(),
"failed to find main symbol");
2212 const symbolt &symbol = s_it->second;
2240 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_loop_contracts(const codet &code, goto_programt::targett loop)
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 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)
irep_idt make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, 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)
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)
std::list< std::pair< goto_programt::targett, goto_programt::instructiont > > declaration_hop_instrumentationt
declaration_hop_instrumentationt build_declaration_hops(goto_programt &dest, std::unordered_map< irep_idt, symbolt, irep_id_hash > &label_flags, const build_declaration_hops_inputst &inputs)
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 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)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
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...
There are a large number of kinds of tree structured or tree-like data in CPROVER.
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
irept & add(const irep_idt &name)
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)
const irep_idt & get_identifier() const
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)
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
#define Forall_operands(it, expr)
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)
exprt simplify_expr(exprt src, 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)
std::list< irep_idt > temporaries
Identifiers of temporaries introduced while cleaning an expression.
void add(clean_expr_resultt &&other)
void add_temporary(const irep_idt &id)
goto_programt side_effects
Statements implementing side effects of the expression that was subject to cleaning.
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