Go to the documentation of this file.
188 const exprt &src_expr,
223 const exprt &asserted_expr,
225 const std::string &property_class,
227 const exprt &src_expr,
294 args[0].type().id()!=ID_unsignedbv ||
295 args[1].type().id()!=ID_unsignedbv)
296 throw "expected two unsigned arguments to "
299 assert(args[0].type()==args[1].type());
306 if(lhs.
id()==ID_index)
308 else if(lhs.
id()==ID_member)
310 else if(lhs.
id()==ID_symbol)
362 std::vector<exprt> disjuncts;
363 for(
const auto &enum_value : enum_values)
392 if(distance_type.
id()==ID_signedbv)
399 "shift distance is negative",
408 if(op_type.
id()==ID_unsignedbv || op_type.
id()==ID_signedbv)
415 "shift distance too large",
421 if(op_type.
id()==ID_signedbv && expr.
id()==ID_shl)
428 "shift operand is negative",
439 "shift of non-integer type",
474 const auto &type = expr.
type();
476 if(type.id() == ID_signedbv)
490 or_exprt(int_min_neq, minus_one_neq),
491 "result of signed mod is not representable",
509 if(type.
id()!=ID_signedbv &&
510 type.
id()!=ID_unsignedbv)
513 if(expr.
id()==ID_typecast)
518 const typet &old_type = op.type();
520 if(type.
id()==ID_signedbv)
524 if(old_type.
id()==ID_signedbv)
527 if(new_width>=old_width)
537 and_exprt(no_overflow_lower, no_overflow_upper),
538 "arithmetic overflow on signed type conversion",
544 else if(old_type.
id()==ID_unsignedbv)
547 if(new_width>=old_width+1)
555 "arithmetic overflow on unsigned to signed type conversion",
561 else if(old_type.
id()==ID_floatbv)
575 and_exprt(no_overflow_lower, no_overflow_upper),
576 "arithmetic overflow on float to signed integer type conversion",
583 else if(type.
id()==ID_unsignedbv)
587 if(old_type.
id()==ID_signedbv)
591 if(new_width>=old_width-1)
599 "arithmetic overflow on signed to unsigned type conversion",
615 and_exprt(no_overflow_lower, no_overflow_upper),
616 "arithmetic overflow on signed to unsigned type conversion",
623 else if(old_type.
id()==ID_unsignedbv)
626 if(new_width>=old_width)
634 "arithmetic overflow on unsigned to unsigned type conversion",
640 else if(old_type.
id()==ID_floatbv)
654 and_exprt(no_overflow_lower, no_overflow_upper),
655 "arithmetic overflow on float to unsigned integer type conversion",
684 if(expr.
id()==ID_div)
687 if(type.
id()==ID_signedbv)
698 "arithmetic overflow on signed division",
707 else if(expr.
id()==ID_unary_minus)
709 if(type.
id()==ID_signedbv)
719 "arithmetic overflow on signed unary minus",
728 else if(expr.
id() == ID_shl)
730 if(type.
id() == ID_signedbv)
733 const auto &op = shl_expr.op();
735 const auto op_width = op_type.get_width();
736 const auto &distance = shl_expr.distance();
737 const auto &distance_type = distance.type();
741 exprt neg_value_shift;
743 if(op_type.id() == ID_unsignedbv)
751 exprt neg_dist_shift;
753 if(distance_type.id() == ID_unsignedbv)
762 distance, ID_gt,
from_integer(op_width, distance_type));
767 new_type.set_width(op_width * 2);
778 bool allow_shift_into_sign_bit =
true;
786 allow_shift_into_sign_bit =
false;
789 else if(
mode == ID_cpp)
795 allow_shift_into_sign_bit =
false;
799 const unsigned number_of_top_bits =
800 allow_shift_into_sign_bit ? op_width : op_width + 1;
804 new_type.get_width() - 1,
805 new_type.get_width() - number_of_top_bits,
808 const exprt top_bits_zero =
822 "arithmetic overflow on signed shl",
840 for(std::size_t i=1; i<expr.
operands().size(); i++)
857 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
861 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
871 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
875 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
893 if(type.
id()!=ID_floatbv)
898 if(expr.
id()==ID_typecast)
903 if(op.type().id() == ID_floatbv)
909 std::move(overflow_check),
910 "arithmetic overflow on floating-point typecast",
921 "arithmetic overflow on floating-point typecast",
930 else if(expr.
id()==ID_div)
937 std::move(overflow_check),
938 "arithmetic overflow on floating-point division",
946 else if(expr.
id()==ID_mod)
951 else if(expr.
id()==ID_unary_minus)
956 else if(expr.
id()==ID_plus || expr.
id()==ID_mult ||
968 expr.
id()==ID_plus?
"addition":
969 expr.
id()==ID_minus?
"subtraction":
970 expr.
id()==ID_mult?
"multiplication":
"";
973 std::move(overflow_check),
974 "arithmetic overflow on floating-point " + kind,
984 assert(expr.
id()!=ID_minus);
1001 if(expr.
type().
id()!=ID_floatbv)
1004 if(expr.
id()!=ID_plus &&
1005 expr.
id()!=ID_mult &&
1006 expr.
id()!=ID_div &&
1007 expr.
id()!=ID_minus)
1014 if(expr.
id()==ID_div)
1023 div_expr.op0(),
from_integer(0, div_expr.dividend().type())),
1025 div_expr.op1(),
from_integer(0, div_expr.divisor().type())));
1029 isnan=
or_exprt(zero_div_zero, div_inf);
1031 else if(expr.
id()==ID_mult)
1042 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())));
1046 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())),
1049 isnan=
or_exprt(inf_times_zero, zero_times_inf);
1051 else if(expr.
id()==ID_plus)
1072 else if(expr.
id()==ID_minus)
1111 if(expr.
op0().
type().
id()==ID_pointer &&
1122 "same object violation",
1138 if(expr.
id() != ID_plus && expr.
id() != ID_minus)
1143 "pointer arithmetic expected to have exactly 2 operands");
1150 "pointer arithmetic overflow on " + expr.
id_string(),
1159 const exprt &src_expr,
1169 if(expr.
type().
id() == ID_empty)
1181 size = size_of_expr_opt.value();
1186 for(
const auto &c : conditions)
1190 "dereference failure: " + c.description,
1191 "pointer dereference",
1208 const exprt pointer = (expr.
id() == ID_r_ok || expr.
id() == ID_w_ok)
1214 if(pointer.
id() == ID_symbol)
1224 const exprt size = !size_of_expr_opt.has_value()
1226 : size_of_expr_opt.value();
1232 for(
const auto &c : conditions)
1233 conjuncts.push_back(c.assertion);
1239 "pointer in pointer primitive is neither null nor valid",
1240 "pointer primitives",
1251 return expr.
id() == ID_pointer_object || expr.
id() == ID_pointer_offset ||
1252 expr.
id() == ID_object_size || expr.
id() == ID_r_ok ||
1253 expr.
id() == ID_w_ok || expr.
id() == ID_is_dynamic_object;
1273 return {
conditiont(not_eq_null,
"reference is null")};
1293 alloc_disjuncts.push_back(
and_exprt(lb_check, ub_check));
1296 const exprt in_bounds_of_some_explicit_allocation =
1307 if(unknown || flags.
is_null())
1311 in_bounds_of_some_explicit_allocation,
1320 in_bounds_of_some_explicit_allocation,
1322 "deallocated dynamic object"));
1329 in_bounds_of_some_explicit_allocation,
1336 const or_exprt object_bounds_violation(
1342 in_bounds_of_some_explicit_allocation,
1345 "pointer outside dynamic object bounds"));
1350 const or_exprt object_bounds_violation(
1356 in_bounds_of_some_explicit_allocation,
1360 "pointer outside object bounds"));
1368 "invalid integer address"));
1393 if(array_type.
id()==ID_pointer)
1394 throw "index got pointer as array type";
1395 else if(array_type.
id()!=ID_array && array_type.
id()!=ID_vector)
1396 throw "bounds check expected array or vector type, got "
1405 if(index.
type().
id()!=ID_unsignedbv)
1409 index.
id() == ID_typecast &&
1416 const auto i = numeric_cast<mp_integer>(index);
1418 if(!i.has_value() || *i < 0)
1426 assert(p_offset.
type()==effective_offset.
type());
1428 effective_offset=
plus_exprt(p_offset, effective_offset);
1435 effective_offset, ID_ge, std::move(zero));
1439 name +
" lower bound",
1452 const exprt &pointer=
1462 assert(effective_offset.
op0().
type()==effective_offset.
op1().
type());
1464 const auto size_casted =
1481 std::move(upper_bound), ID_lt,
plus_exprt{a.first, a.second}};
1483 alloc_disjuncts.push_back(
1484 and_exprt{std::move(lower_bound_check), std::move(upper_bound_check)});
1487 exprt in_bounds_of_some_explicit_allocation =
disjunction(alloc_disjuncts);
1490 std::move(in_bounds_of_some_explicit_allocation),
1496 name +
" dynamic object upper bound",
1504 if(type_size_opt.has_value())
1523 const exprt &size=array_type.
id()==ID_array ?
1532 else if(size.
id()==ID_infinity)
1553 type_size_opt.value());
1557 name +
" upper bound",
1573 name +
" upper bound",
1582 const exprt &asserted_expr,
1584 const std::string &property_class,
1586 const exprt &src_expr,
1590 exprt simplified_expr =
1598 exprt guarded_expr =
1600 ? std::move(simplified_expr)
1607 std::move(guarded_expr), source_location)
1609 std::move(guarded_expr), source_location));
1611 std::string source_expr_string;
1614 t->source_location.set_comment(
comment +
" in " + source_expr_string);
1615 t->source_location.set_property_class(property_class);
1622 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1625 if(expr.
id() == ID_dereference)
1629 else if(expr.
id() == ID_index)
1637 for(
const auto &operand : expr.
operands())
1646 "'" + expr.
id_string() +
"' must be Boolean, but got " + expr.
pretty());
1648 guardt old_guard = guard;
1650 for(
const auto &op : expr.
operands())
1654 "'" + expr.
id_string() +
"' takes Boolean operands only, but got " +
1661 guard = std::move(old_guard);
1668 "first argument of if must be boolean, but got " + if_expr.
cond().
pretty());
1673 guardt old_guard = guard;
1676 guard = std::move(old_guard);
1680 guardt old_guard = guard;
1683 guard = std::move(old_guard);
1702 if(member_offset_opt.has_value())
1729 if(div_expr.
type().
id() == ID_signedbv)
1731 else if(div_expr.
type().
id() == ID_floatbv)
1740 if(expr.
type().
id() == ID_signedbv || expr.
type().
id() == ID_unsignedbv)
1744 else if(expr.
type().
id() == ID_floatbv)
1749 else if(expr.
type().
id() == ID_pointer)
1758 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1761 if(expr.
id() == ID_address_of)
1766 else if(expr.
id() == ID_and || expr.
id() == ID_or)
1771 else if(expr.
id() == ID_if)
1777 expr.
id() == ID_member &&
1787 if(expr.
type().
id() == ID_c_enum_tag)
1790 if(expr.
id()==ID_index)
1794 else if(expr.
id()==ID_div)
1798 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr)
1802 if(expr.
id()==ID_shl && expr.
type().
id()==ID_signedbv)
1805 else if(expr.
id()==ID_mod)
1810 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
1811 expr.
id()==ID_mult ||
1812 expr.
id()==ID_unary_minus)
1816 else if(expr.
id()==ID_typecast)
1818 else if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1819 expr.
id()==ID_ge || expr.
id()==ID_gt)
1821 else if(expr.
id()==ID_dereference)
1840 bool modified =
false;
1845 if(op_result.has_value())
1852 if(expr.
id() == ID_r_ok || expr.
id() == ID_w_ok)
1856 expr.
operands().size() == 2,
"r/w_ok must have two operands");
1858 const auto conditions =
1863 for(
const auto &c : conditions)
1864 conjuncts.push_back(c.assertion);
1869 return std::move(expr);
1882 if(flag != new_value)
1893 *flag_pair.first = flag_pair.second;
1901 const irep_idt &function_identifier,
1906 const auto &function_symbol =
ns.
lookup(function_identifier);
1907 mode = function_symbol.mode;
1909 bool did_something =
false;
1912 util_make_unique<local_bitvector_analysist>(goto_function,
ns);
1923 for(
const auto &d : pragmas)
1925 if(d.first ==
"disable:bounds-check")
1927 else if(d.first ==
"disable:pointer-check")
1929 else if(d.first ==
"disable:memory-leak-check")
1931 else if(d.first ==
"disable:div-by-zero-check")
1933 else if(d.first ==
"disable:enum-range-check")
1935 else if(d.first ==
"disable:signed-overflow-check")
1937 else if(d.first ==
"disable:unsigned-overflow-check")
1939 else if(d.first ==
"disable:pointer-overflow-check")
1941 else if(d.first ==
"disable:float-overflow-check")
1943 else if(d.first ==
"disable:conversion-check")
1945 else if(d.first ==
"disable:undefined-shift-check")
1947 else if(d.first ==
"disable:nan-check")
1949 else if(d.first ==
"disable:pointer-primitive-check")
1967 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1971 if(rw_ok_cond.has_value())
1986 t->source_location.set_property_class(
"error label");
1987 t->source_location.set_comment(
"error label "+label);
1988 t->source_location.set(
"user-provided",
true);
1995 const irep_idt &statement = code.get_statement();
1997 if(statement==ID_expression)
2001 else if(statement==ID_printf)
2003 for(
const auto &op : code.operands())
2024 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
2029 if(rw_ok_cond.has_value())
2042 !code_function_call.
arguments().empty() &&
2059 "this is null on method invocation",
2060 "pointer dereference",
2067 for(
const auto &op : code_function_call.
operands())
2083 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
2088 if(rw_ok_cond.has_value())
2089 return_value = *rw_ok_cond;
2109 "pointer dereference",
2127 did_something =
true;
2135 did_something =
true;
2154 std::move(address_of_expr),
2183 "dynamically allocated memory never freed",
2193 if(i_it->source_location.is_nil())
2195 i_it->source_location.id(
irep_idt());
2197 if(!it->source_location.get_file().empty())
2198 i_it->source_location.set_file(it->source_location.get_file());
2200 if(!it->source_location.get_line().empty())
2201 i_it->source_location.set_line(it->source_location.get_line());
2203 if(!it->source_location.get_function().empty())
2204 i_it->source_location.set_function(
2205 it->source_location.get_function());
2207 if(!it->source_location.get_column().empty())
2208 i_it->source_location.set_column(it->source_location.get_column());
2210 if(!it->source_location.get_java_bytecode_index().empty())
2211 i_it->source_location.set_java_bytecode_index(
2212 it->source_location.get_java_bytecode_index());
2232 const irep_idt &function_identifier,
2238 goto_check.goto_check(function_identifier, goto_function);
2248 goto_check.collect_allocations(goto_functions);
2252 goto_check.goto_check(it->first, it->second);
std::pair< exprt, exprt > allocationt
std::list< allocationt > allocationst
#define Forall_goto_program_instructions(it, program)
const irep_idt & get_identifier() const
std::string array_name(const exprt &)
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
std::string array_name(const namespacet &ns, const exprt &expr)
static exprt conditional_cast(const exprt &expr, const typet &type)
goto_programt::const_targett current_target
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
A base class for multi-ary expressions Associativity is not specified.
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.
bool enable_div_by_zero_check
Field-insensitive, location-sensitive bitvector analysis.
bool enable_undefined_shift_check
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
void set_function(const irep_idt &function)
guard_managert guard_manager
exprt null_pointer(const exprt &pointer)
#define CHECK_RETURN(CONDITION)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
The type of an expression, extends irept.
const irept::named_subt & get_pragmas() const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
typet type
Type of symbol.
Operator to dereference a pointer.
bool is_dynamic_heap() const
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
std::vector< c_enum_membert > memberst
void check_rec_address(const exprt &expr, guardt &guard)
Check an address-of expression: if it is a dereference then check the pointer if it is an index then ...
Various predicates over pointers in programs.
bool enable_assert_to_assume
Split an expression into a base object and a (byte) offset.
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.
bool enable_pointer_primitive_check
~flag_resett()
Restore the values of all flags that have been modified via set_flag.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
The plus expression Associativity is not specified.
Set a Boolean flag to a new value (via set_flag) and restore the previous value when the entire objec...
void pointer_validity_check(const dereference_exprt &expr, const exprt &src_expr, const guardt &guard)
Generates VCCs for the validity of the given dereferencing operation.
Base class for all expressions.
bool enable_conversion_check
void check_rec_div(const div_exprt &div_expr, guardt &guard)
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numb...
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
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.
struct configt::ansi_ct ansi_c
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
void pointer_rel_check(const binary_relation_exprt &, const guardt &)
Expression to hold a symbol (variable)
void nan_check(const exprt &, const guardt &)
bool enable_memory_leak_check
void enum_range_check(const exprt &, const guardt &)
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
void pointer_primitive_check(const exprt &expr, const guardt &guard)
Generates VCCs to check that pointers passed to pointer primitives are either null or valid.
Fixed-width bit-vector with unsigned binary interpretation.
const codet & get_other() const
Get the statement for OTHER.
bool enable_unsigned_overflow_check
bool enable_float_overflow_check
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
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...
This is unused by this implementation of guards, but can be used by other implementations of the same...
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
void check_rec_logical_op(const exprt &expr, guardt &guard)
Check a logical operation: check each operand in separation while extending the guarding condition as...
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 turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
void check(const exprt &expr)
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
void check_rec(const exprt &expr, guardt &guard)
Recursively descend into expr and run the appropriate check for each sub-expression,...
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.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
The null pointer constant.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
void float_overflow_check(const exprt &, const guardt &)
bool enable_pointer_check
codet code
Do not read or modify directly – use get_X() instead.
#define forall_operands(it, expr)
const exprt & struct_op() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
void add(const exprt &expr)
#define PRECONDITION(CONDITION)
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
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
bool is_integer_address() const
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
exprt deallocated(const exprt &pointer, const namespacet &ns)
const std::string & id_string() const
exprt dead_object(const exprt &pointer, const namespacet &ns)
bool enable_enum_range_check
std::set< exprt > assertionst
Abstract interface to support a programming language.
exprt simplify_expr(exprt src, const namespacet &ns)
exprt integer_address(const exprt &pointer)
bool has_condition() const
Does this instruction have a condition?
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
pointer_typet pointer_type(const typet &subtype)
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
bool check_rec_member(const member_exprt &member, guardt &guard)
Check that a member expression is valid:
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
const code_returnt & to_code_return(const codet &code)
The Boolean constant false.
optionalt< exprt > rw_ok_check(exprt)
expand the r_ok and w_ok predicates
void collect_allocations(const goto_functionst &goto_functions)
Fill the list of allocations allocationst with <address, size> for every allocation instruction.
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 &)
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
nonstd::optional< T > optionalt
const constant_exprt & size() const
void div_by_zero_check(const div_exprt &, const guardt &)
exprt pointer_offset(const exprt &pointer)
goto_functionst::goto_functiont goto_functiont
exprt null_object(const exprt &pointer)
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)
void set_flag(bool &flag, bool new_value)
Store the current value of flag and then set its value to new_value.
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.
C enum tag type, i.e., c_enum_typet with an identifier.
codet representation of a "return from a function" statement.
goto_functionst goto_functions
GOTO functions.
std::unordered_set< irep_idt > find_symbols_sett
void goto_check(const irep_idt &function_identifier, goto_functiont &goto_function)
void mod_overflow_check(const mod_exprt &, const guardt &)
check a mod expression for the case INT_MIN % -1
const code_assignt & to_code_assign(const codet &code)
Evaluates to true if the operand is infinite.
void invalidate(const exprt &lhs)
Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
enum configt::ansi_ct::c_standardt c_standard
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 whose two operands have the same type.
void add_guarded_property(const exprt &asserted_expr, const std::string &comment, const std::string &property_class, const source_locationt &source_location, const exprt &src_expr, const guardt &guard)
Include the asserted_expr in the code conditioned by the guard.
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)
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.
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
#define forall_goto_functions(it, functions)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
instructionst::const_iterator const_targett
bool has_prefix(const std::string &s, const std::string &prefix)
constant_exprt to_expr() const
optionst::value_listt error_labelst
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
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".
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 ...
unsignedbv_typet size_type()
bool enable_pointer_overflow_check
const exprt & return_value() const
A codet representing an assignment in the program.
The Boolean constant true.
void check_rec_if(const if_exprt &if_expr, guardt &guard)
Check an if expression: check the if-condition alone, and then check the true/false-cases with the gu...
const irep_idt & get_statement() const
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
A constant literal expression.
IEEE-floating-point equality.
bool is_function_call() const
bool is_boolean() const
Return whether the expression represents a Boolean.
static bool is_built_in(const std::string &s)
bool is_pointer_primitive(const exprt &expr)
Returns true if the given expression is a pointer primitive such as __CPROVER_r_ok()
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
bool is_target() const
Is this node a branch target?
const irep_idt & get_value() const
const source_locationt & source_location() const
conditiont(const exprt &_assertion, const std::string &_description)
exprt dynamic_size(const namespacet &ns)
symbol_tablet symbol_table
Symbol table.
void check_rec_arithmetic_op(const exprt &expr, guardt &guard)
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers),...
const value_listt & get_list_option(const std::string &option) const
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
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.
const memberst & members() const
std::list< std::pair< bool *, bool > > flags_to_reset
enum configt::cppt::cpp_standardt cpp_standard