Go to the documentation of this file.
191 const exprt &src_expr,
211 const exprt &address,
214 const exprt &pointer,
218 const exprt &address,
237 const exprt &asserted_expr,
239 const std::string &property_class,
241 const exprt &src_expr,
298 for(
const auto &instruction : gf_entry.second.body.instructions)
300 if(!instruction.is_function_call())
312 args[0].type().id()!=ID_unsignedbv ||
313 args[1].type().id()!=ID_unsignedbv)
314 throw "expected two unsigned arguments to "
317 assert(args[0].type()==args[1].type());
325 if(lhs.
id()==ID_index)
327 else if(lhs.
id()==ID_member)
329 else if(lhs.
id()==ID_symbol)
385 std::vector<exprt> disjuncts;
386 for(
const auto &enum_value : enum_values)
415 if(distance_type.
id()==ID_signedbv)
422 "shift distance is negative",
431 if(op_type.
id()==ID_unsignedbv || op_type.
id()==ID_signedbv)
438 "shift distance too large",
444 if(op_type.
id()==ID_signedbv && expr.
id()==ID_shl)
451 "shift operand is negative",
462 "shift of non-integer type",
497 const auto &type = expr.
type();
499 if(type.id() == ID_signedbv)
513 or_exprt(int_min_neq, minus_one_neq),
514 "result of signed mod is not representable",
532 if(type.
id()!=ID_signedbv &&
533 type.
id()!=ID_unsignedbv)
536 if(expr.
id()==ID_typecast)
541 const typet &old_type = op.type();
543 if(type.
id()==ID_signedbv)
547 if(old_type.
id()==ID_signedbv)
550 if(new_width>=old_width)
560 and_exprt(no_overflow_lower, no_overflow_upper),
561 "arithmetic overflow on signed type conversion",
567 else if(old_type.
id()==ID_unsignedbv)
570 if(new_width>=old_width+1)
578 "arithmetic overflow on unsigned to signed type conversion",
584 else if(old_type.
id()==ID_floatbv)
598 and_exprt(no_overflow_lower, no_overflow_upper),
599 "arithmetic overflow on float to signed integer type conversion",
606 else if(type.
id()==ID_unsignedbv)
610 if(old_type.
id()==ID_signedbv)
614 if(new_width>=old_width-1)
622 "arithmetic overflow on signed to unsigned type conversion",
638 and_exprt(no_overflow_lower, no_overflow_upper),
639 "arithmetic overflow on signed to unsigned type conversion",
646 else if(old_type.
id()==ID_unsignedbv)
649 if(new_width>=old_width)
657 "arithmetic overflow on unsigned to unsigned type conversion",
663 else if(old_type.
id()==ID_floatbv)
677 and_exprt(no_overflow_lower, no_overflow_upper),
678 "arithmetic overflow on float to unsigned integer type conversion",
707 if(expr.
id()==ID_div)
710 if(type.
id()==ID_signedbv)
721 "arithmetic overflow on signed division",
730 else if(expr.
id()==ID_unary_minus)
732 if(type.
id()==ID_signedbv)
742 "arithmetic overflow on signed unary minus",
751 else if(expr.
id() == ID_shl)
753 if(type.
id() == ID_signedbv)
756 const auto &op = shl_expr.op();
758 const auto op_width = op_type.get_width();
759 const auto &distance = shl_expr.distance();
760 const auto &distance_type = distance.type();
764 exprt neg_value_shift;
766 if(op_type.id() == ID_unsignedbv)
774 exprt neg_dist_shift;
776 if(distance_type.id() == ID_unsignedbv)
785 distance, ID_gt,
from_integer(op_width, distance_type));
790 new_type.set_width(op_width * 2);
801 bool allow_shift_into_sign_bit =
true;
809 allow_shift_into_sign_bit =
false;
812 else if(
mode == ID_cpp)
818 allow_shift_into_sign_bit =
false;
822 const unsigned number_of_top_bits =
823 allow_shift_into_sign_bit ? op_width : op_width + 1;
827 new_type.get_width() - 1,
828 new_type.get_width() - number_of_top_bits,
831 const exprt top_bits_zero =
845 "arithmetic overflow on signed shl",
863 for(std::size_t i=1; i<expr.
operands().size(); i++)
880 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
884 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
894 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
898 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
916 if(type.
id()!=ID_floatbv)
921 if(expr.
id()==ID_typecast)
926 if(op.type().id() == ID_floatbv)
932 std::move(overflow_check),
933 "arithmetic overflow on floating-point typecast",
944 "arithmetic overflow on floating-point typecast",
953 else if(expr.
id()==ID_div)
960 std::move(overflow_check),
961 "arithmetic overflow on floating-point division",
969 else if(expr.
id()==ID_mod)
974 else if(expr.
id()==ID_unary_minus)
979 else if(expr.
id()==ID_plus || expr.
id()==ID_mult ||
991 expr.
id()==ID_plus?
"addition":
992 expr.
id()==ID_minus?
"subtraction":
993 expr.
id()==ID_mult?
"multiplication":
"";
996 std::move(overflow_check),
997 "arithmetic overflow on floating-point " + kind,
1007 assert(expr.
id()!=ID_minus);
1024 if(expr.
type().
id()!=ID_floatbv)
1027 if(expr.
id()!=ID_plus &&
1028 expr.
id()!=ID_mult &&
1029 expr.
id()!=ID_div &&
1030 expr.
id()!=ID_minus)
1037 if(expr.
id()==ID_div)
1046 div_expr.op0(),
from_integer(0, div_expr.dividend().type())),
1048 div_expr.op1(),
from_integer(0, div_expr.divisor().type())));
1052 isnan=
or_exprt(zero_div_zero, div_inf);
1054 else if(expr.
id()==ID_mult)
1065 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())));
1069 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())),
1072 isnan=
or_exprt(inf_times_zero, zero_times_inf);
1074 else if(expr.
id()==ID_plus)
1095 else if(expr.
id()==ID_minus)
1134 if(expr.
op0().
type().
id()==ID_pointer &&
1143 "same object violation",
1149 for(
const auto &pointer : expr.
operands())
1156 for(
const auto &c : conditions)
1160 "pointer relation: " + c.description,
1161 "pointer arithmetic",
1177 if(expr.
id() != ID_plus && expr.
id() != ID_minus)
1182 "pointer arithmetic expected to have exactly 2 operands");
1188 for(
const auto &c : conditions)
1192 "pointer arithmetic: " + c.description,
1193 "pointer arithmetic",
1202 const exprt &src_expr,
1212 if(expr.
type().
id() == ID_empty)
1224 size = size_of_expr_opt.value();
1229 for(
const auto &c : conditions)
1233 "dereference failure: " + c.description,
1234 "pointer dereference",
1251 const exprt pointer = (expr.
id() == ID_r_ok || expr.
id() == ID_w_ok)
1257 if(pointer.
id() == ID_symbol)
1267 const exprt size = !size_of_expr_opt.has_value()
1269 : size_of_expr_opt.value();
1273 for(
const auto &c : conditions)
1278 "pointer primitives",
1290 return expr.
id() == ID_pointer_object || expr.
id() == ID_pointer_offset ||
1291 expr.
id() == ID_object_size || expr.
id() == ID_r_ok ||
1292 expr.
id() == ID_w_ok || expr.
id() == ID_is_dynamic_object;
1296 const exprt &address,
1303 conditions.push_front(*maybe_null_condition);
1326 if(array_type.
id()==ID_pointer)
1327 throw "index got pointer as array type";
1328 else if(array_type.
id()!=ID_array && array_type.
id()!=ID_vector)
1329 throw "bounds check expected array or vector type, got "
1338 if(index.
type().
id()!=ID_unsignedbv)
1342 index.
id() == ID_typecast &&
1349 const auto i = numeric_cast<mp_integer>(index);
1351 if(!i.has_value() || *i < 0)
1359 assert(p_offset.
type()==effective_offset.
type());
1361 effective_offset=
plus_exprt(p_offset, effective_offset);
1368 effective_offset, ID_ge, std::move(zero));
1372 name +
" lower bound",
1385 const exprt &pointer=
1395 assert(effective_offset.
op0().
type()==effective_offset.
op1().
type());
1397 const auto size_casted =
1402 exprt in_bounds_of_some_explicit_allocation =
1408 std::move(in_bounds_of_some_explicit_allocation),
1414 name +
" dynamic object upper bound",
1422 if(type_size_opt.has_value())
1441 const exprt &size=array_type.
id()==ID_array ?
1450 else if(size.
id()==ID_infinity)
1471 type_size_opt.value());
1475 name +
" upper bound",
1491 name +
" upper bound",
1500 const exprt &asserted_expr,
1502 const std::string &property_class,
1504 const exprt &src_expr,
1508 exprt simplified_expr =
1516 exprt guarded_expr =
1518 ? std::move(simplified_expr)
1521 if(
assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1525 std::move(guarded_expr), source_location)
1527 std::move(guarded_expr), source_location));
1529 std::string source_expr_string;
1532 t->source_location.set_comment(
comment +
" in " + source_expr_string);
1533 t->source_location.set_property_class(property_class);
1540 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1543 if(expr.
id() == ID_dereference)
1547 else if(expr.
id() == ID_index)
1555 for(
const auto &operand : expr.
operands())
1564 "'" + expr.
id_string() +
"' must be Boolean, but got " + expr.
pretty());
1566 guardt old_guard = guard;
1568 for(
const auto &op : expr.
operands())
1572 "'" + expr.
id_string() +
"' takes Boolean operands only, but got " +
1579 guard = std::move(old_guard);
1586 "first argument of if must be boolean, but got " + if_expr.
cond().
pretty());
1591 guardt old_guard = guard;
1594 guard = std::move(old_guard);
1598 guardt old_guard = guard;
1601 guard = std::move(old_guard);
1620 if(member_offset_opt.has_value())
1647 if(div_expr.
type().
id() == ID_signedbv)
1649 else if(div_expr.
type().
id() == ID_floatbv)
1658 if(expr.
type().
id() == ID_signedbv || expr.
type().
id() == ID_unsignedbv)
1663 expr.
operands().size() == 2 && expr.
id() == ID_minus &&
1664 expr.
operands()[0].type().id() == ID_pointer &&
1665 expr.
operands()[1].type().id() == ID_pointer)
1670 else if(expr.
type().
id() == ID_floatbv)
1675 else if(expr.
type().
id() == ID_pointer)
1684 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1687 if(expr.
id() == ID_address_of)
1692 else if(expr.
id() == ID_and || expr.
id() == ID_or)
1697 else if(expr.
id() == ID_if)
1703 expr.
id() == ID_member &&
1713 if(expr.
type().
id() == ID_c_enum_tag)
1716 if(expr.
id()==ID_index)
1720 else if(expr.
id()==ID_div)
1724 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr)
1728 if(expr.
id()==ID_shl && expr.
type().
id()==ID_signedbv)
1731 else if(expr.
id()==ID_mod)
1736 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
1737 expr.
id()==ID_mult ||
1738 expr.
id()==ID_unary_minus)
1742 else if(expr.
id()==ID_typecast)
1744 else if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1745 expr.
id()==ID_ge || expr.
id()==ID_gt)
1747 else if(expr.
id()==ID_dereference)
1766 bool modified =
false;
1771 if(op_result.has_value())
1778 if(expr.
id() == ID_r_ok || expr.
id() == ID_w_ok)
1782 expr.
operands().size() == 2,
"r/w_ok must have two operands");
1789 for(
const auto &c : conditions)
1790 conjuncts.push_back(c.assertion);
1795 return std::move(expr);
1808 if(flag != new_value)
1819 *flag_pair.first = flag_pair.second;
1827 const irep_idt &function_identifier,
1832 const auto &function_symbol =
ns.
lookup(function_identifier);
1833 mode = function_symbol.mode;
1835 bool did_something =
false;
1838 util_make_unique<local_bitvector_analysist>(goto_function,
ns);
1849 for(
const auto &d : pragmas)
1851 if(d.first ==
"disable:bounds-check")
1853 else if(d.first ==
"disable:pointer-check")
1855 else if(d.first ==
"disable:memory-leak-check")
1857 else if(d.first ==
"disable:div-by-zero-check")
1859 else if(d.first ==
"disable:enum-range-check")
1861 else if(d.first ==
"disable:signed-overflow-check")
1863 else if(d.first ==
"disable:unsigned-overflow-check")
1865 else if(d.first ==
"disable:pointer-overflow-check")
1867 else if(d.first ==
"disable:float-overflow-check")
1869 else if(d.first ==
"disable:conversion-check")
1871 else if(d.first ==
"disable:undefined-shift-check")
1873 else if(d.first ==
"disable:nan-check")
1875 else if(d.first ==
"disable:pointer-primitive-check")
1893 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1897 if(rw_ok_cond.has_value())
1912 t->source_location.set_property_class(
"error label");
1913 t->source_location.set_comment(
"error label "+label);
1914 t->source_location.set(
"user-provided",
true);
1921 const irep_idt &statement = code.get_statement();
1923 if(statement==ID_expression)
1927 else if(statement==ID_printf)
1929 for(
const auto &op : code.operands())
1950 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1955 if(rw_ok_cond.has_value())
1968 !code_function_call.
arguments().empty() &&
1985 "this is null on method invocation",
1986 "pointer dereference",
1993 for(
const auto &op : code_function_call.
operands())
2006 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
2011 if(rw_ok_cond.has_value())
2012 return_value = *rw_ok_cond;
2031 "pointer dereference",
2049 did_something =
true;
2057 did_something =
true;
2076 std::move(address_of_expr),
2105 "dynamically allocated memory never freed",
2115 if(instruction.source_location.is_nil())
2117 instruction.source_location.id(
irep_idt());
2119 if(!it->source_location.get_file().empty())
2120 instruction.source_location.set_file(it->source_location.get_file());
2122 if(!it->source_location.get_line().empty())
2123 instruction.source_location.set_line(it->source_location.get_line());
2125 if(!it->source_location.get_function().empty())
2126 instruction.source_location.set_function(
2127 it->source_location.get_function());
2129 if(!it->source_location.get_column().empty())
2131 instruction.source_location.set_column(
2132 it->source_location.get_column());
2135 if(!it->source_location.get_java_bytecode_index().empty())
2137 instruction.source_location.set_java_bytecode_index(
2138 it->source_location.get_java_bytecode_index());
2160 const exprt &address,
2176 const exprt in_bounds_of_some_explicit_allocation =
2191 in_bounds_of_some_explicit_allocation,
2193 "deallocated dynamic object"));
2200 in_bounds_of_some_explicit_allocation,
2207 const or_exprt object_bounds_violation(
2213 in_bounds_of_some_explicit_allocation,
2216 "pointer outside dynamic object bounds"));
2221 const or_exprt object_bounds_violation(
2227 in_bounds_of_some_explicit_allocation,
2231 "pointer outside object bounds"));
2239 "invalid integer address"));
2246 const exprt &address,
2259 return {
conditiont{not_eq_null,
"reference is null"}};
2273 const exprt &pointer,
2287 std::move(upper_bound), ID_le,
plus_exprt{a.first, a.second}};
2289 alloc_disjuncts.push_back(
2290 and_exprt{std::move(lb_check), std::move(ub_check)});
2296 const irep_idt &function_identifier,
2302 goto_check.goto_check(function_identifier, goto_function);
2312 goto_check.collect_allocations(goto_functions);
2316 goto_check.goto_check(gf_entry.first, gf_entry.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)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
#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...
A base class for binary expressions.
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
function_mapt function_map
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.
conditionst get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size)
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 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())
bool has_prefix(const std::string &s, const std::string &prefix)
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.
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.
conditionst get_pointer_points_to_valid_memory_conditions(const exprt &address, const exprt &size)
The null pointer constant.
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.
API to expression classes for Pointers.
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
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.
optionalt< goto_checkt::conditiont > get_pointer_is_null_condition(const exprt &address, const exprt &size)
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 body (see body) and parameter identifiers (see parameter_iden...
std::vector< exprt > operandst
exprt::operandst argumentst
The Boolean constant false.
API to expression classes for floating-point arithmetic.
optionalt< exprt > rw_ok_check(exprt)
expand the r_ok and w_ok predicates
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
void pointer_rel_check(const binary_exprt &, const guardt &)
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 is_in_bounds_of_some_explicit_allocation(const exprt &pointer, const exprt &size)
exprt pointer_offset(const exprt &pointer)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
goto_functionst::goto_functiont goto_functiont
exprt null_object(const exprt &pointer)
error_labelst error_labels
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.
const exprt & return_value() const
Get the return value of a RETURN instruction.
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.
A base class for shift and rotate operators.
C enum tag type, i.e., c_enum_typet with an identifier.
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.
std::set< std::pair< exprt, exprt > > assertionst
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.
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
constant_exprt to_expr() const
optionst::value_listt error_labelst
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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
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
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
API to expression classes for bitvectors.
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