98 const exprt &access_lb,
99 const exprt &access_ub);
110 const std::string &property_class,
112 const exprt &src_expr,
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;
226 throw "no zero of argument type of operator "+expr.
id_string();
249 const typet &distance_type=
252 if(distance_type.
id()==ID_signedbv)
259 "shift distance is negative",
266 const typet &op_type=
269 if(op_type.
id()==ID_unsignedbv || op_type.
id()==ID_signedbv)
275 throw "no number for width for operator "+expr.
id_string();
278 expr.
distance(), ID_lt, width_expr);
282 "shift distance too large",
288 if(op_type.
id()==ID_signedbv && expr.
id()==ID_shl)
295 "shift operand is negative",
306 "shift of non-integer type",
326 throw "no zero of argument type of operator "+expr.
id_string();
349 if(type.
id()!=ID_signedbv &&
350 type.
id()!=ID_unsignedbv)
353 if(expr.
id()==ID_typecast)
358 throw "typecast takes one operand";
362 if(type.
id()==ID_signedbv)
366 if(old_type.
id()==ID_signedbv)
369 if(new_width>=old_width)
381 and_exprt(no_overflow_lower, no_overflow_upper),
382 "arithmetic overflow on signed type conversion",
388 else if(old_type.
id()==ID_unsignedbv)
391 if(new_width>=old_width+1)
401 "arithmetic overflow on unsigned to signed type conversion",
407 else if(old_type.
id()==ID_floatbv)
416 lower.from_integer(-
power(2, new_width-1)-1);
418 expr.
op0(), ID_gt, lower.to_expr());
421 and_exprt(no_overflow_lower, no_overflow_upper),
422 "arithmetic overflow on float to signed integer type conversion",
429 else if(type.
id()==ID_unsignedbv)
433 if(old_type.
id()==ID_signedbv)
437 if(new_width>=old_width-1)
445 "arithmetic overflow on signed to unsigned type conversion",
461 and_exprt(no_overflow_lower, no_overflow_upper),
462 "arithmetic overflow on signed to unsigned type conversion",
469 else if(old_type.
id()==ID_unsignedbv)
472 if(new_width>=old_width)
480 "arithmetic overflow on unsigned to unsigned type conversion",
486 else if(old_type.
id()==ID_floatbv)
495 lower.from_integer(-1);
497 expr.
op0(), ID_gt, lower.to_expr());
500 and_exprt(no_overflow_lower, no_overflow_upper),
501 "arithmetic overflow on float to unsigned integer type conversion",
530 if(expr.
id()==ID_div)
535 if(type.
id()==ID_signedbv)
545 "arithmetic overflow on signed division",
554 else if(expr.
id()==ID_mod)
559 else if(expr.
id()==ID_unary_minus)
561 if(type.
id()==ID_signedbv)
571 "arithmetic overflow on signed unary minus",
589 for(std::size_t i=1; i<expr.
operands().size(); i++)
601 overflow.operands().resize(2);
606 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
610 "arithmetic overflow on "+kind+
" "+expr.
id_string(),
620 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
624 "arithmetic overflow on "+kind+
" "+expr.
id_string(),
642 if(type.
id()!=ID_floatbv)
647 if(expr.
id()==ID_typecast)
663 "arithmetic overflow on floating-point typecast",
676 "arithmetic overflow on floating-point typecast",
685 else if(expr.
id()==ID_div)
697 "arithmetic overflow on floating-point division",
705 else if(expr.
id()==ID_mod)
710 else if(expr.
id()==ID_unary_minus)
715 else if(expr.
id()==ID_plus || expr.
id()==ID_mult ||
728 expr.
id()==ID_plus?
"addition":
729 expr.
id()==ID_minus?
"subtraction":
730 expr.
id()==ID_mult?
"multiplication":
"";
734 "arithmetic overflow on floating-point "+kind,
744 assert(expr.
id()!=ID_minus);
762 if(expr.
type().
id()!=ID_floatbv)
765 if(expr.
id()!=ID_plus &&
766 expr.
id()!=ID_mult &&
775 if(expr.
id()==ID_div)
788 isnan=
or_exprt(zero_div_zero, div_inf);
790 else if(expr.
id()==ID_mult)
806 isnan=
or_exprt(inf_times_zero, zero_times_inf);
808 else if(expr.
id()==ID_plus)
830 else if(expr.
id()==ID_minus)
871 throw expr.
id_string()+
" takes two arguments";
884 "same object violation",
900 if(expr.
id()==ID_plus ||
910 "pointer arithmetic overflow on "+expr.
id_string(),
922 const exprt &access_lb,
923 const exprt &access_ub)
949 "pointer dereference",
990 disjuncts.push_back(
and_exprt(lb_check, ub_check));
1000 "dereference failure: pointer NULL",
1001 "pointer dereference",
1010 "dereference failure: pointer invalid",
1011 "pointer dereference",
1019 "dereference failure: pointer uninitialized",
1020 "pointer dereference",
1028 "dereference failure: deallocated dynamic object",
1029 "pointer dereference",
1037 "dereference failure: dead object",
1038 "pointer dereference",
1055 "dereference failure: pointer outside dynamic object bounds",
1056 "pointer dereference",
1072 "dereference failure: pointer outside object bounds",
1073 "pointer dereference",
1099 if(array_type.
id()==ID_pointer)
1100 throw "index got pointer as array type";
1101 else if(array_type.
id()==ID_incomplete_array)
1102 throw "index got incomplete array";
1103 else if(array_type.
id()!=ID_array && array_type.
id()!=ID_vector)
1104 throw "bounds check expected array or vector type, got " 1113 if(index.type().id()!=ID_unsignedbv)
1116 if(index.id()==ID_typecast &&
1117 index.operands().size()==1 &&
1118 index.op0().type().id()==ID_unsignedbv)
1138 assert(p_offset.
type()==effective_offset.
type());
1140 effective_offset=
plus_exprt(p_offset, effective_offset);
1151 name+
" lower bound",
1164 const exprt &pointer=
1174 assert(effective_offset.op0().type()==effective_offset.op1().type());
1175 if(effective_offset.type()!=size.
type())
1188 name+
" dynamic object upper bound",
1195 if(type_size.is_not_nil())
1202 const exprt &size=array_type.
id()==ID_array ?
1211 else if(size.
id()==ID_infinity)
1234 name +
" upper bound",
1254 name+
" upper bound",
1265 const std::string &property_class,
1267 const exprt &src_expr,
1286 new_expr.
swap(expr);
1300 std::string source_expr_string;
1303 t->guard.swap(new_expr);
1304 t->source_location=source_location;
1305 t->source_location.set_comment(
comment+
" in "+source_expr_string);
1306 t->source_location.set_property_class(property_class);
1313 if(expr.
id()==ID_exists || expr.
id()==ID_forall)
1318 if(expr.
id()==ID_dereference)
1323 else if(expr.
id()==ID_index)
1337 if(expr.
id()==ID_address_of)
1343 else if(expr.
id()==ID_and || expr.
id()==ID_or)
1346 throw "`"+expr.
id_string()+
"' must be Boolean, but got "+
1351 for(
const auto &op : expr.
operands())
1353 if(!op.is_boolean())
1354 throw "`"+expr.
id_string()+
"' takes Boolean operands only, but got "+
1359 if(expr.
id()==ID_or)
1365 guard.
swap(old_guard);
1369 else if(expr.
id()==ID_if)
1372 throw "if takes three arguments";
1377 "first argument of if must be boolean, but got " 1388 guard.
swap(old_guard);
1395 guard.
swap(old_guard);
1400 else if(expr.
id()==ID_member &&
1430 if(expr.
id()==ID_index)
1434 else if(expr.
id()==ID_div)
1438 if(expr.
type().
id()==ID_signedbv)
1440 else if(expr.
type().
id()==ID_floatbv)
1446 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr)
1450 if(expr.
id()==ID_shl && expr.
type().
id()==ID_signedbv)
1453 else if(expr.
id()==ID_mod)
1457 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
1458 expr.
id()==ID_mult ||
1459 expr.
id()==ID_unary_minus)
1461 if(expr.
type().
id()==ID_signedbv ||
1462 expr.
type().
id()==ID_unsignedbv)
1470 else if(expr.
type().
id()==ID_floatbv)
1475 else if(expr.
type().
id()==ID_pointer)
1480 else if(expr.
id()==ID_typecast)
1482 else if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1483 expr.
id()==ID_ge || expr.
id()==ID_gt)
1485 else if(expr.
id()==ID_dereference)
1506 bool did_something =
false;
1541 t->source_location.set_property_class(
"error label");
1542 t->source_location.set_comment(
"error label "+label);
1543 t->source_location.set(
"user-provided",
true);
1551 if(statement==ID_expression)
1555 else if(statement==ID_printf)
1580 !code_function_call.
arguments().empty() &&
1597 "this is null on method invocation",
1598 "pointer dereference",
1636 "pointer dereference",
1653 did_something =
true;
1661 did_something =
true;
1701 t->make_assignment();
1712 "dynamically allocated memory never freed",
1722 if(i_it->source_location.is_nil())
1724 i_it->source_location.id(
irep_idt());
1726 if(!it->source_location.get_file().empty())
1727 i_it->source_location.set_file(it->source_location.get_file());
1729 if(!it->source_location.get_line().empty())
1730 i_it->source_location.set_line(it->source_location.get_line());
1732 if(!it->source_location.get_function().empty())
1733 i_it->source_location.set_function(
1734 it->source_location.get_function());
1736 if(!it->source_location.get_column().empty())
1737 i_it->source_location.set_column(it->source_location.get_column());
1739 if(!it->source_location.get_java_bytecode_index().empty())
1740 i_it->source_location.set_java_bytecode_index(
1741 it->source_location.get_java_bytecode_index());
1744 if(i_it->function.empty())
1745 i_it->function=it->function;
1780 goto_check.collect_allocations(goto_functions);
exprt guard
Guard for gotos, assume, assert.
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 pointer_rel_check(const exprt &expr, const guardt &guard)
void goto_check(goto_functiont &goto_function, const irep_idt &mode)
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.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
pointer_typet pointer_type(const typet &subtype)
bool is_dynamic_heap() const
bool enable_signed_overflow_check
bool is_static_lifetime() const
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)
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.
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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Extract member of struct or union.
This class represents an instruction in the GOTO intermediate representation.
void clear()
Clear the goto program.
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
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
exprt object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
Operator to dereference a pointer.
instructionst instructions
The list of instructions in the goto program.
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
instructionst::const_iterator const_targett
bool is_dynamic_local() const
std::list< std::string > value_listt
::goto_functiont goto_functiont
Abstract interface to support a programming language.
const exprt & size() const
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.
void collect_allocations(const goto_functionst &goto_functions)
const typet & follow(const typet &) const
void pointer_overflow_check(const exprt &expr, const guardt &guard)
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
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
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.
typet type
Type of symbol.
void integer_overflow_check(const exprt &expr, const guardt &guard)
static irep_idt entry_point()
exprt dynamic_object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
exprt dynamic_size(const namespacet &ns)
std::string array_name(const exprt &expr)
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.
void mod_by_zero_check(const mod_exprt &expr, const guardt &guard)
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)
void float_overflow_check(const exprt &expr, const guardt &guard)
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
#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)
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)
const typet & subtype() const
#define forall_goto_functions(it, functions)
optionst::value_listt error_labelst
void pointer_validity_check(const dereference_exprt &expr, const guardt &guard, const exprt &access_lb, const exprt &access_ub)
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.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
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.