1/*******************************************************************\
3Module: Program Transformation
5Author: Daniel Kroening, kroening@kroening.com
7\*******************************************************************/
46 // in the first pass collect the labels and the corresponding targets
49 if(!it->labels.empty())
51 for(
auto label : it->labels)
52 // record the label and the corresponding target
57 // in the second pass set the targets
61 instruction.is_catch() &&
64 // Populate `targets` with a GOTO instruction target per
65 // exception handler if it isn't already populated.
66 // (Java handlers, for example, need this finish step; C++
67 // handlers will already be populated by now)
69 if(instruction.targets.empty())
77 // some handlers may not have been converted (if there was no
78 // exception to be caught); in such a situation we abort
109 std::unordered_map<irep_idt, symbolt, irep_id_hash> &
label_flags,
112 // In the case of a goto jumping into a scope, the declarations (but not the
113 // initialisations) need to be executed. This function prepares a
114 // transformation from code that looks like -
116 // statement_block_a();
119 // statement_block_b();
122 // statement_block_c();
125 // statement_block_d();
127 // statement_block_e();
129 // to code which looks like -
131 // __CPROVER_bool __CPROVER_going_to::user_label;
132 // __CPROVER_going_to::user_label = false;
133 // statement_block_a();
136 // __CPROVER_going_to::user_label = true;
137 // goto scope_x_label;
139 // statement_block_b();
142 // if __CPROVER_going_to::user_label goto scope_y_label:
144 // statement_block_c();
147 // if __CPROVER_going_to::user_label goto user_label:
149 // statement_block_d();
151 // __CPROVER_going_to::user_label = false;
152 // statement_block_e();
155 // The actual insertion of instructions needs to be performed by the caller,
156 // which needs to use the result of this method.
162 const auto flag = [&]() ->
symbolt {
178 // Create and initialise flag.
189 // Clear flag on arrival at label.
198 // Set flag before the goto.
211 auto &declaration =
targets.scope_stack.get_declaration(current_node);
212 targets.scope_stack.descend_tree();
216 bool add_if = declaration->accounted_flags.find(flag.name) ==
217 declaration->accounted_flags.end();
224 // this isn't changing any previously existing instruction so we insert
225 // directly rather than going through instructions_to_add
227 std::next(declaration->instruction), std::move(
if_goto));
228 declaration->accounted_flags.insert(flag.name);
230 target = declaration->instruction;
233 // Update the goto so that it goes to the first declaration rather than its
234 // original/final destination.
235 goto_instruction->set_target(target);
240/******************************************************************* \
242Function: goto_convertt::finish_gotos
250\*******************************************************************/
254 std::unordered_map<irep_idt, symbolt, irep_id_hash>
label_flags;
270 i.
code().find_source_location());
284 i.
code().find_source_location());
292 // Compare the currently-live variables on the path of the GOTO and label.
293 // We want to work out what variables should die during the jump.
295 targets.scope_stack.get_nearest_common_ancestor_info(
298 // If our goto had no variables of note, just skip (0 is the index of the
299 // root of the scope tree)
302 // If the goto recorded a destructor stack, execute as much as is
303 // appropriate for however many automatic variables leave scope.
318 // This should leave iterators intact, as long as
319 // goto_programt::instructionst is std::list.
322 // Variables *entering* scope on goto, is illegal for C++ non-pod types
323 // and impossible in Java. However, with the exception of Variable Length
324 // Arrays (VLAs), this is valid C and should be taken into account.
329 // If the goto recorded a destructor stack, execute as much as is
330 // appropriate for however many automatic variables leave scope.
333 <<
"' that enters one or more lexical blocks; "
334 <<
"adding declaration code on jump to '" <<
goto_label <<
"'"
373 // remember the expression for later checks
377 // insert huge case-split
378 for(
const auto &label :
targets.labels)
400 // We cannot use a set of targets, as target iterators
401 // cannot be compared at this stage.
403 // collect targets: reset marking
407 // mark the goto targets
411 i.get_target()->target_number = (++
cnt);
432 // cannot compare iterators, so compare target number instead
433 if(it->get_target()->target_number ==
it_z->target_number)
439 "no loop invariant expected");
499 // magic thread creation label.
500 // The "__CPROVER_ASYNC_" signals the start of a sequence of instructions
501 // that can be executed in parallel, i.e, a new thread.
504 // the body of the thread is expected to be
508 "code() in magic thread creation label is null");
510 // replace the magic thread creation label with a
511 // thread block (START_THREAD...END_THREAD).
525 {label, {target,
targets.scope_stack.get_current_node()}});
526 target->labels.push_front(label);
546 // is a default target given?
557 targets.cases.push_back(std::make_pair(target,
caset()));
559 targets.cases_map.insert(std::make_pair(target, --
targets.cases.end()))
565 // make sure we have a source location in the case operand as otherwise we
566 // end up with a GOTO instruction without a source location
569 "case operand should have a source location",
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"
609 // create a skeleton for case_guard
648 else if(statement ==
ID_for)
678 else if(statement ==
ID_cpp_delete || statement ==
"cpp_delete[]")
694 else if(statement ==
ID_asm)
698 // C23 allows static_assert without message
700 // We are double-checking the work of the type checker here.
706 "static assertion is false",
713 for(
const auto &op : code.
operands())
723 // make sure dest is never empty
737 // this saves the index of the destructor stack
744 // see if we need to do any destructors -- may have been processed
745 // in a prior break/continue/return already, don't create dead code
750 // don't do destructors when we are unreachable
755 // Set the current node of our destructor stack back to before the block.
768 // We do a special treatment for c?t:f
769 // by compiling to if(c) t; else f;
786 // Any residual expression?
787 // We keep it to add checks later.
810 return;
// this is a SKIP!
822 tmp.operands().resize(1);
823 // hide this declaration-without-initializer step in the goto trace
824 tmp.add_source_location().set_hide();
826 // Break up into decl and assignment.
827 // Decl must be visible before initializer.
848 // now create a 'dead' instruction -- will be added after the
849 // destructor created below as unwind_destructor_stack pops off the
850 // top of the destructor stack
866 destructor.
arguments().push_back(this_expr);
868 targets.scope_stack.add(destructor, {});
892 rhs.operands().size() == 2,
893 "function_call sideeffect takes two operands",
894 rhs.find_source_location());
919 // TODO: This should be done in a separate pass
930 // handle above side effects
942 // preserve side effects that will be handled at later stages,
943 // such as allocate, new operators of other languages, e.g. java, etc
958 // do everything else
976 "cpp_delete statement takes one operand",
984 // we call the destructor, and then free
985 const exprt &destructor =
1021 "delete statement takes 1 parameter");
1078 if(assigns.is_not_nil())
1080 PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
1086 if(!invariant.is_nil())
1088 PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
1096 PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
1106 // turn for(A; c; B) { P } into
1107 // A; while(c) { P; B; }
1108 //-----------------------------
1110 // u: sideeffects in c
1111 // v: if(!c) goto Z;
1114 // x: B; <-- continue target
1117 // z: ; <-- break target
1120 if(code.
init().is_not_nil())
1127 // save break/continue targets
1138 // do the z and Z labels
1148 if(code.
iter().is_nil())
1160 if(
tmp_x.instructions.empty())
1164 // optimize the v label
1172 // v: if(!c) goto Z;
1185 // assigns clause, loop invariant and decreases clause
1195 // restore break/continue
1208 //--------------------
1209 // v: sideeffects in c
1212 // y: goto v; <-- continue target
1213 // z: ; <-- break target
1215 // save break/continue targets
1243 // assigns clause, loop invariant and decreases clause
1251 // restore break/continue
1262 "dowhile takes two operands",
1265 // save source location
1273 //--------------------
1275 // x: sideeffects in c <-- continue target
1276 // y: if(!c) goto C;
1280 // z: ; <-- break target
1282 // save break/continue targets
1293 // do the z label and C labels
1300 // y: if(!c) goto C;
1301 y->complete_goto(
C);
1320 W->complete_goto(
w);
1322 // assigns_clause, loop invariant and decreases clause
1330 // restore break/continue targets
1343 for(
const auto &op : case_op)
1345 // could be a skeleton generated by convert_gcc_switch_case_range
1374 // --------------------
1376 // x: if(v==x) goto X;
1377 // y: if(v==y) goto Y;
1384 // we first add a 'location' node for the switch statement,
1385 // which would otherwise not be recorded
1388 // get the location of the end of the body, but
1389 // default to location of switch, if none
1395 // do the value we switch over
1400 // Avoid potential performance penalties caused by evaluating the value
1401 // multiple times (as the below chain-of-ifs does). "needs_cleaning" isn't
1402 // necessarily the right check here, and we may need to introduce a different
1403 // way of identifying the class of non-trivial expressions that warrant
1404 // introduction of a temporary.
1422 // save break/default/cases targets
1430 // set the new targets -- continue stays as is
1441 // The case number represents which case this corresponds to in the sequence
1442 // of case statements.
1446 // case 2: // case_number 1
1448 // case 3: // case_number 2
1450 // case 10: // case_number 3
1472 case_pair.first, std::move(guard_expr), source_location));
1481 std::move(guard_expr), source_location));
1492 targets.default_target,
targets.default_target->source_location()));
1499 // restore old targets
1511 // need to process destructor stack
1533 "return takes none or one operand",
1546 // remove void-typed return value
1555 "function must return value",
1558 // Now add a 'set return value' instruction to set the return value.
1568 "function must not return value",
1572 // Need to process _entire_ destructor stack.
1575 // add goto to end-of-function
1587 "continue without target",
1590 // need to process destructor stack
1601 // this instruction will be completed during post-processing
1605 // Loop contracts annotated in GOTO
1608 // remember it to do the target later
1609 targets.gotos.emplace_back(t,
targets.scope_stack.get_current_node());
1616 // this instruction will turn into OTHER during post-processing
1620 // remember it to do this later
1621 targets.computed_gotos.push_back(t);
1629 // remember it to do target later
1638 "end_thread expects no operands",
1648 "atomic_begin expects no operands",
1658 ": atomic_end expects no operands",
1675 // We do a bit of special treatment for && in the condition
1676 // in case cleaning would be needed otherwise.
1678 code.
cond().id() ==
ID_and && code.
cond().operands().size() == 2 &&
1683 // if(a && b) XX --> if(a) if(b) XX
1686 new_if1.add_source_location() = source_location;
1689 new_if0.add_source_location() = source_location;
1697 // convert 'then'-branch
1732 std::list<exprt> &dest)
1736 dest.push_back(expr);
1740 // left-to-right is important
1741 for(
const auto &op : expr.
operands())
1751 return (!
g.instructions.empty()) &&
1752 ++
g.instructions.begin() ==
g.instructions.end();
1768 // hmpf. Useless branch.
1776 // do guarded assertions directly
1782 // The above conjunction deliberately excludes the instance
1783 // if(some) { label: assert(false); }
1794 // similarly, do guarded assertions directly
1800 // The above conjunction deliberately excludes the instance
1801 // if(some) ... else { label: assert(false); }
1812 // a special case for C libraries that use
1813 // (void)((cond) || (assert(0),0))
1820 true_case.
instructions.back().get_other().get_statement() ==
1832 // Flip around if no 'true' case code.
1849 //--------------------
1850 // v: if(!c) goto z;
1855 //--------------------
1856 // v: if(!c) goto y;
1877 tmp_y.swap(false_case);
1878 y =
tmp_y.instructions.begin();
1881 // v: if(!c) goto z/y;
1888 tmp_w.swap(true_case);
1892 x->complete_goto(
z);
1897 // When the `then` branch of a balanced `if` condition ends with a `return` or
1898 // a `goto` statement, it is not necessary to add the `goto z` and `z:` goto
1899 // elements as they are never used.
1900 // This helps for example when using `--cover location` as such command are
1901 // marked unreachable, but are not part of the user-provided code to analyze.
1906 // Don't add the `goto` at the end of the `then` branch if not needed
1914 // Don't add the `z` label at the end of the `if` when not needed.
1924 for(
const auto &op : expr.
operands())
1945 // if(guard) goto target;
1947 // if(guard) goto target; else goto next;
1985 // simply swap targets
1999 // if(a && b) goto target_true; else goto target_false;
2001 // if(!a) goto target_false;
2002 // if(!b) goto target_false;
2003 // goto target_true;
2005 std::list<exprt> op;
2008 for(
const auto &expr : op)
2019 // if(a || b) goto target_true; else goto target_false;
2021 // if(a) goto target_true;
2022 // if(b) goto target_true;
2023 // goto target_false;
2025 std::list<exprt> op;
2029 for(
const auto &expr : op)
2078 if(op.is_constant())
2084 if(i.value() != 0)
// to skip terminating 0
2085 result +=
static_cast<char>(i.value());
2089 return value =
result,
false;
2109 "expected string constant",
2122 return symbol.
value;
2128 return std::move(
tmp);
2135 return std::move(
tmp);
2143 const std::string &suffix,
2168 const std::string &suffix,
2179 assignment.
rhs() = expr;
2182 convert(assignment, dest, mode);
2208 const symbol_table_baset::symbolst::const_iterator
s_it =
2209 symbol_table.
symbols.find(
"main");
2212 s_it != symbol_table.
symbols.end(),
"failed to find main symbol");
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.
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.
Boolean AND All operands must be boolean, and the result is always boolean.
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.
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 goto_instruction_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
goto_instruction_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
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
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
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)
const goto_instruction_codet & code() const
Get the code represented by this instruction.
targetst targets
The list of successor instructions.
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())
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 & 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)
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)
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_function_callt & to_code_function_call(const goto_instruction_codet &code)
const code_assignt & to_code_assign(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 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)
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,...)
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)
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.