Go to the documentation of this file.
123 const std::string &property_class,
125 const exprt &src_expr,
186 args[0].type().id()!=ID_unsignedbv ||
187 args[1].type().id()!=ID_unsignedbv)
188 throw "expected two unsigned arguments to "
191 assert(args[0].type()==args[1].type());
198 if(lhs.
id()==ID_index)
200 else if(lhs.
id()==ID_member)
202 else if(lhs.
id()==ID_symbol)
208 for(assertionst::iterator
213 assertionst::iterator next=it;
241 throw "no zero of argument type of operator "+expr.
id_string();
264 const typet &distance_type=
267 if(distance_type.
id()==ID_signedbv)
274 "shift distance is negative",
281 const typet &op_type=
284 if(op_type.
id()==ID_unsignedbv || op_type.
id()==ID_signedbv)
290 throw "no number for width for operator "+expr.
id_string();
294 "shift distance too large",
300 if(op_type.
id()==ID_signedbv && expr.
id()==ID_shl)
307 "shift operand is negative",
318 "shift of non-integer type",
338 throw "no zero of argument type of operator "+expr.
id_string();
361 if(type.
id()!=ID_signedbv &&
362 type.
id()!=ID_unsignedbv)
365 if(expr.
id()==ID_typecast)
370 throw "typecast takes one operand";
374 if(type.
id()==ID_signedbv)
378 if(old_type.
id()==ID_signedbv)
381 if(new_width>=old_width)
393 and_exprt(no_overflow_lower, no_overflow_upper),
394 "arithmetic overflow on signed type conversion",
400 else if(old_type.
id()==ID_unsignedbv)
403 if(new_width>=old_width+1)
413 "arithmetic overflow on unsigned to signed type conversion",
419 else if(old_type.
id()==ID_floatbv)
433 and_exprt(no_overflow_lower, no_overflow_upper),
434 "arithmetic overflow on float to signed integer type conversion",
441 else if(type.
id()==ID_unsignedbv)
445 if(old_type.
id()==ID_signedbv)
449 if(new_width>=old_width-1)
457 "arithmetic overflow on signed to unsigned type conversion",
473 and_exprt(no_overflow_lower, no_overflow_upper),
474 "arithmetic overflow on signed to unsigned type conversion",
481 else if(old_type.
id()==ID_unsignedbv)
484 if(new_width>=old_width)
492 "arithmetic overflow on unsigned to unsigned type conversion",
498 else if(old_type.
id()==ID_floatbv)
512 and_exprt(no_overflow_lower, no_overflow_upper),
513 "arithmetic overflow on float to unsigned integer type conversion",
542 if(expr.
id()==ID_div)
547 if(type.
id()==ID_signedbv)
557 "arithmetic overflow on signed division",
566 else if(expr.
id()==ID_mod)
571 else if(expr.
id()==ID_unary_minus)
573 if(type.
id()==ID_signedbv)
583 "arithmetic overflow on signed unary minus",
601 for(std::size_t i=1; i<expr.
operands().size(); i++)
618 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
622 "arithmetic overflow on "+kind+
" "+expr.
id_string(),
632 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
636 "arithmetic overflow on "+kind+
" "+expr.
id_string(),
654 if(type.
id()!=ID_floatbv)
659 if(expr.
id()==ID_typecast)
675 "arithmetic overflow on floating-point typecast",
688 "arithmetic overflow on floating-point typecast",
697 else if(expr.
id()==ID_div)
709 "arithmetic overflow on floating-point division",
717 else if(expr.
id()==ID_mod)
722 else if(expr.
id()==ID_unary_minus)
727 else if(expr.
id()==ID_plus || expr.
id()==ID_mult ||
740 expr.
id()==ID_plus?
"addition":
741 expr.
id()==ID_minus?
"subtraction":
742 expr.
id()==ID_mult?
"multiplication":
"";
746 "arithmetic overflow on floating-point "+kind,
756 assert(expr.
id()!=ID_minus);
774 if(expr.
type().
id()!=ID_floatbv)
777 if(expr.
id()!=ID_plus &&
778 expr.
id()!=ID_mult &&
787 if(expr.
id()==ID_div)
800 isnan=
or_exprt(zero_div_zero, div_inf);
802 else if(expr.
id()==ID_mult)
818 isnan=
or_exprt(inf_times_zero, zero_times_inf);
820 else if(expr.
id()==ID_plus)
842 else if(expr.
id()==ID_minus)
881 throw expr.
id_string()+
" takes two arguments";
894 "same object violation",
910 if(expr.
id()==ID_plus ||
920 "pointer arithmetic overflow on "+expr.
id_string(),
941 for(
const auto &c : conditions)
945 "dereference failure: "+c.description,
946 "pointer dereference",
972 return {
conditiont(not_eq_null,
"reference is null")};
992 alloc_disjuncts.push_back(
and_exprt(lb_check, ub_check));
1007 "pointer invalid"));
1014 "pointer uninitialized"));
1021 "deallocated dynamic object"));
1032 const or_exprt dynamic_bounds_violation(
1038 "pointer outside dynamic object bounds"));
1045 const or_exprt object_bounds_violation(
1051 "pointer outside object bounds"));
1058 "invalid integer address"));
1083 if(array_type.
id()==ID_pointer)
1084 throw "index got pointer as array type";
1085 else if(array_type.
id()==ID_incomplete_array)
1086 throw "index got incomplete array";
1087 else if(array_type.
id()!=ID_array && array_type.
id()!=ID_vector)
1088 throw "bounds check expected array or vector type, got "
1097 if(index.
type().
id()!=ID_unsignedbv)
1100 if(index.
id()==ID_typecast &&
1108 const auto i = numeric_cast<mp_integer>(index);
1110 if(!i.has_value() || *i < 0)
1118 assert(p_offset.
type()==effective_offset.
type());
1120 effective_offset=
plus_exprt(p_offset, effective_offset);
1131 name+
" lower bound",
1144 const exprt &pointer=
1154 assert(effective_offset.
op0().
type()==effective_offset.
op1().
type());
1155 if(effective_offset.
type()!=size.
type())
1168 name+
" dynamic object upper bound",
1182 const exprt &size=array_type.
id()==ID_array ?
1191 else if(size.
id()==ID_infinity)
1214 name +
" upper bound",
1234 name+
" upper bound",
1245 const std::string &property_class,
1247 const exprt &src_expr,
1266 new_expr.
swap(expr);
1280 std::string source_expr_string;
1283 t->guard.swap(new_expr);
1284 t->source_location=source_location;
1286 t->source_location.set_property_class(property_class);
1293 if(expr.
id()==ID_exists || expr.
id()==ID_forall)
1298 if(expr.
id()==ID_dereference)
1303 else if(expr.
id()==ID_index)
1317 if(expr.
id()==ID_address_of)
1323 else if(expr.
id()==ID_and || expr.
id()==ID_or)
1326 throw "`"+expr.
id_string()+
"' must be Boolean, but got "+
1331 for(
const auto &op : expr.
operands())
1333 if(!op.is_boolean())
1334 throw "`"+expr.
id_string()+
"' takes Boolean operands only, but got "+
1339 if(expr.
id()==ID_or)
1345 guard.
swap(old_guard);
1349 else if(expr.
id()==ID_if)
1352 throw "if takes three arguments";
1357 "first argument of if must be boolean, but got "
1368 guard.
swap(old_guard);
1375 guard.
swap(old_guard);
1380 else if(expr.
id()==ID_member &&
1404 const exprt char_pointer =
1412 char_pointer.
type());
1414 const exprt new_address_casted =
1428 if(expr.
id()==ID_index)
1432 else if(expr.
id()==ID_div)
1436 if(expr.
type().
id()==ID_signedbv)
1438 else if(expr.
type().
id()==ID_floatbv)
1444 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr)
1448 if(expr.
id()==ID_shl && expr.
type().
id()==ID_signedbv)
1451 else if(expr.
id()==ID_mod)
1455 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
1456 expr.
id()==ID_mult ||
1457 expr.
id()==ID_unary_minus)
1459 if(expr.
type().
id()==ID_signedbv ||
1460 expr.
type().
id()==ID_unsignedbv)
1468 else if(expr.
type().
id()==ID_floatbv)
1473 else if(expr.
type().
id()==ID_pointer)
1478 else if(expr.
id()==ID_typecast)
1480 else if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1481 expr.
id()==ID_ge || expr.
id()==ID_gt)
1483 else if(expr.
id()==ID_dereference)
1501 if(expr.
id() == ID_r_ok || expr.
id() == ID_w_ok)
1505 expr.
operands().size() == 2,
"r/w_ok must have two operands");
1509 for(
const auto &c : conditions)
1510 conjuncts.push_back(c.assertion);
1523 bool did_something =
false;
1527 util_make_unique<local_bitvector_analysist>(goto_function);
1560 t->source_location.set_comment(
"error label "+label);
1561 t->source_location.set(
"user-provided",
true);
1569 if(statement==ID_expression)
1573 else if(statement==ID_printf)
1598 !code_function_call.
arguments().empty() &&
1615 "this is null on method invocation",
1616 "pointer dereference",
1623 for(
const auto &op : code_function_call.
operands())
1654 "pointer dereference",
1674 did_something =
true;
1682 did_something =
true;
1722 t->make_assignment();
1733 "dynamically allocated memory never freed",
1743 if(i_it->source_location.is_nil())
1745 i_it->source_location.id(
irep_idt());
1747 if(!it->source_location.get_file().empty())
1748 i_it->source_location.set_file(it->source_location.get_file());
1750 if(!it->source_location.get_line().empty())
1751 i_it->source_location.set_line(it->source_location.get_line());
1753 if(!it->source_location.get_function().empty())
1754 i_it->source_location.set_function(
1755 it->source_location.get_function());
1757 if(!it->source_location.get_column().empty())
1758 i_it->source_location.set_column(it->source_location.get_column());
1760 if(!it->source_location.get_java_bytecode_index().empty())
1761 i_it->source_location.set_java_bytecode_index(
1762 it->source_location.get_java_bytecode_index());
1765 if(i_it->function.empty())
1766 i_it->function=it->function;
1801 goto_check.collect_allocations(goto_functions);
std::pair< exprt, exprt > allocationt
std::list< allocationt > allocationst
#define Forall_goto_program_instructions(it, program)
std::string array_name(const exprt &)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::string array_name(const namespacet &ns, const exprt &expr)
static exprt conditional_cast(const exprt &expr, const typet &type)
#define PRECONDITION(CONDITION)
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
goto_programt::const_targett current_target
void rw_ok_check(exprt &)
expand the r_ok and w_ok predicates
const irep_idt & get_property_class() const
source_locationt source_location
The location of the instruction in the source file.
const typet & subtype() const
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
void bounds_check(const index_exprt &, const guardt &)
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
void set_comment(const irep_idt &comment)
const exprt & size() const
bool enable_div_by_zero_check
bool enable_undefined_shift_check
void check_rec(const exprt &expr, guardt &guard, bool address)
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
void set_function(const irep_idt &function)
std::string comment(const rw_set_baset::entryt &entry, bool write)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
exprt null_pointer(const exprt &pointer)
The type of an expression, extends irept.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void pointer_rel_check(const exprt &, const guardt &)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
typet type
Type of symbol.
Operator to dereference a pointer.
bool is_dynamic_heap() const
void add(const exprt &expr)
The trinary if-then-else operator.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
bool enable_built_in_assertions
bool enable_assert_to_assume
Split an expression into a base object and a (byte) offset.
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
const irept & find(const irep_namet &name) const
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
The plus expression Associativity is not specified.
Base class for all expressions.
bool enable_conversion_check
void goto_check(goto_functiont &goto_function, const irep_idt &mode)
std::list< conditiont > conditionst
std::list< std::string > value_listt
exprt dynamic_object(const exprt &pointer)
bool is_true() const
Return whether the expression is a constant representing true.
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
exprt object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
void pointer_validity_check(const dereference_exprt &, const guardt &)
Expression to hold a symbol (variable)
void nan_check(const exprt &, const guardt &)
bool enable_memory_leak_check
#define UNREACHABLE
This should be used to mark dead code.
bool enable_unsigned_overflow_check
bool enable_float_overflow_check
void mod_by_zero_check(const mod_exprt &, const guardt &)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
targett add_instruction()
Adds an instruction at the end.
typet & type()
Return the type of the expression.
void pointer_overflow_check(const exprt &, const guardt &)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
void check(const exprt &expr)
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
conditionst address_check(const exprt &address, const exprt &size)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
exprt size_of_expr(const typet &type, const namespacet &ns)
The null pointer constant.
void float_overflow_check(const exprt &, const guardt &)
bool enable_pointer_check
void add_guarded_claim(const exprt &expr, const std::string &comment, const std::string &property_class, const source_locationt &, const exprt &src_expr, const guardt &guard)
#define forall_operands(it, expr)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
const exprt & struct_op() const
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
const irep_idt & get_identifier() const
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
bool is_integer_address() const
exprt deallocated(const exprt &pointer, const namespacet &ns)
exprt dynamic_object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
const std::string & id_string() const
bool simplify(exprt &expr, const namespacet &ns)
exprt dead_object(const exprt &pointer, const namespacet &ns)
std::set< exprt > assertionst
exprt integer_address(const exprt &pointer)
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
pointer_typet pointer_type(const typet &subtype)
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
exprt object_size(const exprt &pointer)
bool is_static_lifetime() const
const irep_idt & id() const
bool is_end_function() const
const code_function_callt & to_code_function_call(const codet &code)
A goto function, consisting of function type (see type), function body (see body),...
std::vector< exprt > operandst
exprt::operandst argumentst
The Boolean constant false.
void collect_allocations(const goto_functionst &goto_functions)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const exprt & root_object() const
bool is_dynamic_local() const
void from_integer(const mp_integer &i)
void undefined_shift_check(const shift_exprt &, const guardt &)
void div_by_zero_check(const div_exprt &, const guardt &)
exprt pointer_offset(const exprt &pointer)
goto_functionst::goto_functiont goto_functiont
error_labelst error_labels
#define Forall_goto_functions(it, functions)
void clear()
Clear the goto program.
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
bitvector_typet char_type()
std::size_t get_width() const
A side_effect_exprt that returns a non-deterministically chosen value.
::goto_functiont goto_functiont
exprt malloc_object(const exprt &pointer, const namespacet &ns)
bool is_zero() const
Return whether the expression is a constant representing 0.
bool has_symbol(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
Extract member of struct or union.
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
A collection of goto functions.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
A base class for shift operators.
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
goto_functionst goto_functions
GOTO functions.
std::unordered_set< irep_idt > find_symbols_sett
irep_idt function
The function this instruction belongs to.
const code_assignt & to_code_assign(const codet &code)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
Evaluates to true if the operand is infinite.
void invalidate(const exprt &lhs)
bool get_bool_option(const std::string &option) const
bool enable_signed_overflow_check
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
A base class for relations, i.e., binary predicates.
exprt guard
Guard for gotos, assume, assert.
void integer_overflow_check(const exprt &, const guardt &)
bool is_uninitialized() const
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
exprt same_object(const exprt &p1, const exprt &p2)
exprt object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
exprt invalid_pointer(const exprt &pointer)
A generic container class for the GOTO intermediate representation of one function.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
#define forall_goto_functions(it, functions)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
instructionst::const_iterator const_targett
constant_exprt to_expr() const
optionst::value_listt error_labelst
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Operator to return the address of an object.
source_locationt & add_source_location()
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Semantic type conversion.
signedbv_typet pointer_diff_type()
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
bool enable_pointer_overflow_check
A codet representing an assignment in the program.
The Boolean constant true.
const irep_idt & get_statement() const
IEEE-floating-point equality.
bool is_function_call() const
bool is_boolean() const
Return whether the expression represents a Boolean.
This class represents an instruction in the GOTO intermediate representation.
bool is_target() const
Is this node a branch target?
const source_locationt & source_location() const
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
conditiont(const exprt &_assertion, const std::string &_description)
exprt dynamic_size(const namespacet &ns)
symbol_tablet symbol_table
Symbol table.
const value_listt & get_list_option(const std::string &option) const
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
goto_checkt(const namespacet &_ns, const optionst &_options)
void conversion_check(const exprt &, const guardt &)
instructionst::iterator targett
#define forall_goto_program_instructions(it, program)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
void set_property_class(const irep_idt &property_class)