57 for(natural_loopst::loop_mapt::const_iterator
62 assert(!l_it->second.empty());
72 it=l_it->second.begin();
73 it!=l_it->second.end();
77 if((*it)->get_target()==loop_start &&
78 (*it)->location_number>loop_end->location_number)
82 if(!
loop_map.insert(std::make_pair(loop_start, loop_end)).second)
94 if(instruction.is_dead())
96 dead_map[instruction.dead_symbol().get_identifier()] =
97 instruction.location_number;
108 if(instruction.is_assign())
110 const exprt &l = instruction.assign_lhs();
111 const exprt &
r = instruction.assign_rhs();
115 r.id() == ID_side_effect &&
121 else if(l.
type().
id()==ID_pointer &&
122 l.
type().
get(ID_C_typedef)==
"va_list" &&
124 r.id()==ID_typecast &&
142 target->type() !=
ASSERT &&
143 !target->source_location().get_comment().empty())
146 dest.
statements().back().add_source_location().set_comment(
147 target->source_location().get_comment());
151 if(target->is_target() && !target->is_goto())
157 upper_bound->location_number > loop_entry->second->location_number))
163 switch(target->type())
176 target->call_lhs(), target->call_function(), target->call_arguments());
182 dest.
add(target->get_other());
197 dest.
statements().back().add_source_location().set_comment(
198 target->source_location().get_comment());
213 dest.
statements().back().add_source_location().set_comment(
"END_THREAD");
224 dest.
add(std::move(f));
251 if(target->is_target())
253 std::stringstream label;
258 latest_block->
add(std::move(l));
263 for(goto_programt::instructiont::labelst::const_iterator
264 it=target->labels.begin();
265 it!=target->labels.end();
280 latest_block->
add(std::move(l));
285 if(latest_block!=&dest)
294 const code_assignt a{target->assign_lhs(), target->assign_rhs()};
309 const exprt this_va_list_expr = target->assign_lhs();
312 if(
r.id()==ID_constant &&
317 {this_va_list_expr});
319 dest.
add(std::move(f));
322 r.id() == ID_side_effect &&
330 dest.
add(std::move(f));
332 else if(
r.id() == ID_plus)
336 {this_va_list_expr});
350 if(next!=upper_bound &&
353 const exprt &n_r = next->assign_rhs();
355 n_r.
id() == ID_dereference &&
358 f.lhs() = next->assign_lhs();
360 type_of.arguments().push_back(f.lhs());
361 f.arguments().push_back(type_of);
363 dest.
add(std::move(f));
369 assert(
r.find(ID_C_va_arg_type).is_not_nil());
370 const typet &va_arg_type=
371 static_cast<typet const&
>(
r.find(ID_C_va_arg_type));
377 type_of.arguments().push_back(deref);
378 f.arguments().push_back(type_of);
382 dest.
add(std::move(void_f));
388 {this_va_list_expr,
r});
390 dest.
add(std::move(f));
400 if(assign.
rhs().
id()==ID_array)
425 target->return_value().id() != ID_side_effect ||
437 while(next!=upper_bound && next->is_dead() && !next->is_target())
440 if(next!=upper_bound &&
464 upper_bound->location_number > entry->second);
468 if(next!=upper_bound &&
470 !next->is_target() &&
471 (next->is_assign() || next->is_function_call()))
473 exprt lhs = next->is_assign() ? next->assign_lhs() : next->call_lhs();
477 if(next->is_assign())
485 next->call_function(),
486 next->call_arguments(),
504 dest.
add(std::move(d));
516 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
525 for( ; target!=loop_end; ++target)
532 dest.
add(std::move(d));
541 assert(target->is_goto());
543 assert(target->targets.size()==1);
549 upper_bound->location_number > loop_entry->second->location_number))
551 else if(!target->guard.is_true())
564 assert(loop_end->is_goto() && loop_end->is_backwards_goto());
576 if(target->get_target()==after_loop)
581 else if(target->guard.is_true())
592 for(++target; target!=loop_end; ++target)
598 if(loop_end->guard.is_false())
602 else if(!loop_end->guard.is_true())
612 if(w.body().has_operands() &&
616 w.body().operands().pop_back();
617 increment.
id(ID_side_effect);
625 else if(w.body().has_operands() &&
635 w.body().operands().pop_back();
644 dest.
add(std::move(w));
652 const exprt &switch_var,
658 std::set<goto_programt::const_targett> unique_targets;
662 cases_it!=upper_bound && cases_it!=first_target;
665 if(cases_it->is_goto() &&
666 !cases_it->is_backwards_goto() &&
667 cases_it->guard.is_true())
669 default_target=cases_it->get_target();
672 first_target->location_number > default_target->location_number)
673 first_target=default_target;
675 last_target->location_number < default_target->location_number)
676 last_target=default_target;
678 cases.push_back(
caset(
683 unique_targets.insert(default_target);
688 else if(cases_it->is_goto() &&
689 !cases_it->is_backwards_goto() &&
690 (cases_it->guard.id()==ID_equal ||
691 cases_it->guard.id()==ID_or))
694 if(cases_it->guard.id()==ID_equal)
695 eqs.push_back(cases_it->guard);
697 eqs=cases_it->guard.operands();
701 for(exprt::operandst::const_reverse_iterator
703 e_it!=(exprt::operandst::const_reverse_iterator)eqs.rend();
706 if(e_it->id()!=ID_equal ||
711 cases.push_back(
caset(
715 cases_it->get_target()));
716 assert(cases.back().value.is_not_nil());
719 first_target->location_number>
720 cases.back().case_start->location_number)
721 first_target=cases.back().case_start;
723 last_target->location_number<
724 cases.back().case_start->location_number)
725 last_target=cases.back().case_start;
727 unique_targets.insert(cases.back().case_start);
736 if(unique_targets.size()<3)
740 if(cases_it==upper_bound ||
742 upper_bound->location_number < last_target->location_number) ||
744 last_target->location_number > default_target->location_number) ||
745 target->get_target()==default_target)
755 std::set<unsigned> &processed_locations)
757 std::set<goto_programt::const_targett> targets_done;
759 for(cases_listt::iterator it=cases.begin();
765 if(!targets_done.insert(it->case_start).second)
771 case_end->type() !=
END_FUNCTION && case_end != upper_bound;
774 const auto &case_end_node = dominators.
get_node(case_end);
781 if(case_end==it->case_start)
788 if(!dominators.
dominates(it->case_start, case_end_node))
791 if(!processed_locations.insert(case_end->location_number).second)
794 it->case_last=case_end;
806 for(cases_listt::const_iterator it=cases.begin();
815 cases_listt::const_iterator last=--cases.end();
816 if(last->case_start==default_target &&
831 next_case == default_target &&
832 (!it->case_last->is_goto() ||
833 (it->case_last->get_condition().is_true() &&
834 it->case_last->get_target() == default_target)))
843 if(it->case_last->is_goto() &&
844 it->case_last->guard.is_true() &&
845 it->case_last->get_target()==default_target)
849 if(!it->case_last->is_goto())
864 exprt eq_cand=target->guard;
865 if(eq_cand.
id()==ID_or)
868 if(target->is_backwards_goto() ||
869 eq_cand.
id()!=ID_equal ||
901 if(cases_start==target)
909 for(target=cases_start; target!=first_target; ++target)
912 std::set<unsigned> processed_locations;
931 for(cases_listt::const_iterator it=cases.begin();
935 it->case_last->location_number > max_target->location_number)
936 max_target=it->case_last;
938 std::map<goto_programt::const_targett, unsigned> targets_done;
943 for(cases_listt::const_iterator it=cases.begin();
949 if(it->value.is_nil())
952 csc.case_op()=it->value;
956 if(targets_done.find(it->case_start)!=targets_done.end())
958 assert(it->case_selector==orig_target ||
959 !it->case_selector->is_target());
967 csc.code().swap(cscp->
code());
974 if(it->case_selector!=orig_target)
978 target=it->case_start;
985 if(it->case_start!=(--cases.end())->case_start)
999 for( ; target!=after_last; ++target)
1004 targets_done[it->case_start]=s.
body().
operands().size();
1014 if(processed_locations.find(it->location_number)==
1015 processed_locations.end())
1024 dest.
add(std::move(s));
1037 bool has_else=
false;
1039 if(!target->is_backwards_goto())
1046 if(before_else==target)
1053 before_else->is_goto() &&
1054 before_else->get_target()->location_number > end_if->location_number &&
1055 before_else->guard.is_true() &&
1057 upper_bound->location_number>=
1058 before_else->get_target()->location_number);
1061 end_if=before_else->get_target();
1065 if(target->is_backwards_goto() ||
1067 upper_bound->location_number < end_if->location_number))
1084 for(++target; target!=before_else; ++target)
1090 for(++target; target!=end_if; ++target)
1096 for(++target; target!=end_if; ++target)
1101 dest.
add(std::move(i));
1124 if(target->get_target()==next)
1133 if(target->get_target()==loop_end &&
1144 dest.
add(std::move(i));
1158 if(target->get_target()==after_loop)
1168 dest.
add(std::move(i));
1183 if(target->get_target()==next)
1193 std::stringstream label;
1195 for(goto_programt::instructiont::labelst::const_iterator
1196 it=target->get_target()->labels.begin();
1197 it!=target->get_target()->labels.end();
1211 if(label.str().empty())
1212 label <<
CPROVER_PREFIX "DUMP_L" << target->get_target()->target_number;
1226 dest.
add(std::move(i));
1236 assert(target->is_start_thread());
1239 assert(thread_start->location_number > target->location_number);
1250 if(!next->is_goto())
1254 assert(this_end->is_end_thread());
1255 assert(thread_start->location_number > this_end->location_number);
1260 for(goto_programt::instructiont::labelst::const_iterator
1261 it=target->labels.begin();
1262 it!=target->labels.end();
1274 dest.
add(std::move(b));
1285 assert(next->is_goto() && next->guard.is_true());
1286 assert(!next->is_backwards_goto());
1287 assert(thread_start->location_number < next->get_target()->location_number);
1289 ++after_thread_start;
1293 assert(thread_start->location_number < thread_end->location_number);
1294 assert(thread_end->is_end_thread());
1297 thread_end->location_number < upper_bound->location_number);
1303 thread_start->is_function_call() &&
1304 thread_start->call_arguments().size() == 1 &&
1305 after_thread_start == thread_end)
1311 thread_start->call_lhs(),
1315 thread_start->call_function(),
1316 thread_start->call_arguments().front()}));
1322 for( ; thread_start!=thread_end; ++thread_start)
1326 for(goto_programt::instructiont::labelst::const_iterator
1327 it=target->labels.begin();
1328 it!=target->labels.end();
1340 dest.
add(std::move(b));
1365 if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
1382 else if(type.
id()==ID_c_enum_tag)
1391 assert(!identifier.
empty());
1394 else if(type.
id()==ID_pointer ||
1395 type.
id()==ID_array)
1408 code.
op1().
id()==ID_side_effect &&
1427 if(!typedef_str.
empty() &&
1440 call.
lhs().
id()==ID_typecast)
1448 if(op.id() == ID_code)
1456 if(statement==ID_label)
1461 assert(!label.
empty());
1469 else if(statement==ID_block)
1471 else if(statement==ID_ifthenelse)
1473 else if(statement==ID_dowhile)
1484 code=do_while.
body();
1489 const exprt &function,
1492 if(function.
id()!=ID_symbol)
1505 if(parameters.size()==arguments.size())
1507 code_typet::parameterst::const_iterator it=parameters.begin();
1508 for(
auto &argument : arguments)
1511 argument.type().id() == ID_union ||
1512 argument.type().id() == ID_union_tag)
1514 argument.type() = it->type();
1530 operands.size()>1 && i<operands.size();
1533 exprt::operandst::iterator it=operands.begin()+i;
1536 it->source_location().get_comment().
empty())
1541 bool has_decl=
false;
1551 operands.insert(operands.begin()+i+1,
1552 it->operands().begin(), it->operands().end());
1553 operands.erase(operands.begin()+i);
1563 if(operands.empty() && parent_stmt!=ID_nil)
1565 else if(operands.size()==1 &&
1566 parent_stmt!=ID_nil &&
1577 type.
remove(ID_C_constant);
1579 if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
1588 "Symbol "+
id2string(identifier)+
" should be a type");
1592 else if(type.
id()==ID_array)
1594 else if(type.
id()==ID_struct ||
1595 type.
id()==ID_union)
1600 for(struct_union_typet::componentst::iterator
1606 else if(type.
id() == ID_c_bit_field)
1626 if(expr.
is_nil() ||
to_code(expr).get_statement() != ID_block)
1632 block.
statements().back().get_statement() != ID_label)
1713 code =
code_blockt({i_t_e, then_label, else_label});
1746 (expr.
id()==ID_address_of || expr.
id()==ID_member))
1751 else if(!no_typecast &&
1752 (expr.
id()==ID_union || expr.
id()==ID_struct ||
1753 expr.
id()==ID_array || expr.
id()==ID_vector))
1766 expr.
id() == ID_union && expr.
type().
id() != ID_union &&
1767 expr.
type().
id() != ID_union_tag)
1773 if(expr.
id()==ID_typecast &&
1777 if(expr.
id()==ID_union ||
1778 expr.
id()==ID_struct)
1784 expr.
type().
id() == ID_struct_tag || expr.
type().
id() == ID_union_tag,
1785 "union/struct expressions should have a tag type");
1793 if(!typedef_str.
empty() &&
1797 else if(expr.
id()==ID_array ||
1798 expr.
id()==ID_vector)
1801 expr.
get_bool(ID_C_string_constant))
1810 if(!typedef_str.
empty() &&
1814 else if(expr.
id()==ID_side_effect)
1818 if(statement==ID_nondet)
1825 for(symbol_tablet::symbolst::const_iterator
1830 if(it->second.type.id()!=ID_code)
1852 suffix=expr.
type().
get(ID_C_c_type);
1859 if(base_name.
empty())
1870 symbol.
name=base_name;
1888 else if(expr.
id()==ID_isnan ||
1891 else if(expr.
id()==ID_constant)
1893 if(expr.
type().
id()==ID_floatbv)
1899 else if(expr.
type().
id()==ID_pointer)
1902 const irept &c_sizeof_type=expr.
find(ID_C_c_sizeof_type);
1907 else if(expr.
id()==ID_typecast)
1909 if(expr.
type().
id() == ID_c_bit_field)
1916 if(!typedef_str.
empty() &&
1920 assert(expr.
type().
id()!=ID_union &&
1921 expr.
type().
id()!=ID_struct);
1924 else if(expr.
id()==ID_symbol)
1926 if(expr.
type().
id()!=ID_code)
1932 symbol.
type.
id()!=ID_code &&
1953 if(src->get_code().source_location().is_not_nil())
1955 else if(src->source_location().is_not_nil())
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
typet index_type() const
The type of the index expressions into any instance of this type.
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
const typet & underlying_type() const
const cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
bool dominates(T lhs, const nodet &rhs_node) const
Returns true if the program point corresponding to rhs_node is dominated by program point lhs.
bool program_point_reachable(const nodet &program_point_node) const
Returns true if the program point for program_point_node is reachable from the entry point.
A non-fatal assertion, which checks a condition then permits execution to continue.
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
A codet representing sequential composition of program statements.
code_operandst & statements()
void add(const codet &code)
codet representation of a break statement (within a for or while loop).
codet representation of a continue statement (within a for or while loop).
codet representation of a do while statement.
const codet & body() const
const exprt & cond() const
codet representation of an expression statement.
codet representation of a for statement.
A codet representing the declaration of a local variable.
void set_initial_value(optionalt< exprt > initial_value)
Sets the value to which this declaration initializes the declared variable.
codet representation of a function call statement.
exprt::operandst argumentst
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
codet representation of a "return from a function" statement.
const exprt & return_value() const
A codet representing a skip statement.
codet representation of a switch-case, i.e. a case statement within a switch.
codet representing a switch statement.
const codet & body() const
const exprt & value() const
std::vector< parametert > parameterst
const parameterst & parameters() const
const typet & return_type() const
codet representing a while statement.
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
void set_statement(const irep_idt &statement)
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool has_operands() const
Return true if there is at least one operand.
bool is_true() const
Return whether the expression is a constant representing true.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
bool is_false() const
Return whether the expression is a constant representing false.
void reserve_operands(operandst::size_type n)
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
The Boolean constant false.
goto_programt::const_targett convert_goto_switch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
goto_programt::const_targett convert_assign_varargs(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
std::unordered_set< irep_idt > local_static_set
std::unordered_set< irep_idt > type_names_set
goto_programt::const_targett convert_goto_break_continue(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
void cleanup_code_ifthenelse(codet &code, const irep_idt parent_stmt)
loop_last_stackt loop_last_stack
void convert_labels(goto_programt::const_targett target, code_blockt &dest)
goto_programt::const_targett convert_decl(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
symbol_tablet & symbol_table
goto_programt::const_targett convert_do_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, code_blockt &dest)
goto_programt::const_targett convert_goto_goto(goto_programt::const_targett target, code_blockt &dest)
const goto_programt & goto_program
goto_programt::const_targett convert_start_thread(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
goto_programt::const_targett get_cases(goto_programt::const_targett target, goto_programt::const_targett upper_bound, const exprt &switch_var, cases_listt &cases, goto_programt::const_targett &first_target, goto_programt::const_targett &default_target)
void cleanup_code_block(codet &code, const irep_idt parent_stmt)
std::list< caset > cases_listt
void copy_source_location(goto_programt::const_targett, codet &dst)
bool remove_default(const cfg_dominatorst &dominators, const cases_listt &cases, goto_programt::const_targett default_target)
goto_programt::const_targett convert_throw(goto_programt::const_targett target, code_blockt &dest)
std::unordered_set< irep_idt > const_removed
goto_programt::const_targett convert_catch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
void remove_const(typet &type)
std::unordered_set< exprt, irep_hash > va_list_expr
goto_programt::const_targett convert_goto(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
void add_local_types(const typet &type)
void cleanup_expr(exprt &expr, bool no_typecast)
void cleanup_code(codet &code, const irep_idt parent_stmt)
void cleanup_function_call(const exprt &function, code_function_callt::argumentst &arguments)
goto_programt::const_targett convert_assign(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
goto_programt::const_targett convert_instruction(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
void convert_assign_rec(const code_assignt &assign, code_blockt &dest)
std::unordered_set< irep_idt > labels_in_use
goto_programt::const_targett convert_goto_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, code_blockt &dest)
goto_programt::const_targett convert_goto_if(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
std::set< std::string > & system_headers
code_blockt & toplevel_block
const std::unordered_set< irep_idt > & typedef_names
goto_programt::const_targett convert_set_return_value(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
bool set_block_end_points(goto_programt::const_targett upper_bound, const cfg_dominatorst &dominators, cases_listt &cases, std::set< unsigned > &processed_locations)
This class represents an instruction in the GOTO intermediate representation.
exprt guard
Guard for gotos, assume, assert Use condition() method to access.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::const_iterator const_targett
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void remove(const irep_idt &name)
const irep_idt & id() const
loop_instructionst::const_iterator const_iterator
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const cfg_dominators_templatet< P, T, false > & get_dominator_info() const
The null pointer constant.
A side_effect_exprt representation of a function call side effect.
exprt::operandst & arguments()
const irep_idt & get_statement() const
const irep_idt & get_function() const
Base type for structs and unions.
const componentst & components() const
std::vector< componentt > componentst
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
const irep_idt & get_identifier() const
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
const typet & subtype() const
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
const code_function_callt & to_code_function_call(const codet &code)
static bool has_labels(const codet &code)
static bool move_label_ifthenelse(exprt &expr, exprt &label_dest)
Dump Goto-Program as C/C++ Source.
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
bool is_true(const literalt &l)
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 simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#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,...
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_switch_caset & to_code_switch_case(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_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 codet & to_code(const exprt &expr)
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const type_with_subtypet & to_type_with_subtype(const typet &type)