Go to the documentation of this file.
193 const exprt &src_expr,
213 const exprt &address,
216 const exprt &pointer,
220 const exprt &address,
239 const exprt &asserted_expr,
241 const std::string &property_class,
243 const exprt &src_expr,
300 for(
const auto &instruction : gf_entry.second.body.instructions)
302 if(!instruction.is_function_call())
305 const auto &
function = instruction.call_function();
307 function.
id() != ID_symbol ||
313 instruction.call_arguments();
315 args[0].type().id()!=ID_unsignedbv ||
316 args[1].type().id()!=ID_unsignedbv)
317 throw "expected two unsigned arguments to "
320 assert(args[0].type()==args[1].type());
328 if(lhs.
id()==ID_index)
330 else if(lhs.
id()==ID_member)
332 else if(lhs.
id()==ID_symbol)
388 std::vector<exprt> disjuncts;
389 for(
const auto &enum_value : enum_values)
418 if(distance_type.
id()==ID_signedbv)
425 "shift distance is negative",
434 if(op_type.
id()==ID_unsignedbv || op_type.
id()==ID_signedbv)
441 "shift distance too large",
447 if(op_type.
id()==ID_signedbv && expr.
id()==ID_shl)
454 "shift operand is negative",
465 "shift of non-integer type",
500 const auto &type = expr.
type();
502 if(type.id() == ID_signedbv)
516 or_exprt(int_min_neq, minus_one_neq),
517 "result of signed mod is not representable",
535 if(type.
id()!=ID_signedbv &&
536 type.
id()!=ID_unsignedbv)
539 if(expr.
id()==ID_typecast)
544 const typet &old_type = op.type();
546 if(type.
id()==ID_signedbv)
550 if(old_type.
id()==ID_signedbv)
553 if(new_width>=old_width)
563 and_exprt(no_overflow_lower, no_overflow_upper),
564 "arithmetic overflow on signed type conversion",
570 else if(old_type.
id()==ID_unsignedbv)
573 if(new_width>=old_width+1)
581 "arithmetic overflow on unsigned to signed type conversion",
587 else if(old_type.
id()==ID_floatbv)
601 and_exprt(no_overflow_lower, no_overflow_upper),
602 "arithmetic overflow on float to signed integer type conversion",
609 else if(type.
id()==ID_unsignedbv)
613 if(old_type.
id()==ID_signedbv)
617 if(new_width>=old_width-1)
625 "arithmetic overflow on signed to unsigned type conversion",
641 and_exprt(no_overflow_lower, no_overflow_upper),
642 "arithmetic overflow on signed to unsigned type conversion",
649 else if(old_type.
id()==ID_unsignedbv)
652 if(new_width>=old_width)
660 "arithmetic overflow on unsigned to unsigned type conversion",
666 else if(old_type.
id()==ID_floatbv)
680 and_exprt(no_overflow_lower, no_overflow_upper),
681 "arithmetic overflow on float to unsigned integer type conversion",
710 if(expr.
id()==ID_div)
713 if(type.
id()==ID_signedbv)
724 "arithmetic overflow on signed division",
733 else if(expr.
id()==ID_unary_minus)
735 if(type.
id()==ID_signedbv)
745 "arithmetic overflow on signed unary minus",
751 else if(type.
id() == ID_unsignedbv)
761 "arithmetic overflow on unsigned unary minus",
770 else if(expr.
id() == ID_shl)
772 if(type.
id() == ID_signedbv)
775 const auto &op = shl_expr.op();
777 const auto op_width = op_type.get_width();
778 const auto &distance = shl_expr.distance();
779 const auto &distance_type = distance.type();
783 exprt neg_value_shift;
785 if(op_type.id() == ID_unsignedbv)
793 exprt neg_dist_shift;
795 if(distance_type.id() == ID_unsignedbv)
806 distance, ID_gt,
from_integer(op_width, distance_type));
811 new_type.set_width(op_width * 2);
822 bool allow_shift_into_sign_bit =
true;
830 allow_shift_into_sign_bit =
false;
833 else if(
mode == ID_cpp)
839 allow_shift_into_sign_bit =
false;
843 const unsigned number_of_top_bits =
844 allow_shift_into_sign_bit ? op_width : op_width + 1;
848 new_type.get_width() - 1,
849 new_type.get_width() - number_of_top_bits,
852 const exprt top_bits_zero =
866 "arithmetic overflow on signed shl",
884 for(std::size_t i=1; i<expr.
operands().size(); i++)
897 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
901 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
908 else if(expr.
operands().size() == 2)
910 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
915 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
926 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
930 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
948 if(type.
id()!=ID_floatbv)
953 if(expr.
id()==ID_typecast)
958 if(op.type().id() == ID_floatbv)
964 std::move(overflow_check),
965 "arithmetic overflow on floating-point typecast",
976 "arithmetic overflow on floating-point typecast",
985 else if(expr.
id()==ID_div)
992 std::move(overflow_check),
993 "arithmetic overflow on floating-point division",
1001 else if(expr.
id()==ID_mod)
1006 else if(expr.
id()==ID_unary_minus)
1011 else if(expr.
id()==ID_plus || expr.
id()==ID_mult ||
1012 expr.
id()==ID_minus)
1023 expr.
id()==ID_plus?
"addition":
1024 expr.
id()==ID_minus?
"subtraction":
1025 expr.
id()==ID_mult?
"multiplication":
"";
1028 std::move(overflow_check),
1029 "arithmetic overflow on floating-point " + kind,
1039 assert(expr.
id()!=ID_minus);
1056 if(expr.
type().
id()!=ID_floatbv)
1059 if(expr.
id()!=ID_plus &&
1060 expr.
id()!=ID_mult &&
1061 expr.
id()!=ID_div &&
1062 expr.
id()!=ID_minus)
1069 if(expr.
id()==ID_div)
1078 div_expr.op0(),
from_integer(0, div_expr.dividend().type())),
1080 div_expr.op1(),
from_integer(0, div_expr.divisor().type())));
1084 isnan=
or_exprt(zero_div_zero, div_inf);
1086 else if(expr.
id()==ID_mult)
1097 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())));
1101 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())),
1104 isnan=
or_exprt(inf_times_zero, zero_times_inf);
1106 else if(expr.
id()==ID_plus)
1127 else if(expr.
id()==ID_minus)
1166 if(expr.
op0().
type().
id()==ID_pointer &&
1175 "same object violation",
1181 for(
const auto &pointer : expr.
operands())
1188 for(
const auto &c : conditions)
1192 "pointer relation: " + c.description,
1193 "pointer arithmetic",
1209 if(expr.
id() != ID_plus && expr.
id() != ID_minus)
1214 "pointer arithmetic expected to have exactly 2 operands");
1220 for(
const auto &c : conditions)
1224 "pointer arithmetic: " + c.description,
1225 "pointer arithmetic",
1234 const exprt &src_expr,
1244 if(expr.
type().
id() == ID_empty)
1256 size = size_of_expr_opt.value();
1261 for(
const auto &c : conditions)
1265 "dereference failure: " + c.description,
1266 "pointer dereference",
1283 const exprt pointer =
1284 (expr.
id() == ID_r_ok || expr.
id() == ID_w_ok || expr.
id() == ID_rw_ok)
1290 if(pointer.
id() == ID_symbol)
1300 const exprt size = !size_of_expr_opt.has_value()
1302 : size_of_expr_opt.value();
1306 for(
const auto &c : conditions)
1311 "pointer primitives",
1323 return expr.
id() == ID_pointer_object || expr.
id() == ID_pointer_offset ||
1324 expr.
id() == ID_object_size || expr.
id() == ID_r_ok ||
1325 expr.
id() == ID_w_ok || expr.
id() == ID_rw_ok ||
1326 expr.
id() == ID_is_dynamic_object;
1330 const exprt &address,
1337 conditions.push_front(*maybe_null_condition);
1359 if(expr.
id() == ID_index)
1362 expr.
id() == ID_count_leading_zeros || expr.
id() == ID_count_trailing_zeros)
1374 if(array_type.
id()==ID_pointer)
1375 throw "index got pointer as array type";
1376 else if(array_type.
id()!=ID_array && array_type.
id()!=ID_vector)
1377 throw "bounds check expected array or vector type, got "
1386 if(index.
type().
id()!=ID_unsignedbv)
1390 index.
id() == ID_typecast &&
1397 const auto i = numeric_cast<mp_integer>(index);
1399 if(!i.has_value() || *i < 0)
1410 effective_offset, p_offset.
type())};
1417 effective_offset, ID_ge, std::move(zero));
1421 name +
" lower bound",
1432 const exprt &pointer=
1446 exprt in_bounds_of_some_explicit_allocation =
1452 std::move(in_bounds_of_some_explicit_allocation),
1457 name +
" dynamic object upper bound",
1466 const exprt &size=array_type.
id()==ID_array ?
1475 else if(size.
id()==ID_infinity)
1496 type_size_opt.value());
1500 name +
" upper bound",
1513 name +
" upper bound",
1527 if(expr.
id() == ID_count_leading_zeros)
1529 else if(expr.
id() == ID_count_trailing_zeros)
1536 "count " + name +
" zeros is undefined for value zero",
1544 const exprt &asserted_expr,
1546 const std::string &property_class,
1548 const exprt &src_expr,
1552 exprt simplified_expr =
1560 exprt guarded_expr =
1562 ? std::move(simplified_expr)
1565 if(
assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1569 std::move(guarded_expr), source_location)
1571 std::move(guarded_expr), source_location));
1573 std::string source_expr_string;
1576 t->source_location.set_comment(
comment +
" in " + source_expr_string);
1577 t->source_location.set_property_class(property_class);
1584 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1587 if(expr.
id() == ID_dereference)
1591 else if(expr.
id() == ID_index)
1599 for(
const auto &operand : expr.
operands())
1608 "'" + expr.
id_string() +
"' must be Boolean, but got " + expr.
pretty());
1610 guardt old_guard = guard;
1612 for(
const auto &op : expr.
operands())
1616 "'" + expr.
id_string() +
"' takes Boolean operands only, but got " +
1623 guard = std::move(old_guard);
1630 "first argument of if must be boolean, but got " + if_expr.
cond().
pretty());
1635 guardt old_guard = guard;
1638 guard = std::move(old_guard);
1642 guardt old_guard = guard;
1645 guard = std::move(old_guard);
1664 if(member_offset_opt.has_value())
1691 if(div_expr.
type().
id() == ID_signedbv)
1693 else if(div_expr.
type().
id() == ID_floatbv)
1702 if(expr.
type().
id() == ID_signedbv || expr.
type().
id() == ID_unsignedbv)
1707 expr.
operands().size() == 2 && expr.
id() == ID_minus &&
1708 expr.
operands()[0].type().id() == ID_pointer &&
1709 expr.
operands()[1].type().id() == ID_pointer)
1714 else if(expr.
type().
id() == ID_floatbv)
1719 else if(expr.
type().
id() == ID_pointer)
1728 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1731 if(expr.
id() == ID_address_of)
1736 else if(expr.
id() == ID_and || expr.
id() == ID_or)
1741 else if(expr.
id() == ID_if)
1747 expr.
id() == ID_member &&
1757 if(expr.
type().
id() == ID_c_enum_tag)
1760 if(expr.
id()==ID_index)
1764 else if(expr.
id()==ID_div)
1768 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr)
1772 if(expr.
id()==ID_shl && expr.
type().
id()==ID_signedbv)
1775 else if(expr.
id()==ID_mod)
1780 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
1781 expr.
id()==ID_mult ||
1782 expr.
id()==ID_unary_minus)
1786 else if(expr.
id()==ID_typecast)
1788 else if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1789 expr.
id()==ID_ge || expr.
id()==ID_gt)
1791 else if(expr.
id()==ID_dereference)
1800 expr.
id() == ID_count_leading_zeros || expr.
id() == ID_count_trailing_zeros)
1815 bool modified =
false;
1820 if(op_result.has_value())
1827 if(expr.
id() == ID_r_ok || expr.
id() == ID_w_ok || expr.
id() == ID_rw_ok)
1831 expr.
operands().size() == 2,
"r/w_ok must have two operands");
1838 for(
const auto &c : conditions)
1839 conjuncts.push_back(c.assertion);
1844 return std::move(expr);
1857 if(flag != new_value)
1868 *flag_pair.first = flag_pair.second;
1876 const irep_idt &function_identifier,
1881 const auto &function_symbol =
ns.
lookup(function_identifier);
1882 mode = function_symbol.mode;
1884 bool did_something =
false;
1887 util_make_unique<local_bitvector_analysist>(goto_function,
ns);
1898 for(
const auto &d : pragmas)
1900 if(d.first ==
"disable:bounds-check")
1902 else if(d.first ==
"disable:pointer-check")
1904 else if(d.first ==
"disable:memory-leak-check")
1906 else if(d.first ==
"disable:div-by-zero-check")
1908 else if(d.first ==
"disable:enum-range-check")
1910 else if(d.first ==
"disable:signed-overflow-check")
1912 else if(d.first ==
"disable:unsigned-overflow-check")
1914 else if(d.first ==
"disable:pointer-overflow-check")
1916 else if(d.first ==
"disable:float-overflow-check")
1918 else if(d.first ==
"disable:conversion-check")
1920 else if(d.first ==
"disable:undefined-shift-check")
1922 else if(d.first ==
"disable:nan-check")
1924 else if(d.first ==
"disable:pointer-primitive-check")
1942 return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
1943 expr.id() == ID_rw_ok;
1947 if(rw_ok_cond.has_value())
1962 t->source_location.set_property_class(
"error label");
1963 t->source_location.set_comment(
"error label "+label);
1964 t->source_location.set(
"user-provided",
true);
1971 const irep_idt &statement = code.get_statement();
1973 if(statement==ID_expression)
1977 else if(statement==ID_printf)
1979 for(
const auto &op : code.operands())
2000 return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
2001 expr.id() == ID_rw_ok;
2006 if(rw_ok_cond.has_value())
2009 new_assign.
rhs() = *rw_ok_cond;
2022 !i.
call_arguments().empty() &&
function.type().id() == ID_code &&
2038 "this is null on method invocation",
2039 "pointer dereference",
2062 return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
2063 expr.id() == ID_rw_ok;
2068 if(rw_ok_cond.has_value())
2069 return_value = *rw_ok_cond;
2089 "pointer dereference",
2107 did_something =
true;
2115 did_something =
true;
2133 std::move(address_of_expr),
2142 variable.
type().
id() == ID_pointer &&
2143 function_identifier !=
"alloca" &&
2145 "return_value___builtin_alloca" ||
2147 "return_value_alloca"))
2151 exprt alloca_result =
2155 std::move(alloca_result),
2184 "dynamically allocated memory never freed",
2194 if(instruction.source_location.is_nil())
2196 instruction.source_location.id(
irep_idt());
2198 if(!it->source_location.get_file().empty())
2199 instruction.source_location.set_file(it->source_location.get_file());
2201 if(!it->source_location.get_line().empty())
2202 instruction.source_location.set_line(it->source_location.get_line());
2204 if(!it->source_location.get_function().empty())
2205 instruction.source_location.set_function(
2206 it->source_location.get_function());
2208 if(!it->source_location.get_column().empty())
2210 instruction.source_location.set_column(
2211 it->source_location.get_column());
2214 if(!it->source_location.get_java_bytecode_index().empty())
2216 instruction.source_location.set_java_bytecode_index(
2217 it->source_location.get_java_bytecode_index());
2239 const exprt &address,
2255 const exprt in_bounds_of_some_explicit_allocation =
2270 in_bounds_of_some_explicit_allocation,
2272 "deallocated dynamic object"));
2279 in_bounds_of_some_explicit_allocation,
2286 const or_exprt object_bounds_violation(
2292 in_bounds_of_some_explicit_allocation,
2294 "pointer outside dynamic object bounds"));
2299 const or_exprt object_bounds_violation(
2305 in_bounds_of_some_explicit_allocation,
2307 "pointer outside object bounds"));
2315 "invalid integer address"));
2322 const exprt &address,
2335 return {
conditiont{not_eq_null,
"reference is null"}};
2349 const exprt &pointer,
2363 std::move(upper_bound), ID_le,
plus_exprt{a.first, a.second}};
2365 alloc_disjuncts.push_back(
2366 and_exprt{std::move(lb_check), std::move(ub_check)});
2372 const irep_idt &function_identifier,
2378 goto_check.goto_check(function_identifier, goto_function);
2388 goto_check.collect_allocations(goto_functions);
2392 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 r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
std::string array_name(const namespacet &ns, const exprt &expr)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
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...
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
void set_assign(code_assignt c)
Set the assignment for ASSIGN.
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)
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 floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
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.
void bounds_check_bit_count(const unary_exprt &, const guardt &)
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
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
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...
Generic base class for unary expressions.
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
bool is_true() const
Return whether the expression is a constant representing true.
struct configt::ansi_ct ansi_c
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
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.
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
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.
static const exprt & root_object(const exprt &expr)
const codet & get_other() const
Get the statement for OTHER.
const codet & get_code() const
Get the code represented by this instruction.
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.
const exprt & pointer() const
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().
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.
#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 symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const std::string & id2string(const irep_idt &d)
void float_overflow_check(const exprt &, const guardt &)
bool enable_pointer_check
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
#define forall_operands(it, expr)
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
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
void bounds_check(const exprt &, const guardt &)
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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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)
bool is_set_return_value() const
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
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, w_ok and rw_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 &)
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
void collect_allocations(const goto_functionst &goto_functions)
Fill the list of allocations allocationst with <address, size> for every allocation instruction.
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 SET_RETURN_VALUE instruction.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
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
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 Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
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
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
void bounds_check_index(const index_exprt &, const guardt &)
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 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)
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 exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
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.
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
const memberst & members() const
std::list< std::pair< bool *, bool > > flags_to_reset
enum configt::cppt::cpp_standardt cpp_standard