122 const std::string &property_class,
124 const exprt &src_expr,
185 args[0].type().id()!=ID_unsignedbv ||
186 args[1].type().id()!=ID_unsignedbv)
187 throw "expected two unsigned arguments to " 190 assert(args[0].type()==args[1].type());
197 if(lhs.
id()==ID_index)
199 else if(lhs.
id()==ID_member)
201 else if(lhs.
id()==ID_symbol)
207 for(assertionst::iterator
212 assertionst::iterator next=it;
240 throw "no zero of argument type of operator "+expr.
id_string();
263 const typet &distance_type=
266 if(distance_type.
id()==ID_signedbv)
273 "shift distance is negative",
280 const typet &op_type=
283 if(op_type.
id()==ID_unsignedbv || op_type.
id()==ID_signedbv)
289 throw "no number for width for operator "+expr.
id_string();
292 expr.
distance(), ID_lt, width_expr);
296 "shift distance too large",
302 if(op_type.
id()==ID_signedbv && expr.
id()==ID_shl)
309 "shift operand is negative",
320 "shift of non-integer type",
340 throw "no zero of argument type of operator "+expr.
id_string();
363 if(type.
id()!=ID_signedbv &&
364 type.
id()!=ID_unsignedbv)
367 if(expr.
id()==ID_typecast)
372 throw "typecast takes one operand";
376 if(type.
id()==ID_signedbv)
380 if(old_type.
id()==ID_signedbv)
383 if(new_width>=old_width)
395 and_exprt(no_overflow_lower, no_overflow_upper),
396 "arithmetic overflow on signed type conversion",
402 else if(old_type.
id()==ID_unsignedbv)
405 if(new_width>=old_width+1)
415 "arithmetic overflow on unsigned to signed type conversion",
421 else if(old_type.
id()==ID_floatbv)
430 lower.from_integer(-
power(2, new_width-1)-1);
432 expr.
op0(), ID_gt, lower.to_expr());
435 and_exprt(no_overflow_lower, no_overflow_upper),
436 "arithmetic overflow on float to signed integer type conversion",
443 else if(type.
id()==ID_unsignedbv)
447 if(old_type.
id()==ID_signedbv)
451 if(new_width>=old_width-1)
459 "arithmetic overflow on signed to unsigned type conversion",
475 and_exprt(no_overflow_lower, no_overflow_upper),
476 "arithmetic overflow on signed to unsigned type conversion",
483 else if(old_type.
id()==ID_unsignedbv)
486 if(new_width>=old_width)
494 "arithmetic overflow on unsigned to unsigned type conversion",
500 else if(old_type.
id()==ID_floatbv)
509 lower.from_integer(-1);
511 expr.
op0(), ID_gt, lower.to_expr());
514 and_exprt(no_overflow_lower, no_overflow_upper),
515 "arithmetic overflow on float to unsigned integer type conversion",
544 if(expr.
id()==ID_div)
549 if(type.
id()==ID_signedbv)
559 "arithmetic overflow on signed division",
568 else if(expr.
id()==ID_mod)
573 else if(expr.
id()==ID_unary_minus)
575 if(type.
id()==ID_signedbv)
585 "arithmetic overflow on signed unary minus",
603 for(std::size_t i=1; i<expr.
operands().size(); i++)
615 overflow.operands().resize(2);
620 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
624 "arithmetic overflow on "+kind+
" "+expr.
id_string(),
634 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
638 "arithmetic overflow on "+kind+
" "+expr.
id_string(),
656 if(type.
id()!=ID_floatbv)
661 if(expr.
id()==ID_typecast)
677 "arithmetic overflow on floating-point typecast",
690 "arithmetic overflow on floating-point typecast",
699 else if(expr.
id()==ID_div)
711 "arithmetic overflow on floating-point division",
719 else if(expr.
id()==ID_mod)
724 else if(expr.
id()==ID_unary_minus)
729 else if(expr.
id()==ID_plus || expr.
id()==ID_mult ||
742 expr.
id()==ID_plus?
"addition":
743 expr.
id()==ID_minus?
"subtraction":
744 expr.
id()==ID_mult?
"multiplication":
"";
748 "arithmetic overflow on floating-point "+kind,
758 assert(expr.
id()!=ID_minus);
776 if(expr.
type().
id()!=ID_floatbv)
779 if(expr.
id()!=ID_plus &&
780 expr.
id()!=ID_mult &&
789 if(expr.
id()==ID_div)
802 isnan=
or_exprt(zero_div_zero, div_inf);
804 else if(expr.
id()==ID_mult)
820 isnan=
or_exprt(inf_times_zero, zero_times_inf);
822 else if(expr.
id()==ID_plus)
844 else if(expr.
id()==ID_minus)
885 throw expr.
id_string()+
" takes two arguments";
898 "same object violation",
914 if(expr.
id()==ID_plus ||
924 "pointer arithmetic overflow on "+expr.
id_string(),
945 for(
const auto &c : conditions)
949 "dereference failure: "+c.description,
950 "pointer dereference",
972 if(flags.is_unknown() || flags.is_null())
976 return {
conditiont(not_eq_null,
"reference is null")};
996 alloc_disjuncts.push_back(
and_exprt(lb_check, ub_check));
1001 if(flags.is_unknown() || flags.is_null())
1007 if(flags.is_unknown())
1011 "pointer invalid"));
1014 if(flags.is_uninitialized())
1018 "pointer uninitialized"));
1021 if(flags.is_unknown() || flags.is_dynamic_heap())
1025 "deallocated dynamic object"));
1028 if(flags.is_unknown() || flags.is_dynamic_local())
1034 if(flags.is_unknown() || flags.is_dynamic_heap())
1036 const or_exprt dynamic_bounds_violation(
1042 "pointer outside dynamic object bounds"));
1046 flags.is_unknown() || flags.is_dynamic_local() ||
1047 flags.is_static_lifetime())
1049 const or_exprt object_bounds_violation(
1055 "pointer outside object bounds"));
1058 if(flags.is_unknown() || flags.is_integer_address())
1062 "invalid integer address"));
1087 if(array_type.
id()==ID_pointer)
1088 throw "index got pointer as array type";
1089 else if(array_type.
id()==ID_incomplete_array)
1090 throw "index got incomplete array";
1091 else if(array_type.
id()!=ID_array && array_type.
id()!=ID_vector)
1092 throw "bounds check expected array or vector type, got " 1101 if(index.type().id()!=ID_unsignedbv)
1104 if(index.id()==ID_typecast &&
1105 index.operands().size()==1 &&
1106 index.op0().type().id()==ID_unsignedbv)
1126 assert(p_offset.
type()==effective_offset.
type());
1128 effective_offset=
plus_exprt(p_offset, effective_offset);
1139 name+
" lower bound",
1152 const exprt &pointer=
1162 assert(effective_offset.op0().type()==effective_offset.op1().type());
1163 if(effective_offset.type()!=size.
type())
1176 name+
" dynamic object upper bound",
1183 if(type_size.is_not_nil())
1190 const exprt &size=array_type.
id()==ID_array ?
1199 else if(size.
id()==ID_infinity)
1222 name +
" upper bound",
1242 name+
" upper bound",
1253 const std::string &property_class,
1255 const exprt &src_expr,
1274 new_expr.
swap(expr);
1288 std::string source_expr_string;
1291 t->guard.swap(new_expr);
1292 t->source_location=source_location;
1293 t->source_location.set_comment(
comment+
" in "+source_expr_string);
1294 t->source_location.set_property_class(property_class);
1301 if(expr.
id()==ID_exists || expr.
id()==ID_forall)
1306 if(expr.
id()==ID_dereference)
1311 else if(expr.
id()==ID_index)
1325 if(expr.
id()==ID_address_of)
1331 else if(expr.
id()==ID_and || expr.
id()==ID_or)
1334 throw "`"+expr.
id_string()+
"' must be Boolean, but got "+
1339 for(
const auto &op : expr.
operands())
1341 if(!op.is_boolean())
1342 throw "`"+expr.
id_string()+
"' takes Boolean operands only, but got "+
1347 if(expr.
id()==ID_or)
1353 guard.
swap(old_guard);
1357 else if(expr.
id()==ID_if)
1360 throw "if takes three arguments";
1365 "first argument of if must be boolean, but got " 1376 guard.
swap(old_guard);
1383 guard.
swap(old_guard);
1388 else if(expr.
id()==ID_member &&
1412 const exprt char_pointer =
1420 char_pointer.
type());
1422 const exprt new_address_casted =
1436 if(expr.
id()==ID_index)
1440 else if(expr.
id()==ID_div)
1444 if(expr.
type().
id()==ID_signedbv)
1446 else if(expr.
type().
id()==ID_floatbv)
1452 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr)
1456 if(expr.
id()==ID_shl && expr.
type().
id()==ID_signedbv)
1459 else if(expr.
id()==ID_mod)
1463 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
1464 expr.
id()==ID_mult ||
1465 expr.
id()==ID_unary_minus)
1467 if(expr.
type().
id()==ID_signedbv ||
1468 expr.
type().
id()==ID_unsignedbv)
1476 else if(expr.
type().
id()==ID_floatbv)
1481 else if(expr.
type().
id()==ID_pointer)
1486 else if(expr.
id()==ID_typecast)
1488 else if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1489 expr.
id()==ID_ge || expr.
id()==ID_gt)
1491 else if(expr.
id()==ID_dereference)
1509 if(expr.
id() == ID_r_ok || expr.
id() == ID_w_ok)
1513 expr.
operands().size() == 2,
"r/w_ok must have two operands");
1517 for(
const auto &c : conditions)
1518 conjuncts.push_back(c.assertion);
1531 bool did_something =
false;
1566 t->source_location.set_property_class(
"error label");
1567 t->source_location.set_comment(
"error label "+label);
1568 t->source_location.set(
"user-provided",
true);
1576 if(statement==ID_expression)
1580 else if(statement==ID_printf)
1605 !code_function_call.
arguments().empty() &&
1622 "this is null on method invocation",
1623 "pointer dereference",
1661 "pointer dereference",
1681 did_something =
true;
1689 did_something =
true;
1729 t->make_assignment();
1740 "dynamically allocated memory never freed",
1750 if(i_it->source_location.is_nil())
1752 i_it->source_location.id(
irep_idt());
1754 if(!it->source_location.get_file().empty())
1755 i_it->source_location.set_file(it->source_location.get_file());
1757 if(!it->source_location.get_line().empty())
1758 i_it->source_location.set_line(it->source_location.get_line());
1760 if(!it->source_location.get_function().empty())
1761 i_it->source_location.set_function(
1762 it->source_location.get_function());
1764 if(!it->source_location.get_column().empty())
1765 i_it->source_location.set_column(it->source_location.get_column());
1767 if(!it->source_location.get_java_bytecode_index().empty())
1768 i_it->source_location.set_java_bytecode_index(
1769 it->source_location.get_java_bytecode_index());
1772 if(i_it->function.empty())
1773 i_it->function=it->function;
1808 goto_check.collect_allocations(goto_functions);
exprt guard
Guard for gotos, assume, assert.
void nan_check(const exprt &, const guardt &)
const irep_idt & get_statement() const
irep_idt function
The function this instruction belongs to.
The type of an expression.
exprt size_of_expr(const typet &type, const namespacet &ns)
bool enable_div_by_zero_check
void set_function(const irep_idt &function)
void rw_ok_check(exprt &)
expand the r_ok and w_ok predicates
void goto_check(goto_functiont &goto_function, const irep_idt &mode)
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
conditiont(const exprt &_assertion, const std::string &_description)
A generic base class for relations, i.e., binary predicates.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
pointer_typet pointer_type(const typet &subtype)
void bounds_check(const index_exprt &, const guardt &)
bool enable_signed_overflow_check
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
constant_exprt to_expr() const
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
goto_checkt(const namespacet &_ns, const optionst &_options)
std::string comment(const rw_set_baset::entryt &entry, bool write)
exprt object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
bool enable_assert_to_assume
bool is_function_call() const
Evaluates to true if the operand is infinite.
Deprecated expression utility functions.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
bool enable_float_overflow_check
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
local_bitvector_analysist * local_bitvector_analysis
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
void move_to_operands(exprt &expr)
The null pointer constant.
bool enable_undefined_shift_check
const exprt & root_object() const
The trinary if-then-else operator.
exprt::operandst argumentst
Field-insensitive, location-sensitive bitvector analysis.
const value_listt & get_list_option(const std::string &option) const
bool enable_unsigned_overflow_check
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
bool get_bool(const irep_namet &name) const
signedbv_typet pointer_diff_type()
exprt deallocated(const exprt &pointer, const namespacet &ns)
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Extract member of struct or union.
conditionst address_check(const exprt &address, const exprt &size)
This class represents an instruction in the GOTO intermediate representation.
void clear()
Clear the goto program.
exprt conjunction(const exprt::operandst &op)
void pointer_rel_check(const exprt &, const guardt &)
bool is_end_function() const
const code_assignt & to_code_assign(const codet &code)
goto_programt::const_targett t
std::list< allocationt > allocationst
exprt object_size(const exprt &pointer)
const irep_idt & id() const
void mod_by_zero_check(const mod_exprt &, const guardt &)
bool enable_memory_leak_check
void check(const exprt &expr)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
bool enable_conversion_check
The boolean constant true.
division (integer and real)
constant_exprt smallest_expr() const
instructionst::iterator targett
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
const source_locationt & find_source_location() const
Operator to dereference a pointer.
void undefined_shift_check(const shift_exprt &, const guardt &)
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
bool get_bool_option(const std::string &option) const
exprt integer_address(const exprt &pointer)
const irep_idt & get(const irep_namet &name) const
instructionst::const_iterator const_targett
std::list< std::string > value_listt
::goto_functiont goto_functiont
Abstract interface to support a programming language.
const exprt & size() const
#define PRECONDITION(CONDITION)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
A side effect that returns a non-deterministically chosen value.
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
split an expression into a base object and a (byte) offset
const exprt & size() const
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
exprt object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
void collect_allocations(const goto_functionst &goto_functions)
const typet & follow(const typet &) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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)
Operator to return the address of an object.
error_labelst error_labels
void pointer_overflow_check(const exprt &, const guardt &)
Various predicates over pointers in programs.
exprt dynamic_object_lower_bound(const exprt &pointer, const namespacet &ns, const exprt &offset)
bool has_symbol(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
The boolean constant false.
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
std::size_t get_width() const
exprt disjunction(const exprt::operandst &op)
static exprt conditional_cast(const exprt &expr, const typet &type)
std::vector< exprt > operandst
std::list< conditiont > conditionst
A generic container class for the GOTO intermediate representation of one function.
exprt malloc_object(const exprt &pointer, const namespacet &ns)
flagst get(const goto_programt::const_targett t, const exprt &src)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
void pointer_validity_check(const dereference_exprt &, const guardt &)
typet type
Type of symbol.
static irep_idt entry_point()
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
void float_overflow_check(const exprt &, const guardt &)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
exprt dynamic_size(const namespacet &ns)
source_locationt source_location
The location of the instruction in the source file.
targett add_instruction()
Adds an instruction at the end.
exprt invalid_pointer(const exprt &pointer)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
const exprt & struct_op() const
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
exprt pointer_offset(const exprt &pointer)
bool enable_pointer_check
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
std::set< exprt > assertionst
bool enable_built_in_assertions
const std::string & id_string() const
void from_integer(const mp_integer &i)
goto_programt & goto_program
source_locationt & add_source_location()
#define Forall_goto_program_instructions(it, program)
bool enable_pointer_overflow_check
goto_functionst::goto_functiont goto_functiont
std::pair< exprt, exprt > allocationt
void integer_overflow_check(const exprt &, const guardt &)
Expression to hold a symbol (variable)
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
exprt dynamic_object(const exprt &pointer)
std::unordered_set< irep_idt > find_symbols_sett
exprt null_pointer(const exprt &pointer)
void div_by_zero_check(const div_exprt &, const guardt &)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
#define forall_goto_functions(it, functions)
std::string array_name(const exprt &)
optionst::value_listt error_labelst
exprt dead_object(const exprt &pointer, const namespacet &ns)
const irep_idt & get_property_class() const
#define forall_goto_program_instructions(it, program)
exprt same_object(const exprt &p1, const exprt &p2)
bool is_target() const
Is this node a branch target?
void check_rec(const exprt &expr, guardt &guard, bool address)
void make_typecast(const typet &_type)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const irept & find(const irep_namet &name) const
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
A base class for shift operators.
goto_functionst goto_functions
GOTO functions.
bitvector_typet char_type()
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void conversion_check(const exprt &, const guardt &)
void add(const exprt &expr)
void invalidate(const exprt &lhs)
std::string array_name(const namespacet &ns, const exprt &expr)
const code_function_callt & to_code_function_call(const codet &code)
bool simplify(exprt &expr, const namespacet &ns)
IEEE-floating-point equality.