94 const exprt &access_lb,
95 const exprt &access_ub,
107 const std::string &property_class,
109 const exprt &src_expr,
158 const goto_programt::instructiont &instruction=*it;
159 if(!instruction.is_function_call())
171 args[0].type().id()!=ID_unsignedbv ||
172 args[1].type().id()!=ID_unsignedbv)
173 throw "expected two unsigned arguments to " 176 assert(args[0].type()==args[1].type());
183 if(lhs.
id()==ID_index)
185 else if(lhs.
id()==ID_member)
187 else if(lhs.
id()==ID_symbol)
193 for(assertionst::iterator
198 assertionst::iterator next=it;
227 throw "no zero of argument type of operator "+expr.
id_string();
251 const typet &distance_type=
254 if(distance_type.
id()==ID_signedbv)
261 "shift distance is negative",
268 const typet &op_type=
271 if(op_type.
id()==ID_unsignedbv || op_type.
id()==ID_signedbv)
277 throw "no number for width for operator "+expr.
id_string();
280 expr.
distance(), ID_lt, width_expr);
284 "shift distance too large",
304 throw "no zero of argument type of operator "+expr.
id_string();
328 if(type.
id()!=ID_signedbv &&
329 type.
id()!=ID_unsignedbv)
332 if(expr.
id()==ID_typecast)
337 throw "typecast takes one operand";
341 if(type.
id()==ID_signedbv)
345 if(old_type.
id()==ID_signedbv)
348 if(new_width>=old_width)
352 no_overflow_upper.
lhs()=expr.
op0();
356 no_overflow_lower.
lhs()=expr.
op0();
360 and_exprt(no_overflow_lower, no_overflow_upper),
361 "arithmetic overflow on signed type conversion",
367 else if(old_type.
id()==ID_unsignedbv)
370 if(new_width>=old_width+1)
374 no_overflow_upper.
lhs()=expr.
op0();
379 "arithmetic overflow on unsigned to signed type conversion",
385 else if(old_type.
id()==ID_floatbv)
391 no_overflow_upper.
lhs()=expr.
op0();
397 no_overflow_lower.
lhs()=expr.
op0();
401 and_exprt(no_overflow_lower, no_overflow_upper),
402 "arithmetic overflow on float to signed integer type conversion",
409 else if(type.
id()==ID_unsignedbv)
413 if(old_type.
id()==ID_signedbv)
417 if(new_width>=old_width-1)
421 no_overflow_lower.
lhs()=expr.
op0();
426 "arithmetic overflow on signed to unsigned type conversion",
436 no_overflow_upper.
lhs()=expr.
op0();
440 no_overflow_lower.
lhs()=expr.
op0();
444 and_exprt(no_overflow_lower, no_overflow_upper),
445 "arithmetic overflow on signed to unsigned type conversion",
452 else if(old_type.
id()==ID_unsignedbv)
455 if(new_width>=old_width)
459 no_overflow_upper.
lhs()=expr.
op0();
464 "arithmetic overflow on unsigned to unsigned type conversion",
470 else if(old_type.
id()==ID_floatbv)
476 no_overflow_upper.
lhs()=expr.
op0();
482 no_overflow_lower.
lhs()=expr.
op0();
486 and_exprt(no_overflow_lower, no_overflow_upper),
487 "arithmetic overflow on float to unsigned integer type conversion",
516 if(expr.
id()==ID_div)
521 if(type.
id()==ID_signedbv)
531 "arithmetic overflow on signed division",
540 else if(expr.
id()==ID_mod)
545 else if(expr.
id()==ID_unary_minus)
547 if(type.
id()==ID_signedbv)
557 "arithmetic overflow on signed unary minus",
575 for(
unsigned i=1; i<expr.
operands().size(); i++)
587 overflow.operands().resize(2);
592 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
596 "arithmetic overflow on "+kind+
" "+expr.
id_string(),
606 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
610 "arithmetic overflow on "+kind+
" "+expr.
id_string(),
628 if(type.
id()!=ID_floatbv)
633 if(expr.
id()==ID_typecast)
649 "arithmetic overflow on floating-point typecast",
662 "arithmetic overflow on floating-point typecast",
671 else if(expr.
id()==ID_div)
683 "arithmetic overflow on floating-point division",
691 else if(expr.
id()==ID_mod)
696 else if(expr.
id()==ID_unary_minus)
701 else if(expr.
id()==ID_plus || expr.
id()==ID_mult ||
714 expr.
id()==ID_plus?
"addition":
715 expr.
id()==ID_minus?
"subtraction":
716 expr.
id()==ID_mult?
"multiplication":
"";
720 "arithmetic overflow on floating-point "+kind,
730 assert(expr.
id()!=ID_minus);
748 if(expr.
type().
id()!=ID_floatbv)
751 if(expr.
id()!=ID_plus &&
752 expr.
id()!=ID_mult &&
761 if(expr.
id()==ID_div)
774 isnan=
or_exprt(zero_div_zero, div_inf);
776 else if(expr.
id()==ID_mult)
792 isnan=
or_exprt(inf_times_zero, zero_times_inf);
794 else if(expr.
id()==ID_plus)
816 else if(expr.
id()==ID_minus)
857 throw expr.
id_string()+
" takes two arguments";
870 "same object violation",
886 if(expr.
id()==ID_plus ||
896 "pointer arithmetic overflow on "+expr.
id_string(),
908 const exprt &access_lb,
909 const exprt &access_ub,
936 "pointer dereference",
977 disjuncts.push_back(
and_exprt(lb_check, ub_check));
987 "dereference failure: pointer NULL",
988 "pointer dereference",
997 "dereference failure: pointer invalid",
998 "pointer dereference",
1006 "dereference failure: pointer uninitialized",
1007 "pointer dereference",
1015 "dereference failure: deallocated dynamic object",
1016 "pointer dereference",
1024 "dereference failure: dead object",
1025 "pointer dereference",
1032 exprt dynamic_bounds=
1046 "dereference failure: pointer outside dynamic object bounds",
1047 "pointer dereference",
1057 exprt object_bounds=
1067 "dereference failure: pointer outside object bounds",
1068 "pointer dereference",
1094 if(array_type.
id()==ID_pointer)
1095 throw "index got pointer as array type";
1096 else if(array_type.
id()==ID_incomplete_array)
1097 throw "index got incomplete array";
1098 else if(array_type.
id()!=ID_array && array_type.
id()!=ID_vector)
1099 throw "bounds check expected array or vector type, got " 1108 if(index.type().id()!=ID_unsignedbv)
1111 if(index.id()==ID_typecast &&
1112 index.operands().size()==1 &&
1113 index.op0().type().id()==ID_unsignedbv)
1133 assert(p_offset.
type()==effective_offset.
type());
1135 effective_offset=
plus_exprt(p_offset, effective_offset);
1146 name+
" lower bound",
1159 const exprt &pointer=
1169 assert(effective_offset.op0().type()==effective_offset.op1().type());
1170 if(effective_offset.type()!=size.
type())
1183 name+
" dynamic object upper bound",
1190 if(type_size.is_not_nil())
1197 const exprt &size=array_type.
id()==ID_array ?
1206 else if(size.
id()==ID_infinity)
1228 name+
" upper bound",
1239 const std::string &property_class,
1241 const exprt &src_expr,
1260 new_expr.
swap(expr);
1274 std::string source_expr_string=
from_expr(
ns,
"", src_expr);
1276 t->guard.swap(new_expr);
1277 t->source_location=source_location;
1278 t->source_location.set_comment(
comment+
" in "+source_expr_string);
1279 t->source_location.set_property_class(property_class);
1290 if(expr.
id()==ID_exists || expr.
id()==ID_forall)
1295 if(expr.
id()==ID_dereference)
1300 else if(expr.
id()==ID_index)
1314 if(expr.
id()==ID_address_of)
1320 else if(expr.
id()==ID_and || expr.
id()==ID_or)
1323 throw "`"+expr.
id_string()+
"' must be Boolean, but got "+
1328 for(
const auto &op : expr.
operands())
1330 if(!op.is_boolean())
1331 throw "`"+expr.
id_string()+
"' takes Boolean operands only, but got "+
1336 if(expr.
id()==ID_or)
1342 guard.
swap(old_guard);
1346 else if(expr.
id()==ID_if)
1349 throw "if takes three arguments";
1354 "first argument of if must be boolean, but got " 1365 guard.
swap(old_guard);
1372 guard.
swap(old_guard);
1377 else if(expr.
id()==ID_member &&
1402 if(expr.
id()==ID_index)
1406 else if(expr.
id()==ID_div)
1410 if(expr.
type().
id()==ID_signedbv)
1412 else if(expr.
type().
id()==ID_floatbv)
1418 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr)
1422 else if(expr.
id()==ID_mod)
1426 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
1427 expr.
id()==ID_mult ||
1428 expr.
id()==ID_unary_minus)
1430 if(expr.
type().
id()==ID_signedbv ||
1431 expr.
type().
id()==ID_unsignedbv)
1439 else if(expr.
type().
id()==ID_floatbv)
1444 else if(expr.
type().
id()==ID_pointer)
1449 else if(expr.
id()==ID_typecast)
1451 else if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1452 expr.
id()==ID_ge || expr.
id()==ID_gt)
1454 else if(expr.
id()==ID_dereference)
1483 goto_programt::instructiont &i=*it;
1494 check(i.guard, mode);
1499 if(std::find(i.labels.begin(), i.labels.end(), label)!=i.labels.end())
1507 t->source_location=i.source_location;
1508 t->source_location.set_property_class(
"error label");
1509 t->source_location.set_comment(
"error label "+label);
1510 t->source_location.set(
"user-provided",
true);
1516 const irep_idt &statement=i.code.get(ID_statement);
1518 if(statement==ID_expression)
1520 check(i.code, mode);
1522 else if(statement==ID_printf)
1528 else if(i.is_assign())
1538 else if(i.is_function_call())
1547 !code_function_call.
arguments().empty() &&
1564 "this is null on method invocation",
1565 "pointer dereference",
1578 else if(i.is_return())
1580 if(i.code.operands().size()==1)
1582 check(i.code.op0(), mode);
1587 else if(i.is_throw())
1589 if(i.code.get_statement()==ID_expression &&
1590 i.code.operands().size()==1 &&
1591 i.code.op0().operands().size()==1)
1598 "java::java.lang.AssertionError")
1607 "pointer dereference",
1617 else if(i.is_assert())
1619 bool is_user_provided=i.source_location.get_bool(
"user-provided");
1621 i.source_location.get_property_class()!=
"error label") ||
1625 else if(i.is_assume())
1630 else if(i.is_dead())
1634 assert(i.code.operands().size()==1);
1652 t->source_location=i.source_location;
1654 t->code.add_source_location()=i.source_location;
1658 else if(i.is_end_function())
1668 t->make_assignment();
1679 "dynamically allocated memory never freed",
1689 if(i_it->source_location.is_nil())
1691 i_it->source_location.id(
irep_idt());
1693 if(!it->source_location.get_file().empty())
1694 i_it->source_location.set_file(it->source_location.get_file());
1696 if(!it->source_location.get_line().empty())
1697 i_it->source_location.set_line(it->source_location.get_line());
1699 if(!it->source_location.get_function().empty())
1700 i_it->source_location.set_function(
1701 it->source_location.get_function());
1703 if(!it->source_location.get_column().empty())
1704 i_it->source_location.set_column(it->source_location.get_column());
1707 if(i_it->function.empty())
1708 i_it->function=it->function;
1738 goto_check.collect_allocations(goto_functions);
The type of an expression.
exprt size_of_expr(const typet &type, const namespacet &ns)
const typet & follow(const typet &src) const
goto_program_instruction_typet
The type of an instruction in a GOTO program.
bool enable_div_by_zero_check
void set_function(const irep_idt &function)
void pointer_validity_check(const dereference_exprt &expr, const guardt &guard, const exprt &access_lb, const exprt &access_ub, const irep_idt &mode)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
void pointer_rel_check(const exprt &expr, const guardt &guard)
void goto_check(goto_functiont &goto_function, const irep_idt &mode)
targett add_instruction()
Adds an instruction at the end.
bool is_uninitialized() const
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
A generic base class for relations, i.e., binary predicates.
pointer_typet pointer_type(const typet &subtype)
bool is_dynamic_heap() const
bool enable_signed_overflow_check
bool is_static_lifetime() const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
constant_exprt to_expr() const
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
void clear()
Clear the goto program.
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
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
bool enable_float_overflow_check
void goto_check(const namespacet &ns, const optionst &options, goto_functionst::goto_functiont &goto_function)
void copy_to_operands(const exprt &expr)
local_bitvector_analysist * local_bitvector_analysis
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
void move_to_operands(exprt &expr)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
void undefined_shift_check(const shift_exprt &expr, const guardt &guard)
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.
void bounds_check(const index_exprt &expr, const guardt &guard)
const value_listt & get_list_option(const std::string &option) const
bool enable_unsigned_overflow_check
void nan_check(const exprt &expr, const guardt &guard)
symbol_tablet 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
exprt deallocated(const exprt &pointer, const namespacet &ns)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Extract member of struct or union.
std::unordered_set< irep_idt, irep_id_hash > find_symbols_sett
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
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
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
bool enable_memory_leak_check
instructionst::const_iterator const_targett
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
bool enable_conversion_check
The boolean constant true.
static bool has_dereference(const exprt &src)
division (integer and real)
constant_exprt smallest_expr() const
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
const source_locationt & find_source_location() const
exprt object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
Operator to dereference a pointer.
static irep_idt entry_point()
API to expression classes.
bool get_bool_option(const std::string &option) const
void div_by_zero_check(const div_exprt &expr, const guardt &guard)
const irep_idt & get(const irep_namet &name) const
Generic base class for unary expressions.
bool is_dynamic_local() const
std::list< std::string > value_listt
const exprt & size() const
A side effect that returns a non-deterministically chosen value.
split an expression into a base object and a (byte) offset
const exprt & size() const
#define forall_operands(it, expr)
const mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
void collect_allocations(const goto_functionst &goto_functions)
void pointer_overflow_check(const exprt &expr, const guardt &guard)
goto_function_templatet< goto_programt > goto_functiont
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)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Operator to return the address of an object.
error_labelst error_labels
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)
void check_rec(const exprt &expr, guardt &guard, bool address, const irep_idt &mode)
The boolean constant false.
bool has_subexpr(const exprt &src, const irep_idt &id)
returns true if the expression has a subexpression with given ID
std::size_t get_width() const
exprt disjunction(const exprt::operandst &op)
std::vector< exprt > operandst
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
exprt malloc_object(const exprt &pointer, const namespacet &ns)
flagst get(const goto_programt::const_targett t, const exprt &src)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
typet type
Type of symbol.
void integer_overflow_check(const exprt &expr, const guardt &guard)
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
exprt dynamic_object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
void check(const exprt &expr, const irep_idt &mode)
exprt dynamic_size(const namespacet &ns)
std::string array_name(const exprt &expr)
exprt invalid_pointer(const exprt &pointer)
Base class for all expressions.
void mod_by_zero_check(const mod_exprt &expr, const guardt &guard)
const exprt & struct_op() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
exprt pointer_offset(const exprt &pointer)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
bool enable_pointer_check
#define Forall_goto_functions(it, functions)
void float_overflow_check(const exprt &expr, const guardt &guard)
std::set< exprt > assertionst
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
bool enable_built_in_assertions
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const std::string & id_string() const
void from_integer(const mp_integer &i)
#define Forall_goto_program_instructions(it, program)
bool enable_pointer_overflow_check
void conversion_check(const exprt &expr, const guardt &guard)
goto_functionst::goto_functiont goto_functiont
std::pair< exprt, exprt > allocationt
Expression to hold a symbol (variable)
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
exprt dynamic_object(const exprt &pointer)
exprt null_pointer(const exprt &pointer)
const typet & subtype() const
#define forall_goto_functions(it, functions)
optionst::value_listt error_labelst
exprt dead_object(const exprt &pointer, const namespacet &ns)
#define forall_goto_program_instructions(it, program)
exprt same_object(const exprt &p1, const exprt &p2)
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
void make_typecast(const typet &_type)
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
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)
instructionst::iterator targett
IEEE-floating-point equality.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.