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())
313 args[0].type().id()!=ID_unsignedbv ||
314 args[1].type().id()!=ID_unsignedbv)
315 throw "expected two unsigned arguments to "
318 assert(args[0].type()==args[1].type());
326 if(lhs.
id()==ID_index)
328 else if(lhs.
id()==ID_member)
330 else if(lhs.
id()==ID_symbol)
386 std::vector<exprt> disjuncts;
387 for(
const auto &enum_value : enum_values)
416 if(distance_type.
id()==ID_signedbv)
423 "shift distance is negative",
432 if(op_type.
id()==ID_unsignedbv || op_type.
id()==ID_signedbv)
439 "shift distance too large",
445 if(op_type.
id()==ID_signedbv && expr.
id()==ID_shl)
452 "shift operand is negative",
463 "shift of non-integer type",
498 const auto &type = expr.
type();
500 if(type.id() == ID_signedbv)
514 or_exprt(int_min_neq, minus_one_neq),
515 "result of signed mod is not representable",
533 if(type.
id()!=ID_signedbv &&
534 type.
id()!=ID_unsignedbv)
537 if(expr.
id()==ID_typecast)
542 const typet &old_type = op.type();
544 if(type.
id()==ID_signedbv)
548 if(old_type.
id()==ID_signedbv)
551 if(new_width>=old_width)
561 and_exprt(no_overflow_lower, no_overflow_upper),
562 "arithmetic overflow on signed type conversion",
568 else if(old_type.
id()==ID_unsignedbv)
571 if(new_width>=old_width+1)
579 "arithmetic overflow on unsigned to signed type conversion",
585 else if(old_type.
id()==ID_floatbv)
599 and_exprt(no_overflow_lower, no_overflow_upper),
600 "arithmetic overflow on float to signed integer type conversion",
607 else if(type.
id()==ID_unsignedbv)
611 if(old_type.
id()==ID_signedbv)
615 if(new_width>=old_width-1)
623 "arithmetic overflow on signed to unsigned type conversion",
639 and_exprt(no_overflow_lower, no_overflow_upper),
640 "arithmetic overflow on signed to unsigned type conversion",
647 else if(old_type.
id()==ID_unsignedbv)
650 if(new_width>=old_width)
658 "arithmetic overflow on unsigned to unsigned type conversion",
664 else if(old_type.
id()==ID_floatbv)
678 and_exprt(no_overflow_lower, no_overflow_upper),
679 "arithmetic overflow on float to unsigned integer type conversion",
708 if(expr.
id()==ID_div)
711 if(type.
id()==ID_signedbv)
722 "arithmetic overflow on signed division",
731 else if(expr.
id()==ID_unary_minus)
733 if(type.
id()==ID_signedbv)
743 "arithmetic overflow on signed unary minus",
752 else if(expr.
id() == ID_shl)
754 if(type.
id() == ID_signedbv)
757 const auto &op = shl_expr.op();
759 const auto op_width = op_type.get_width();
760 const auto &distance = shl_expr.distance();
761 const auto &distance_type = distance.type();
765 exprt neg_value_shift;
767 if(op_type.id() == ID_unsignedbv)
775 exprt neg_dist_shift;
777 if(distance_type.id() == ID_unsignedbv)
786 distance, ID_gt,
from_integer(op_width, distance_type));
791 new_type.set_width(op_width * 2);
802 bool allow_shift_into_sign_bit =
true;
810 allow_shift_into_sign_bit =
false;
813 else if(
mode == ID_cpp)
819 allow_shift_into_sign_bit =
false;
823 const unsigned number_of_top_bits =
824 allow_shift_into_sign_bit ? op_width : op_width + 1;
828 new_type.get_width() - 1,
829 new_type.get_width() - number_of_top_bits,
832 const exprt top_bits_zero =
846 "arithmetic overflow on signed shl",
864 for(std::size_t i=1; i<expr.
operands().size(); i++)
877 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
881 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
888 else if(expr.
operands().size() == 2)
890 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
895 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
906 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
910 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
928 if(type.
id()!=ID_floatbv)
933 if(expr.
id()==ID_typecast)
938 if(op.type().id() == ID_floatbv)
944 std::move(overflow_check),
945 "arithmetic overflow on floating-point typecast",
956 "arithmetic overflow on floating-point typecast",
965 else if(expr.
id()==ID_div)
972 std::move(overflow_check),
973 "arithmetic overflow on floating-point division",
981 else if(expr.
id()==ID_mod)
986 else if(expr.
id()==ID_unary_minus)
991 else if(expr.
id()==ID_plus || expr.
id()==ID_mult ||
1003 expr.
id()==ID_plus?
"addition":
1004 expr.
id()==ID_minus?
"subtraction":
1005 expr.
id()==ID_mult?
"multiplication":
"";
1008 std::move(overflow_check),
1009 "arithmetic overflow on floating-point " + kind,
1019 assert(expr.
id()!=ID_minus);
1036 if(expr.
type().
id()!=ID_floatbv)
1039 if(expr.
id()!=ID_plus &&
1040 expr.
id()!=ID_mult &&
1041 expr.
id()!=ID_div &&
1042 expr.
id()!=ID_minus)
1049 if(expr.
id()==ID_div)
1058 div_expr.op0(),
from_integer(0, div_expr.dividend().type())),
1060 div_expr.op1(),
from_integer(0, div_expr.divisor().type())));
1064 isnan=
or_exprt(zero_div_zero, div_inf);
1066 else if(expr.
id()==ID_mult)
1077 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())));
1081 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())),
1084 isnan=
or_exprt(inf_times_zero, zero_times_inf);
1086 else if(expr.
id()==ID_plus)
1107 else if(expr.
id()==ID_minus)
1146 if(expr.
op0().
type().
id()==ID_pointer &&
1155 "same object violation",
1161 for(
const auto &pointer : expr.
operands())
1168 for(
const auto &c : conditions)
1172 "pointer relation: " + c.description,
1173 "pointer arithmetic",
1189 if(expr.
id() != ID_plus && expr.
id() != ID_minus)
1194 "pointer arithmetic expected to have exactly 2 operands");
1200 for(
const auto &c : conditions)
1204 "pointer arithmetic: " + c.description,
1205 "pointer arithmetic",
1214 const exprt &src_expr,
1224 if(expr.
type().
id() == ID_empty)
1236 size = size_of_expr_opt.value();
1241 for(
const auto &c : conditions)
1245 "dereference failure: " + c.description,
1246 "pointer dereference",
1263 const exprt pointer = (expr.
id() == ID_r_ok || expr.
id() == ID_w_ok)
1269 if(pointer.
id() == ID_symbol)
1279 const exprt size = !size_of_expr_opt.has_value()
1281 : size_of_expr_opt.value();
1285 for(
const auto &c : conditions)
1290 "pointer primitives",
1302 return expr.
id() == ID_pointer_object || expr.
id() == ID_pointer_offset ||
1303 expr.
id() == ID_object_size || expr.
id() == ID_r_ok ||
1304 expr.
id() == ID_w_ok || expr.
id() == ID_is_dynamic_object;
1308 const exprt &address,
1315 conditions.push_front(*maybe_null_condition);
1337 if(expr.
id() == ID_index)
1339 else if(expr.
id() == ID_count_leading_zeros)
1349 if(array_type.
id()==ID_pointer)
1350 throw "index got pointer as array type";
1351 else if(array_type.
id()!=ID_array && array_type.
id()!=ID_vector)
1352 throw "bounds check expected array or vector type, got "
1361 if(index.
type().
id()!=ID_unsignedbv)
1365 index.
id() == ID_typecast &&
1372 const auto i = numeric_cast<mp_integer>(index);
1374 if(!i.has_value() || *i < 0)
1382 assert(p_offset.
type()==effective_offset.
type());
1384 effective_offset=
plus_exprt(p_offset, effective_offset);
1391 effective_offset, ID_ge, std::move(zero));
1395 name +
" lower bound",
1408 const exprt &pointer=
1418 assert(effective_offset.
op0().
type()==effective_offset.
op1().
type());
1420 const auto size_casted =
1425 exprt in_bounds_of_some_explicit_allocation =
1431 std::move(in_bounds_of_some_explicit_allocation),
1437 name +
" dynamic object upper bound",
1445 if(type_size_opt.has_value())
1464 const exprt &size=array_type.
id()==ID_array ?
1473 else if(size.
id()==ID_infinity)
1494 type_size_opt.value());
1498 name +
" upper bound",
1514 name +
" upper bound",
1528 "count leading zeros argument",
1536 const exprt &asserted_expr,
1538 const std::string &property_class,
1540 const exprt &src_expr,
1544 exprt simplified_expr =
1552 exprt guarded_expr =
1554 ? std::move(simplified_expr)
1557 if(
assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1561 std::move(guarded_expr), source_location)
1563 std::move(guarded_expr), source_location));
1565 std::string source_expr_string;
1568 t->source_location.set_comment(
comment +
" in " + source_expr_string);
1569 t->source_location.set_property_class(property_class);
1576 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1579 if(expr.
id() == ID_dereference)
1583 else if(expr.
id() == ID_index)
1591 for(
const auto &operand : expr.
operands())
1600 "'" + expr.
id_string() +
"' must be Boolean, but got " + expr.
pretty());
1602 guardt old_guard = guard;
1604 for(
const auto &op : expr.
operands())
1608 "'" + expr.
id_string() +
"' takes Boolean operands only, but got " +
1615 guard = std::move(old_guard);
1622 "first argument of if must be boolean, but got " + if_expr.
cond().
pretty());
1627 guardt old_guard = guard;
1630 guard = std::move(old_guard);
1634 guardt old_guard = guard;
1637 guard = std::move(old_guard);
1656 if(member_offset_opt.has_value())
1683 if(div_expr.
type().
id() == ID_signedbv)
1685 else if(div_expr.
type().
id() == ID_floatbv)
1694 if(expr.
type().
id() == ID_signedbv || expr.
type().
id() == ID_unsignedbv)
1699 expr.
operands().size() == 2 && expr.
id() == ID_minus &&
1700 expr.
operands()[0].type().id() == ID_pointer &&
1701 expr.
operands()[1].type().id() == ID_pointer)
1706 else if(expr.
type().
id() == ID_floatbv)
1711 else if(expr.
type().
id() == ID_pointer)
1720 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1723 if(expr.
id() == ID_address_of)
1728 else if(expr.
id() == ID_and || expr.
id() == ID_or)
1733 else if(expr.
id() == ID_if)
1739 expr.
id() == ID_member &&
1749 if(expr.
type().
id() == ID_c_enum_tag)
1752 if(expr.
id()==ID_index)
1756 else if(expr.
id()==ID_div)
1760 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr)
1764 if(expr.
id()==ID_shl && expr.
type().
id()==ID_signedbv)
1767 else if(expr.
id()==ID_mod)
1772 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
1773 expr.
id()==ID_mult ||
1774 expr.
id()==ID_unary_minus)
1778 else if(expr.
id()==ID_typecast)
1780 else if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1781 expr.
id()==ID_ge || expr.
id()==ID_gt)
1783 else if(expr.
id()==ID_dereference)
1791 else if(expr.
id() == ID_count_leading_zeros)
1806 bool modified =
false;
1811 if(op_result.has_value())
1818 if(expr.
id() == ID_r_ok || expr.
id() == ID_w_ok)
1822 expr.
operands().size() == 2,
"r/w_ok must have two operands");
1829 for(
const auto &c : conditions)
1830 conjuncts.push_back(c.assertion);
1835 return std::move(expr);
1848 if(flag != new_value)
1859 *flag_pair.first = flag_pair.second;
1867 const irep_idt &function_identifier,
1872 const auto &function_symbol =
ns.
lookup(function_identifier);
1873 mode = function_symbol.mode;
1875 bool did_something =
false;
1878 util_make_unique<local_bitvector_analysist>(goto_function,
ns);
1889 for(
const auto &d : pragmas)
1891 if(d.first ==
"disable:bounds-check")
1893 else if(d.first ==
"disable:pointer-check")
1895 else if(d.first ==
"disable:memory-leak-check")
1897 else if(d.first ==
"disable:div-by-zero-check")
1899 else if(d.first ==
"disable:enum-range-check")
1901 else if(d.first ==
"disable:signed-overflow-check")
1903 else if(d.first ==
"disable:unsigned-overflow-check")
1905 else if(d.first ==
"disable:pointer-overflow-check")
1907 else if(d.first ==
"disable:float-overflow-check")
1909 else if(d.first ==
"disable:conversion-check")
1911 else if(d.first ==
"disable:undefined-shift-check")
1913 else if(d.first ==
"disable:nan-check")
1915 else if(d.first ==
"disable:pointer-primitive-check")
1933 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1937 if(rw_ok_cond.has_value())
1952 t->source_location.set_property_class(
"error label");
1953 t->source_location.set_comment(
"error label "+label);
1954 t->source_location.set(
"user-provided",
true);
1961 const irep_idt &statement = code.get_statement();
1963 if(statement==ID_expression)
1967 else if(statement==ID_printf)
1969 for(
const auto &op : code.operands())
1990 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1995 if(rw_ok_cond.has_value())
1998 new_assign.
rhs() = *rw_ok_cond;
2011 !code_function_call.
arguments().empty() &&
2028 "this is null on method invocation",
2029 "pointer dereference",
2036 for(
const auto &op : code_function_call.
operands())
2049 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
2054 if(rw_ok_cond.has_value())
2055 return_value = *rw_ok_cond;
2075 "pointer dereference",
2093 did_something =
true;
2101 did_something =
true;
2119 std::move(address_of_expr),
2148 "dynamically allocated memory never freed",
2158 if(instruction.source_location.is_nil())
2160 instruction.source_location.id(
irep_idt());
2162 if(!it->source_location.get_file().empty())
2163 instruction.source_location.set_file(it->source_location.get_file());
2165 if(!it->source_location.get_line().empty())
2166 instruction.source_location.set_line(it->source_location.get_line());
2168 if(!it->source_location.get_function().empty())
2169 instruction.source_location.set_function(
2170 it->source_location.get_function());
2172 if(!it->source_location.get_column().empty())
2174 instruction.source_location.set_column(
2175 it->source_location.get_column());
2178 if(!it->source_location.get_java_bytecode_index().empty())
2180 instruction.source_location.set_java_bytecode_index(
2181 it->source_location.get_java_bytecode_index());
2203 const exprt &address,
2219 const exprt in_bounds_of_some_explicit_allocation =
2234 in_bounds_of_some_explicit_allocation,
2236 "deallocated dynamic object"));
2243 in_bounds_of_some_explicit_allocation,
2250 const or_exprt object_bounds_violation(
2256 in_bounds_of_some_explicit_allocation,
2259 "pointer outside dynamic object bounds"));
2264 const or_exprt object_bounds_violation(
2270 in_bounds_of_some_explicit_allocation,
2274 "pointer outside object bounds"));
2282 "invalid integer address"));
2289 const exprt &address,
2302 return {
conditiont{not_eq_null,
"reference is null"}};
2316 const exprt &pointer,
2330 std::move(upper_bound), ID_le,
plus_exprt{a.first, a.second}};
2332 alloc_disjuncts.push_back(
2333 and_exprt{std::move(lb_check), std::move(ub_check)});
2339 const irep_idt &function_identifier,
2345 goto_check.goto_check(function_identifier, goto_function);
2355 goto_check.collect_allocations(goto_functions);
2359 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.
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...
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
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 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().
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.
#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)
void bounds_check_clz(const count_leading_zeros_exprt &, const guardt &)
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.
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
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)
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 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.
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.
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
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 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)
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
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
API to expression classes for bitvectors.
const memberst & members() const
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
std::list< std::pair< bool *, bool > > flags_to_reset
enum configt::cppt::cpp_standardt cpp_standard