49 if(!it->labels.empty())
51 for(
auto label : it->labels)
61 instruction.is_catch() &&
69 if(instruction.targets.empty())
109 std::unordered_map<irep_idt, symbolt, irep_id_hash> &
label_flags,
162 const auto flag = [&]() ->
symbolt {
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();
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);
254 std::unordered_map<irep_idt, symbolt, irep_id_hash>
label_flags;
270 i.
code().find_source_location());
284 i.
code().find_source_location());
295 targets.scope_stack.get_nearest_common_ancestor_info(
333 <<
"' that enters one or more lexical blocks; "
334 <<
"adding declaration code on jump to '" <<
goto_label <<
"'"
378 for(
const auto &label :
targets.labels)
411 i.get_target()->target_number = (++
cnt);
433 if(it->get_target()->target_number ==
it_z->target_number)
439 "no loop invariant expected");
508 "code() in magic thread creation label is null");
525 {label, {target,
targets.scope_stack.get_current_node()}});
526 target->labels.push_front(label);
557 targets.cases.push_back(std::make_pair(target,
caset()));
559 targets.cases_map.insert(std::make_pair(target, --
targets.cases.end()))
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"
648 else if(statement ==
ID_for)
678 else if(statement ==
ID_cpp_delete || statement ==
"cpp_delete[]")
694 else if(statement ==
ID_asm)
711 for(
const auto &op : code.
operands())
820 tmp.operands().resize(1);
822 tmp.add_source_location().set_hide();
864 destructor.
arguments().push_back(this_expr);
866 targets.scope_stack.add(destructor, {});
890 rhs.operands().size() == 2,
891 "function_call sideeffect takes two operands",
892 rhs.find_source_location());
974 "cpp_delete statement takes one operand",
983 const exprt &destructor =
1019 "delete statement takes 1 parameter");
1076 if(assigns.is_not_nil())
1078 PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
1084 if(!invariant.is_nil())
1086 PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
1094 PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
1118 if(code.
init().is_not_nil())
1146 if(code.
iter().is_nil())
1158 if(
tmp_x.instructions.empty())
1260 "dowhile takes two operands",
1299 y->complete_goto(
C);
1318 W->complete_goto(
w);
1341 for(
const auto &op : case_op)
1470 case_pair.first, std::move(guard_expr), source_location));
1479 std::move(guard_expr), source_location));
1490 targets.default_target,
targets.default_target->source_location()));
1531 "return takes none or one operand",
1553 "function must return value",
1566 "function must not return value",
1585 "continue without target",
1607 targets.gotos.emplace_back(t,
targets.scope_stack.get_current_node());
1619 targets.computed_gotos.push_back(t);
1636 "end_thread expects no operands",
1646 "atomic_begin expects no operands",
1656 ": atomic_end expects no operands",
1676 code.
cond().id() ==
ID_and && code.
cond().operands().size() == 2 &&
1684 new_if1.add_source_location() = source_location;
1687 new_if0.add_source_location() = source_location;
1730 std::list<exprt> &dest)
1734 dest.push_back(expr);
1739 for(
const auto &op : expr.
operands())
1749 return (!
g.instructions.empty()) &&
1750 ++
g.instructions.begin() ==
g.instructions.end();
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() ==
1875 tmp_y.swap(false_case);
1876 y =
tmp_y.instructions.begin();
1886 tmp_w.swap(true_case);
1890 x->complete_goto(
z);
1922 for(
const auto &op : expr.
operands())
2003 std::list<exprt> op;
2006 for(
const auto &expr : op)
2023 std::list<exprt> op;
2027 for(
const auto &expr : op)
2076 if(op.is_constant())
2083 result +=
static_cast<char>(i.value());
2087 return value =
result,
false;
2107 "expected string constant",
2120 return symbol.
value;
2126 return std::move(
tmp);
2133 return std::move(
tmp);
2141 const std::string &suffix,
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");
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.
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
bool is_false() const
Return whether the expression is a constant representing false.
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.