Go to the documentation of this file.
185 const exprt &src_expr,
206 const exprt &asserted_expr,
208 const std::string &property_class,
210 const exprt &src_expr,
276 args[0].type().id()!=ID_unsignedbv ||
277 args[1].type().id()!=ID_unsignedbv)
278 throw "expected two unsigned arguments to "
281 assert(args[0].type()==args[1].type());
288 if(lhs.
id()==ID_index)
290 else if(lhs.
id()==ID_member)
292 else if(lhs.
id()==ID_symbol)
344 std::vector<exprt> disjuncts;
345 for(
const auto &enum_value : enum_values)
374 if(distance_type.
id()==ID_signedbv)
381 "shift distance is negative",
390 if(op_type.
id()==ID_unsignedbv || op_type.
id()==ID_signedbv)
397 "shift distance too large",
403 if(op_type.
id()==ID_signedbv && expr.
id()==ID_shl)
410 "shift operand is negative",
421 "shift of non-integer type",
456 const auto &type = expr.
type();
458 if(type.id() == ID_signedbv)
472 or_exprt(int_min_neq, minus_one_neq),
473 "result of signed mod is not representable",
491 if(type.
id()!=ID_signedbv &&
492 type.
id()!=ID_unsignedbv)
495 if(expr.
id()==ID_typecast)
500 const typet &old_type = op.type();
502 if(type.
id()==ID_signedbv)
506 if(old_type.
id()==ID_signedbv)
509 if(new_width>=old_width)
519 and_exprt(no_overflow_lower, no_overflow_upper),
520 "arithmetic overflow on signed type conversion",
526 else if(old_type.
id()==ID_unsignedbv)
529 if(new_width>=old_width+1)
537 "arithmetic overflow on unsigned to signed type conversion",
543 else if(old_type.
id()==ID_floatbv)
557 and_exprt(no_overflow_lower, no_overflow_upper),
558 "arithmetic overflow on float to signed integer type conversion",
565 else if(type.
id()==ID_unsignedbv)
569 if(old_type.
id()==ID_signedbv)
573 if(new_width>=old_width-1)
581 "arithmetic overflow on signed to unsigned type conversion",
597 and_exprt(no_overflow_lower, no_overflow_upper),
598 "arithmetic overflow on signed to unsigned type conversion",
605 else if(old_type.
id()==ID_unsignedbv)
608 if(new_width>=old_width)
616 "arithmetic overflow on unsigned to unsigned type conversion",
622 else if(old_type.
id()==ID_floatbv)
636 and_exprt(no_overflow_lower, no_overflow_upper),
637 "arithmetic overflow on float to unsigned integer type conversion",
666 if(expr.
id()==ID_div)
669 if(type.
id()==ID_signedbv)
680 "arithmetic overflow on signed division",
689 else if(expr.
id()==ID_unary_minus)
691 if(type.
id()==ID_signedbv)
701 "arithmetic overflow on signed unary minus",
710 else if(expr.
id() == ID_shl)
712 if(type.
id() == ID_signedbv)
715 const auto &op = shl_expr.op();
717 const auto op_width = op_type.get_width();
718 const auto &distance = shl_expr.distance();
719 const auto &distance_type = distance.type();
723 exprt neg_value_shift;
725 if(op_type.id() == ID_unsignedbv)
733 exprt neg_dist_shift;
735 if(distance_type.id() == ID_unsignedbv)
744 distance, ID_gt,
from_integer(op_width, distance_type));
749 new_type.set_width(op_width * 2);
760 bool allow_shift_into_sign_bit =
true;
768 allow_shift_into_sign_bit =
false;
771 else if(
mode == ID_cpp)
777 allow_shift_into_sign_bit =
false;
781 const unsigned number_of_top_bits =
782 allow_shift_into_sign_bit ? op_width : op_width + 1;
786 new_type.get_width() - 1,
787 new_type.get_width() - number_of_top_bits,
790 const exprt top_bits_zero =
804 "arithmetic overflow on signed shl",
822 for(std::size_t i=1; i<expr.
operands().size(); i++)
839 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
843 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
853 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
857 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
875 if(type.
id()!=ID_floatbv)
880 if(expr.
id()==ID_typecast)
885 if(op.type().id() == ID_floatbv)
891 std::move(overflow_check),
892 "arithmetic overflow on floating-point typecast",
903 "arithmetic overflow on floating-point typecast",
912 else if(expr.
id()==ID_div)
919 std::move(overflow_check),
920 "arithmetic overflow on floating-point division",
928 else if(expr.
id()==ID_mod)
933 else if(expr.
id()==ID_unary_minus)
938 else if(expr.
id()==ID_plus || expr.
id()==ID_mult ||
950 expr.
id()==ID_plus?
"addition":
951 expr.
id()==ID_minus?
"subtraction":
952 expr.
id()==ID_mult?
"multiplication":
"";
955 std::move(overflow_check),
956 "arithmetic overflow on floating-point " + kind,
966 assert(expr.
id()!=ID_minus);
983 if(expr.
type().
id()!=ID_floatbv)
986 if(expr.
id()!=ID_plus &&
987 expr.
id()!=ID_mult &&
996 if(expr.
id()==ID_div)
1005 div_expr.op0(),
from_integer(0, div_expr.dividend().type())),
1007 div_expr.op1(),
from_integer(0, div_expr.divisor().type())));
1011 isnan=
or_exprt(zero_div_zero, div_inf);
1013 else if(expr.
id()==ID_mult)
1024 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())));
1028 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())),
1031 isnan=
or_exprt(inf_times_zero, zero_times_inf);
1033 else if(expr.
id()==ID_plus)
1054 else if(expr.
id()==ID_minus)
1093 if(expr.
op0().
type().
id()==ID_pointer &&
1104 "same object violation",
1120 if(expr.
id() != ID_plus && expr.
id() != ID_minus)
1125 "pointer arithmetic expected to have exactly 2 operands");
1132 "pointer arithmetic overflow on " + expr.
id_string(),
1141 const exprt &src_expr,
1152 auto conditions =
address_check(pointer, size_of_expr_opt.value());
1154 for(
const auto &c : conditions)
1158 "dereference failure: " + c.description,
1159 "pointer dereference",
1183 return {
conditiont(not_eq_null,
"reference is null")};
1203 alloc_disjuncts.push_back(
and_exprt(lb_check, ub_check));
1206 const exprt in_bounds_of_some_explicit_allocation =
1213 in_bounds_of_some_explicit_allocation,
1226 conditions.push_back(
1229 "pointer uninitialized"});
1236 in_bounds_of_some_explicit_allocation,
1238 "deallocated dynamic object"));
1245 in_bounds_of_some_explicit_allocation,
1252 const or_exprt dynamic_bounds_violation(
1258 in_bounds_of_some_explicit_allocation,
1261 "pointer outside dynamic object bounds"));
1268 const or_exprt object_bounds_violation(
1274 in_bounds_of_some_explicit_allocation,
1278 "pointer outside object bounds"));
1286 "invalid integer address"));
1311 if(array_type.
id()==ID_pointer)
1312 throw "index got pointer as array type";
1313 else if(array_type.
id()!=ID_array && array_type.
id()!=ID_vector)
1314 throw "bounds check expected array or vector type, got "
1323 if(index.
type().
id()!=ID_unsignedbv)
1327 index.
id() == ID_typecast &&
1334 const auto i = numeric_cast<mp_integer>(index);
1336 if(!i.has_value() || *i < 0)
1344 assert(p_offset.
type()==effective_offset.
type());
1346 effective_offset=
plus_exprt(p_offset, effective_offset);
1353 effective_offset, ID_ge, std::move(zero));
1357 name +
" lower bound",
1370 const exprt &pointer=
1380 assert(effective_offset.
op0().
type()==effective_offset.
op1().
type());
1382 const auto size_casted =
1399 std::move(upper_bound), ID_lt,
plus_exprt{a.first, a.second}};
1401 alloc_disjuncts.push_back(
1402 and_exprt{std::move(lower_bound_check), std::move(upper_bound_check)});
1405 exprt in_bounds_of_some_explicit_allocation =
disjunction(alloc_disjuncts);
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)
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)
1662 else if(expr.
type().
id() == ID_floatbv)
1667 else if(expr.
type().
id() == ID_pointer)
1676 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1679 if(expr.
id() == ID_address_of)
1684 else if(expr.
id() == ID_and || expr.
id() == ID_or)
1689 else if(expr.
id() == ID_if)
1695 expr.
id() == ID_member &&
1705 if(expr.
type().
id() == ID_c_enum_tag)
1708 if(expr.
id()==ID_index)
1712 else if(expr.
id()==ID_div)
1716 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr)
1720 if(expr.
id()==ID_shl && expr.
type().
id()==ID_signedbv)
1723 else if(expr.
id()==ID_mod)
1728 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
1729 expr.
id()==ID_mult ||
1730 expr.
id()==ID_unary_minus)
1734 else if(expr.
id()==ID_typecast)
1736 else if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1737 expr.
id()==ID_ge || expr.
id()==ID_gt)
1739 else if(expr.
id()==ID_dereference)
1754 bool modified =
false;
1759 if(op_result.has_value())
1766 if(expr.
id() == ID_r_ok || expr.
id() == ID_w_ok)
1770 expr.
operands().size() == 2,
"r/w_ok must have two operands");
1772 const auto conditions =
1777 for(
const auto &c : conditions)
1778 conjuncts.push_back(c.assertion);
1783 return std::move(expr);
1796 if(flag != new_value)
1807 *flag_pair.first = flag_pair.second;
1815 const irep_idt &function_identifier,
1820 const auto &function_symbol =
ns.
lookup(function_identifier);
1821 mode = function_symbol.mode;
1823 bool did_something =
false;
1826 util_make_unique<local_bitvector_analysist>(goto_function,
ns);
1837 for(
const auto &d : pragmas)
1839 if(d.first ==
"disable:bounds-check")
1841 else if(d.first ==
"disable:pointer-check")
1843 else if(d.first ==
"disable:memory-leak-check")
1845 else if(d.first ==
"disable:div-by-zero-check")
1847 else if(d.first ==
"disable:enum-range-check")
1849 else if(d.first ==
"disable:signed-overflow-check")
1851 else if(d.first ==
"disable:unsigned-overflow-check")
1853 else if(d.first ==
"disable:pointer-overflow-check")
1855 else if(d.first ==
"disable:float-overflow-check")
1857 else if(d.first ==
"disable:conversion-check")
1859 else if(d.first ==
"disable:undefined-shift-check")
1861 else if(d.first ==
"disable:nan-check")
1879 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1883 if(rw_ok_cond.has_value())
1898 t->source_location.set_property_class(
"error label");
1899 t->source_location.set_comment(
"error label "+label);
1900 t->source_location.set(
"user-provided",
true);
1907 const irep_idt &statement = code.get_statement();
1909 if(statement==ID_expression)
1913 else if(statement==ID_printf)
1915 for(
const auto &op : code.operands())
1936 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1941 if(rw_ok_cond.has_value())
1954 !code_function_call.
arguments().empty() &&
1971 "this is null on method invocation",
1972 "pointer dereference",
1979 for(
const auto &op : code_function_call.
operands())
1995 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
2000 if(rw_ok_cond.has_value())
2001 return_value = *rw_ok_cond;
2021 "pointer dereference",
2039 did_something =
true;
2047 did_something =
true;
2066 std::move(address_of_expr),
2095 "dynamically allocated memory never freed",
2105 if(i_it->source_location.is_nil())
2107 i_it->source_location.id(
irep_idt());
2109 if(!it->source_location.get_file().empty())
2110 i_it->source_location.set_file(it->source_location.get_file());
2112 if(!it->source_location.get_line().empty())
2113 i_it->source_location.set_line(it->source_location.get_line());
2115 if(!it->source_location.get_function().empty())
2116 i_it->source_location.set_function(
2117 it->source_location.get_function());
2119 if(!it->source_location.get_column().empty())
2120 i_it->source_location.set_column(it->source_location.get_column());
2122 if(!it->source_location.get_java_bytecode_index().empty())
2123 i_it->source_location.set_java_bytecode_index(
2124 it->source_location.get_java_bytecode_index());
2144 const irep_idt &function_identifier,
2150 goto_check.goto_check(function_identifier, goto_function);
2160 goto_check.collect_allocations(goto_functions);
2164 goto_check.goto_check(it->first, it->second);
std::pair< exprt, exprt > allocationt
std::list< allocationt > allocationst
#define Forall_goto_program_instructions(it, program)
const irep_idt & get_identifier() const
std::string array_name(const exprt &)
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
std::string array_name(const namespacet &ns, const exprt &expr)
static exprt conditional_cast(const exprt &expr, const typet &type)
goto_programt::const_targett current_target
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
A base class for multi-ary expressions Associativity is not specified.
const irep_idt & get_property_class() const
source_locationt source_location
The location of the instruction in the source file.
const typet & subtype() const
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
void bounds_check(const index_exprt &, const guardt &)
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
bool enable_div_by_zero_check
bool enable_undefined_shift_check
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
void set_function(const irep_idt &function)
guard_managert guard_manager
exprt null_pointer(const exprt &pointer)
#define CHECK_RETURN(CONDITION)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
The type of an expression, extends irept.
const irept::named_subt & get_pragmas() const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
typet type
Type of symbol.
Operator to dereference a pointer.
bool is_dynamic_heap() const
The trinary if-then-else operator.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
bool enable_built_in_assertions
std::vector< c_enum_membert > memberst
void check_rec_address(const exprt &expr, guardt &guard)
Check an address-of expression: if it is a dereference then check the pointer if it is an index then ...
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.
~flag_resett()
Restore the values of all flags that have been modified via set_flag.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
The plus expression Associativity is not specified.
Set a Boolean flag to a new value (via set_flag) and restore the previous value when the entire objec...
void pointer_validity_check(const dereference_exprt &expr, const exprt &src_expr, const guardt &guard)
Generates VCCs for the validity of the given dereferencing operation.
Base class for all expressions.
bool enable_conversion_check
void check_rec_div(const div_exprt &div_expr, guardt &guard)
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numb...
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
std::list< conditiont > conditionst
std::list< std::string > value_listt
exprt dynamic_object(const exprt &pointer)
bool is_true() const
Return whether the expression is a constant representing true.
struct configt::ansi_ct ansi_c
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
void pointer_rel_check(const binary_relation_exprt &, const guardt &)
Expression to hold a symbol (variable)
void nan_check(const exprt &, const guardt &)
bool enable_memory_leak_check
void enum_range_check(const exprt &, const guardt &)
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Fixed-width bit-vector with unsigned binary interpretation.
const codet & get_other() const
Get the statement for OTHER.
bool enable_unsigned_overflow_check
bool enable_float_overflow_check
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
void mod_by_zero_check(const mod_exprt &, const guardt &)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
This is unused by this implementation of guards, but can be used by other implementations of the same...
typet & type()
Return the type of the expression.
void pointer_overflow_check(const exprt &, const guardt &)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
void check_rec_logical_op(const exprt &expr, guardt &guard)
Check a logical operation: check each operand in separation while extending the guarding condition as...
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
void check(const exprt &expr)
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
void check_rec(const exprt &expr, guardt &guard)
Recursively descend into expr and run the appropriate check for each sub-expression,...
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
conditionst address_check(const exprt &address, const exprt &size)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
The null pointer constant.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
void float_overflow_check(const exprt &, const guardt &)
bool enable_pointer_check
codet code
Do not read or modify directly – use get_X() instead.
#define forall_operands(it, expr)
const exprt & struct_op() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
void add(const exprt &expr)
#define PRECONDITION(CONDITION)
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
const irep_idt & get_identifier() const
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
bool is_integer_address() const
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
exprt deallocated(const exprt &pointer, const namespacet &ns)
const std::string & id_string() const
exprt dead_object(const exprt &pointer, const namespacet &ns)
bool enable_enum_range_check
std::set< exprt > assertionst
exprt simplify_expr(exprt src, const namespacet &ns)
exprt integer_address(const exprt &pointer)
bool has_condition() const
Does this instruction have a condition?
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
pointer_typet pointer_type(const typet &subtype)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
exprt object_size(const exprt &pointer)
bool is_static_lifetime() const
bool check_rec_member(const member_exprt &member, guardt &guard)
Check that a member expression is valid:
const irep_idt & id() const
bool is_end_function() const
const code_function_callt & to_code_function_call(const codet &code)
A goto function, consisting of function type (see type), function body (see body),...
std::vector< exprt > operandst
exprt::operandst argumentst
const code_returnt & to_code_return(const codet &code)
The Boolean constant false.
optionalt< exprt > rw_ok_check(exprt)
expand the r_ok and w_ok predicates
void collect_allocations(const goto_functionst &goto_functions)
Fill the list of allocations allocationst with <address, size> for every allocation instruction.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const exprt & root_object() const
bool is_dynamic_local() const
void from_integer(const mp_integer &i)
void undefined_shift_check(const shift_exprt &, const guardt &)
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
nonstd::optional< T > optionalt
const constant_exprt & size() const
void div_by_zero_check(const div_exprt &, const guardt &)
exprt pointer_offset(const exprt &pointer)
goto_functionst::goto_functiont goto_functiont
error_labelst error_labels
#define Forall_goto_functions(it, functions)
void clear()
Clear the goto program.
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
void set_flag(bool &flag, bool new_value)
Store the current value of flag and then set its value to new_value.
bitvector_typet char_type()
std::size_t get_width() const
A side_effect_exprt that returns a non-deterministically chosen value.
::goto_functiont goto_functiont
exprt malloc_object(const exprt &pointer, const namespacet &ns)
bool is_zero() const
Return whether the expression is a constant representing 0.
bool has_symbol(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
Extract member of struct or union.
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
A collection of goto functions.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
A base class for shift operators.
exprt dynamic_object_upper_bound(const exprt &pointer, const namespacet &ns, const exprt &access_size)
C enum tag type, i.e., c_enum_typet with an identifier.
codet representation of a "return from a function" statement.
goto_functionst goto_functions
GOTO functions.
std::unordered_set< irep_idt > find_symbols_sett
void goto_check(const irep_idt &function_identifier, goto_functiont &goto_function)
void mod_overflow_check(const mod_exprt &, const guardt &)
check a mod expression for the case INT_MIN % -1
const code_assignt & to_code_assign(const codet &code)
Evaluates to true if the operand is infinite.
void invalidate(const exprt &lhs)
Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
enum configt::ansi_ct::c_standardt c_standard
bool get_bool_option(const std::string &option) const
bool enable_signed_overflow_check
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
A base class for relations, i.e., binary predicates whose two operands have the same type.
void add_guarded_property(const exprt &asserted_expr, const std::string &comment, const std::string &property_class, const source_locationt &source_location, const exprt &src_expr, const guardt &guard)
Include the asserted_expr in the code conditioned by the guard.
void integer_overflow_check(const exprt &, const guardt &)
bool is_uninitialized() const
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
exprt same_object(const exprt &p1, const exprt &p2)
A generic container class for the GOTO intermediate representation of one function.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
#define forall_goto_functions(it, functions)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
instructionst::const_iterator const_targett
constant_exprt to_expr() const
optionst::value_listt error_labelst
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Operator to return the address of an object.
source_locationt & add_source_location()
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
exprt dynamic_object_lower_bound(const exprt &pointer, const exprt &offset)
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 ...
bool enable_pointer_overflow_check
const exprt & return_value() const
A codet representing an assignment in the program.
The Boolean constant true.
void check_rec_if(const if_exprt &if_expr, guardt &guard)
Check an if expression: check the if-condition alone, and then check the true/false-cases with the gu...
const irep_idt & get_statement() const
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
A constant literal expression.
IEEE-floating-point equality.
bool is_function_call() const
bool is_boolean() const
Return whether the expression represents a Boolean.
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.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
bool is_target() const
Is this node a branch target?
const irep_idt & get_value() const
const source_locationt & source_location() const
conditiont(const exprt &_assertion, const std::string &_description)
exprt dynamic_size(const namespacet &ns)
symbol_tablet symbol_table
Symbol table.
void check_rec_arithmetic_op(const exprt &expr, guardt &guard)
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers),...
const value_listt & get_list_option(const std::string &option) const
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
goto_checkt(const namespacet &_ns, const optionst &_options)
void conversion_check(const exprt &, const guardt &)
instructionst::iterator targett
#define forall_goto_program_instructions(it, program)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const memberst & members() const
std::list< std::pair< bool *, bool > > flags_to_reset
enum configt::cppt::cpp_standardt cpp_standard