58 for(natural_loopst::loop_mapt::const_iterator
72 for(natural_loopst::natural_loopt::const_iterator
73 it=
l_it->second.begin();
74 it!=
l_it->second.end();
79 (*it)->location_number>
loop_end->location_number)
95 if(instruction.is_dead())
97 dead_map[instruction.dead_symbol().get_identifier()] =
98 instruction.location_number;
107 for(
const auto &instruction :
goto_program.instructions)
109 if(instruction.is_assign())
111 const exprt &l = instruction.assign_lhs();
112 const exprt &
r = instruction.assign_rhs();
143 target->type() !=
ASSERT &&
144 !target->source_location().get_comment().empty())
147 dest.
statements().back().add_source_location().set_comment(
148 target->source_location().get_comment());
152 if(target->is_target() && !target->is_goto())
158 upper_bound->location_number >
loop_entry->second->location_number))
164 switch(target->type())
177 target->call_lhs(), target->call_function(), target->call_arguments());
183 dest.
add(target->get_other());
198 dest.
statements().back().add_source_location().set_comment(
199 target->source_location().get_comment());
214 dest.
statements().back().add_source_location().set_comment(
"END_THREAD");
225 dest.
add(std::move(f));
252 if(target->is_target())
254 std::stringstream label;
264 for(goto_programt::instructiont::labelst::const_iterator
265 it=target->labels.begin();
266 it!=target->labels.end();
295 const code_assignt a{target->assign_lhs(), target->assign_rhs()};
319 dest.
add(std::move(f));
330 dest.
add(std::move(f));
350 if(next!=upper_bound &&
353 const exprt &
n_r = next->assign_rhs();
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));
379 f.arguments().push_back(
type_of);
391 dest.
add(std::move(f));
438 while(next!=upper_bound && next->is_dead() && !next->is_target())
441 if(next!=upper_bound &&
465 upper_bound->location_number > entry->second);
469 if(next!=upper_bound &&
471 !next->is_target() &&
472 (next->is_assign() || next->is_function_call()))
474 exprt lhs = next->is_assign() ? next->assign_lhs() : next->call_lhs();
478 if(next->is_assign())
486 next->call_function(),
487 next->call_arguments(),
505 dest.
add(std::move(d));
533 dest.
add(std::move(d));
550 upper_bound->location_number >
loop_entry->second->location_number))
552 else if(!target->condition().is_true())
577 if(target->get_target()==after_loop)
582 else if(target->condition().is_true())
593 for(++target; target!=
loop_end; ++target)
599 if(
loop_end->condition().is_false())
603 else if(!
loop_end->condition().is_true())
613 if(
w.body().has_operands() &&
616 exprt increment =
w.body().operands().back();
617 w.body().operands().pop_back();
626 else if(
w.body().has_operands() &&
636 w.body().operands().pop_back();
645 dest.
add(std::move(
w));
659 std::set<goto_programt::const_targett, goto_programt::target_less_than>
671 default_target=
cases_it->get_target();
674 first_target->location_number > default_target->location_number)
677 last_target->location_number < default_target->location_number)
680 cases.push_back(
caset(
703 for(exprt::operandst::const_reverse_iterator
705 e_it!=(exprt::operandst::const_reverse_iterator)
eqs.rend();
713 cases.push_back(
caset(
718 DATA_INVARIANT(cases.back().value.is_not_nil(),
"cases should be set");
722 cases.back().case_start->location_number)
726 cases.back().case_start->location_number)
744 upper_bound->location_number <
last_target->location_number) ||
746 last_target->location_number > default_target->location_number) ||
747 target->get_target()==default_target)
759 std::set<goto_programt::const_targett, goto_programt::target_less_than>
762 for(cases_listt::iterator it=cases.begin();
809 for(cases_listt::const_iterator it=cases.begin();
818 cases_listt::const_iterator
last=--cases.end();
819 if(
last->case_start==default_target &&
835 (!it->case_last->is_goto() ||
836 (it->case_last->condition().is_true() &&
837 it->case_last->get_target() == default_target)))
847 it->case_last->is_goto() && it->case_last->condition().is_true() &&
848 it->case_last->get_target() == default_target)
852 if(!it->case_last->is_goto())
871 if(target->is_backwards_goto() ||
934 for(cases_listt::const_iterator it=cases.begin();
938 it->case_last->location_number >
max_target->location_number)
942 map<goto_programt::const_targett, unsigned, goto_programt::target_less_than>
948 for(cases_listt::const_iterator it=cases.begin();
954 if(it->value.is_nil())
957 csc.case_op()=it->value;
964 it->case_selector ==
orig_target || !it->case_selector->is_target(),
965 "valid case selector required");
984 target=it->case_start;
991 if(it->case_start!=(--cases.end())->case_start)
997 tmp.insert_before_swap(
tmp.insert_before(
tmp.instructions.end()), i);
1030 dest.
add(std::move(s));
1045 if(!target->is_backwards_goto())
1063 upper_bound->location_number >=
1071 if(target->is_backwards_goto() ||
1073 upper_bound->location_number <
end_if->location_number))
1096 for(++target; target!=
end_if; ++target)
1102 for(++target; target!=
end_if; ++target)
1107 dest.
add(std::move(i));
1123 next!=upper_bound && next!=
goto_program.instructions.end();
1130 if(target->get_target()==next)
1139 if(target->get_target()==
loop_end &&
1147 if(i.
cond().is_true())
1150 dest.
add(std::move(i));
1164 if(target->get_target()==after_loop)
1171 if(i.
cond().is_true())
1174 dest.
add(std::move(i));
1189 if(target->get_target()==next)
1199 std::stringstream label;
1201 for(goto_programt::instructiont::labelst::const_iterator
1202 it=target->get_target()->labels.begin();
1203 it!=target->get_target()->labels.end();
1217 if(label.str().empty())
1218 label <<
CPROVER_PREFIX "DUMP_L" << target->get_target()->target_number;
1229 if(i.
cond().is_true())
1232 dest.
add(std::move(i));
1256 if(!next->is_goto())
1263 "start of new thread must precede end of thread");
1268 for(goto_programt::instructiont::labelst::const_iterator
1269 it=target->labels.begin();
1270 it!=target->labels.end();
1282 dest.
add(std::move(
b));
1294 next->is_goto() && next->condition().is_true(),
"START THREAD pattern");
1295 DATA_INVARIANT(!next->is_backwards_goto(),
"START THREAD pattern");
1297 thread_start->location_number < next->get_target()->location_number,
1298 "START THREAD pattern");
1306 "monotone location numbers");
1311 thread_end->location_number < upper_bound->location_number,
1312 "end or monotone location numbers");
1341 for(goto_programt::instructiont::labelst::const_iterator
1342 it=target->labels.begin();
1343 it!=target->labels.end();
1355 dest.
add(std::move(
b));
1382 const typet &full_type=
ns.follow(type);
1385 const symbolt &symbol =
ns.lookup(identifier);
1400 const symbolt &symbol=
ns.lookup(identifier);
1454 while(
call.lhs().is_not_nil() &&
1497 else if(
do_while.cond().is_false() &&
1504 const exprt &function,
1514 if(!
ns.lookup(
fn.get_identifier(), s))
1520 if(parameters.size()==arguments.size())
1522 code_typet::parameterst::const_iterator it=parameters.begin();
1544 for(exprt::operandst::size_type i=0;
1545 operands.size()>1 && i<operands.size();
1548 exprt::operandst::iterator it=operands.begin()+i;
1551 it->source_location().get_comment().empty())
1557 for(
const auto &op :
as_const(*it).operands())
1568 operands.insert(operands.begin()+i+1,
1569 it->operands().begin(), it->operands().end());
1570 operands.erase(operands.begin()+i);
1582 else if(operands.size()==1 &&
1605 "Symbol "+
id2string(identifier)+
" should be a type");
1617 for(struct_union_typet::componentst::iterator
1634 for(
const auto &op : code.
operands())
1689 if(
i_t_e.else_case().is_nil())
1700 i_t_e.then_case().is_not_nil() &&
1709 i_t_e.else_case().is_not_nil() &&
1725 if(
i_t_e.then_case().is_not_nil())
1727 if(
i_t_e.else_case().is_not_nil())
1752 i_t_e.else_case().make_nil();
1756 (
i_t_e.then_case().is_nil() ||
1804 "union/struct expressions should have a tag type");
1844 for(symbol_tablet::symbolst::const_iterator
1849 if(it->second.type.id()!=
ID_code)
1878 if(base_name.
empty())
1884 base_name=
"nondet_"+std::to_string(count);
1888 symbol.base_name=base_name;
1939 "typedef must not be that of a struct or union type");
1947 const symbolt &symbol=
ns.lookup(identifier);
1971 if(src->code().source_location().is_not_nil())
1972 dst.add_source_location() = src->code().source_location();
1973 else if(src->source_location().is_not_nil())
1974 dst.add_source_location() = src->source_location();
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
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.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
typet index_type() const
The type of the index expressions into any instance of this type.
const typet & element_type() const
The type of the elements of the array.
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 goto_instruction_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.
goto_instruction_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
goto_instruction_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
codet representing a while statement.
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
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 & condition_nonconst()
Get the condition of gotos, assume, assert.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
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
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.
const irep_idt & get_statement() const
const irep_idt & get_function() const
Base type for structs and unions.
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.
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.
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
bool has_prefix(const std::string &s, const std::string &prefix)
#define Forall_operands(it, expr)
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
const code_function_callt & to_code_function_call(const goto_instruction_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 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(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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.
const type_with_subtypet & to_type_with_subtype(const typet &type)
typename detail::make_voidt< typest... >::type void_t