200 const exprt &src_expr,
218 std::optional<goto_check_ct::conditiont>
221 const exprt &address,
224 const exprt &pointer,
228 const exprt &address,
246 const exprt &asserted_expr,
248 const std::string &property_class,
250 const exprt &src_expr,
371 "Flag " +
id2string(flag_name) +
" set twice at \n" +
373 if(flag != new_value)
388 "Flag " +
id2string(flag_name) +
" disabled twice at \n" +
409 *flag_pair.first = flag_pair.second;
421 if(rhs.
id() == ID_implies)
425 and_exprt(std::move(lhs), rhs_implication.lhs()), rhs_implication.rhs());
437 for(
const auto &instruction : gf_entry.second.body.instructions)
439 if(!instruction.is_function_call())
442 const auto &
function = instruction.call_function();
444 function.
id() != ID_symbol ||
450 instruction.call_arguments();
452 args.size() != 2 || args[0].type().id() != ID_unsignedbv ||
453 args[1].type().id() != ID_unsignedbv)
458 args[0].type() == args[1].type(),
459 "arguments of allocated_memory must have same type");
467 if(lhs.
id() == ID_index)
469 else if(lhs.
id() == ID_member)
471 else if(lhs.
id() == ID_symbol)
530 "floating-point division by zero",
531 "float-division-by-zero",
544 for(
const auto &d : pragmas)
546 if(d.first ==
"disable:enum-range-check")
573 if(distance_type.
id() == ID_signedbv)
580 "shift distance is negative",
589 if(op_type.
id() == ID_unsignedbv || op_type.
id() == ID_signedbv)
596 "shift distance too large",
602 if(op_type.
id() == ID_signedbv && expr.
id() == ID_shl)
609 "shift operand is negative",
620 "shift of non-integer type",
657 const auto &type = expr.
type();
659 if(type.id() == ID_signedbv)
673 or_exprt(int_min_neq, minus_one_neq),
674 "result of signed mod is not representable",
690 if(type.
id() != ID_signedbv && type.
id() != ID_unsignedbv)
693 if(expr.
id() == ID_typecast)
698 const typet &old_type = op.type();
700 if(type.
id() == ID_signedbv)
704 if(old_type.
id() == ID_signedbv)
707 if(new_width >= old_width)
717 and_exprt(no_overflow_lower, no_overflow_upper),
718 "arithmetic overflow on signed type conversion",
724 else if(old_type.
id() == ID_unsignedbv)
727 if(new_width >= old_width + 1)
735 "arithmetic overflow on unsigned to signed type conversion",
741 else if(old_type.
id() == ID_floatbv)
755 and_exprt(no_overflow_lower, no_overflow_upper),
756 "arithmetic overflow on float to signed integer type conversion",
763 else if(type.
id() == ID_unsignedbv)
767 if(old_type.
id() == ID_signedbv)
771 if(new_width >= old_width - 1)
779 "arithmetic overflow on signed to unsigned type conversion",
795 and_exprt(no_overflow_lower, no_overflow_upper),
796 "arithmetic overflow on signed to unsigned type conversion",
803 else if(old_type.
id() == ID_unsignedbv)
806 if(new_width >= old_width)
814 "arithmetic overflow on unsigned to unsigned type conversion",
820 else if(old_type.
id() == ID_floatbv)
834 and_exprt(no_overflow_lower, no_overflow_upper),
835 "arithmetic overflow on float to unsigned integer type conversion",
863 if(expr.
id() == ID_div)
866 if(type.
id() == ID_signedbv)
877 "arithmetic overflow on signed division",
886 else if(expr.
id() == ID_unary_minus)
888 if(type.
id() == ID_signedbv)
898 "arithmetic overflow on signed unary minus",
904 else if(type.
id() == ID_unsignedbv)
914 "arithmetic overflow on unsigned unary minus",
923 else if(expr.
id() == ID_shl)
925 if(type.
id() == ID_signedbv)
928 const auto &op = shl_expr.op();
930 const auto op_width = op_type.get_width();
931 const auto &distance = shl_expr.distance();
932 const auto &distance_type = distance.type();
936 exprt neg_value_shift;
938 if(op_type.id() == ID_unsignedbv)
946 exprt neg_dist_shift;
948 if(distance_type.id() == ID_unsignedbv)
959 distance, ID_gt,
from_integer(op_width, distance_type));
964 new_type.set_width(op_width * 2);
975 bool allow_shift_into_sign_bit =
true;
983 allow_shift_into_sign_bit =
false;
986 else if(
mode == ID_cpp)
993 allow_shift_into_sign_bit =
false;
997 const unsigned number_of_top_bits =
998 allow_shift_into_sign_bit ? op_width : op_width + 1;
1002 new_type.get_width() - 1,
1003 new_type.get_width() - number_of_top_bits,
1006 const exprt top_bits_zero =
1021 "arithmetic overflow on signed shl",
1039 for(std::size_t i = 1; i < expr.
operands().size(); i++)
1051 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
1055 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
1062 else if(expr.
operands().size() == 2)
1064 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
1069 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
1079 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
1083 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
1099 if(type.
id() != ID_floatbv)
1104 if(expr.
id() == ID_typecast)
1109 if(op.type().id() == ID_floatbv)
1115 std::move(overflow_check),
1116 "arithmetic overflow on floating-point typecast",
1127 "arithmetic overflow on floating-point typecast",
1136 else if(expr.
id() == ID_div)
1143 std::move(overflow_check),
1144 "arithmetic overflow on floating-point division",
1152 else if(expr.
id() == ID_mod)
1157 else if(expr.
id() == ID_unary_minus)
1162 else if(expr.
id() == ID_plus || expr.
id() == ID_mult || expr.
id() == ID_minus)
1172 std::string kind = expr.
id() == ID_plus
1174 : expr.
id() == ID_minus
1176 : expr.
id() == ID_mult ?
"multiplication" :
"";
1179 std::move(overflow_check),
1180 "arithmetic overflow on floating-point " + kind,
1188 else if(expr.
operands().size() >= 3)
1205 if(expr.
type().
id() != ID_floatbv)
1209 expr.
id() != ID_plus && expr.
id() != ID_mult && expr.
id() != ID_div &&
1210 expr.
id() != ID_minus)
1217 if(expr.
id() == ID_div)
1226 div_expr.op0(),
from_integer(0, div_expr.dividend().type())),
1228 div_expr.op1(),
from_integer(0, div_expr.divisor().type())));
1234 else if(expr.
id() == ID_mult)
1245 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())));
1249 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())),
1254 else if(expr.
id() == ID_plus)
1275 else if(expr.
id() == ID_minus)
1324 "same object violation",
1330 for(
const auto &pointer : expr.
operands())
1337 for(
const auto &c : conditions)
1341 "pointer relation: " + c.description,
1342 "pointer arithmetic",
1358 if(expr.
id() != ID_plus && expr.
id() != ID_minus)
1363 "pointer arithmetic expected to have exactly 2 operands");
1368 if(object_type.
id() != ID_empty)
1375 exprt offset_operand = binary_expr.
lhs().
type().
id() == ID_pointer
1377 : binary_expr.
lhs();
1395 for(
const auto &c : conditions)
1399 "pointer arithmetic: " + c.description,
1400 "pointer arithmetic",
1409 const exprt &src_expr,
1419 if(expr.
type().
id() == ID_empty)
1431 size = size_of_expr_opt.value();
1436 for(
const auto &c : conditions)
1440 "dereference failure: " + c.description,
1441 "pointer dereference",
1458 const exprt pointer =
1459 (expr.
id() == ID_r_ok || expr.
id() == ID_w_ok || expr.
id() == ID_rw_ok)
1467 if(pointer.
id() == ID_symbol)
1477 for(
const auto &c : conditions)
1482 "pointer primitives",
1502 expr.
id() == ID_w_ok || expr.
id() == ID_rw_ok ||
1504 expr.
id() == ID_is_dynamic_object;
1509 const exprt &address,
1516 conditions.push_front(*maybe_null_condition);
1531 if(expr.
id() == ID_index)
1534 (expr.
id() == ID_count_leading_zeros &&
1536 (expr.
id() == ID_count_trailing_zeros &&
1549 if(array_type.
id() == ID_pointer)
1550 throw "index got pointer as array type";
1551 else if(array_type.
id() != ID_array && array_type.
id() != ID_vector)
1552 throw "bounds check expected array or vector type, got " +
1561 if(index.
type().
id() != ID_unsignedbv)
1565 index.
id() == ID_typecast &&
1572 const auto i = numeric_cast<mp_integer>(index);
1574 if(!i.has_value() || *i < 0)
1586 effective_offset, p_offset.
type())};
1593 effective_offset, ID_ge, std::move(zero));
1597 name +
" lower bound",
1621 exprt in_bounds_of_some_explicit_allocation =
1627 std::move(in_bounds_of_some_explicit_allocation), inequality);
1631 name +
" dynamic object upper bound",
1640 const exprt &size = array_type.
id() == ID_array
1644 if(size.
is_nil() && !array_type.
get_bool(ID_C_flexible_array_member))
1649 else if(size.
id() == ID_infinity)
1653 expr.
array().
id() == ID_member &&
1664 const auto type_size_opt =
1675 name +
" upper bound",
1688 name +
" upper bound",
1702 if(expr.
id() == ID_count_leading_zeros)
1704 else if(expr.
id() == ID_count_trailing_zeros)
1711 "count " + name +
" zeros is undefined for value zero",
1719 const exprt &asserted_expr,
1721 const std::string &property_class,
1723 const exprt &src_expr,
1727 exprt simplified_expr =
1737 if(
assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1739 std::string source_expr_string;
1751 std::move(guarded_expr), annotated_location));
1756 std::move(guarded_expr), annotated_location));
1764 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1767 if(expr.
id() == ID_dereference)
1771 else if(expr.
id() == ID_index)
1779 for(
const auto &operand : expr.
operands())
1787 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies);
1790 "'" + expr.
id_string() +
"' must be Boolean, but got " + expr.
pretty());
1794 for(
const auto &op : expr.
operands())
1798 "'" + expr.
id_string() +
"' takes Boolean operands only, but got " +
1801 auto new_guard = [&
guard, &constraints](
exprt expr) {
1815 "first argument of if must be boolean, but got " + if_expr.
cond().
pretty());
1820 auto new_guard = [&
guard, &if_expr](
exprt expr) {
1827 auto new_guard = [&
guard, &if_expr](
exprt expr) {
1851 if(member_offset_opt.has_value())
1880 div_expr.
type().
id() == ID_signedbv ||
1881 div_expr.
type().
id() == ID_unsignedbv || div_expr.
type().
id() == ID_c_bool)
1886 else if(div_expr.
type().
id() == ID_floatbv)
1895 if(div_expr.
type().
id() == ID_signedbv)
1897 else if(div_expr.
type().
id() == ID_floatbv)
1908 if(expr.
type().
id() == ID_signedbv || expr.
type().
id() == ID_unsignedbv)
1913 expr.
operands().size() == 2 && expr.
id() == ID_minus &&
1914 expr.
operands()[0].type().id() == ID_pointer &&
1915 expr.
operands()[1].type().id() == ID_pointer)
1920 else if(expr.
type().
id() == ID_floatbv)
1925 else if(expr.
type().
id() == ID_pointer)
1933 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1938 auto new_guard = [&
guard, &quantifier_expr](
exprt expr) {
1942 check_rec(quantifier_expr.where(), new_guard);
1945 else if(expr.
id() == ID_address_of)
1950 else if(expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies)
1955 else if(expr.
id() == ID_if)
1961 expr.
id() == ID_member &&
1968 for(
const auto &op : expr.
operands())
1971 if(expr.
type().
id() == ID_c_enum_tag)
1974 if(expr.
id() == ID_index)
1978 else if(expr.
id() == ID_div)
1982 else if(expr.
id() == ID_shl || expr.
id() == ID_ashr || expr.
id() == ID_lshr)
1986 if(expr.
id() == ID_shl && expr.
type().
id() == ID_signedbv)
1989 else if(expr.
id() == ID_mod)
1995 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
1996 expr.
id() == ID_unary_minus)
2000 else if(expr.
id() == ID_typecast)
2003 expr.
id() == ID_le || expr.
id() == ID_lt || expr.
id() == ID_ge ||
2006 else if(expr.
id() == ID_dereference)
2015 expr.
id() == ID_count_leading_zeros || expr.
id() == ID_count_trailing_zeros)
2041 "dynamically allocated memory never freed",
2049 const irep_idt &function_identifier,
2052 const auto &function_symbol =
ns.
lookup(function_identifier);
2053 mode = function_symbol.mode;
2060 bool did_something =
false;
2063 std::make_unique<local_bitvector_analysist>(goto_function,
ns);
2074 for(
const auto &d : pragmas)
2078 if(matched.has_value())
2080 auto named_check = matched.value();
2081 auto name = named_check.first;
2082 auto status = named_check.second;
2086 case check_statust::ENABLE:
2087 resetter.
set_flag(*flag,
true, name);
2089 case check_statust::DISABLE:
2090 resetter.
set_flag(*flag,
false, name);
2092 case check_statust::CHECKED:
2122 annotated_location.
set_comment(
"error label " + label);
2123 annotated_location.
set(
"user-provided",
true);
2141 const irep_idt &statement = code.get_statement();
2143 if(statement == ID_expression)
2147 else if(statement == ID_printf)
2149 for(
const auto &op : code.operands())
2207 (function_identifier ==
"abort" || function_identifier ==
"exit" ||
2208 function_identifier ==
"_Exit" ||
2209 (i.
labels.size() == 1 && i.
labels.front() ==
"__VERIFIER_abort")))
2229 std::move(address_of_expr),
2249 if(instruction.source_location().is_nil())
2251 instruction.source_location_nonconst().id(
irep_idt());
2253 if(!it->source_location().get_file().empty())
2254 instruction.source_location_nonconst().set_file(
2255 it->source_location().get_file());
2257 if(!it->source_location().get_line().empty())
2258 instruction.source_location_nonconst().set_line(
2259 it->source_location().get_line());
2261 if(!it->source_location().get_function().empty())
2262 instruction.source_location_nonconst().set_function(
2263 it->source_location().get_function());
2265 if(!it->source_location().get_column().empty())
2267 instruction.source_location_nonconst().set_column(
2268 it->source_location().get_column());
2309 const exprt &address,
2319 const exprt in_bounds_of_some_explicit_allocation =
2334 in_bounds_of_some_explicit_allocation,
2336 "deallocated dynamic object"));
2343 in_bounds_of_some_explicit_allocation,
2350 const or_exprt object_bounds_violation(
2356 in_bounds_of_some_explicit_allocation,
2358 "pointer outside dynamic object bounds"));
2363 const or_exprt object_bounds_violation(
2369 in_bounds_of_some_explicit_allocation,
2371 "pointer outside object bounds"));
2379 "invalid integer address"));
2385 std::optional<goto_check_ct::conditiont>
2387 const exprt &address,
2408 const exprt &pointer,
2422 std::move(upper_bound), ID_le,
plus_exprt{a.first, a.second}};
2424 alloc_disjuncts.push_back(
2425 and_exprt{std::move(lb_check), std::move(ub_check)});
2431 const irep_idt &function_identifier,
2438 goto_check.
goto_check(function_identifier, goto_function);
2453 goto_check.
goto_check(gf_entry.first, gf_entry.second);
2485 auto col = s.find(
":");
2487 if(col == std::string::npos)
2490 auto name = s.substr(col + 1);
2496 if(!s.compare(0, 6,
"enable"))
2497 status = check_statust::ENABLE;
2498 else if(!s.compare(0, 7,
"disable"))
2499 status = check_statust::DISABLE;
2500 else if(!s.compare(0, 7,
"checked"))
2501 status = check_statust::CHECKED;
2506 return std::pair<irep_idt, check_statust>{name, status};
std::string array_name(const namespacet &ns, const exprt &expr)
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
API to expression classes that are internal to the C frontend.
static exprt guard(const exprt::operandst &guards, exprt cond)
pointer_typet pointer_type(const typet &subtype)
signedbv_typet pointer_diff_type()
bitvector_typet char_type()
Operator to return the address of an object.
const exprt & size() const
A base class for binary expressions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
A base class for relations, i.e., binary predicates whose two operands have the same type.
std::size_t get_width() const
A goto_instruction_codet representing an assignment in the program.
exprt::operandst argumentst
struct configt::ansi_ct ansi_c
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's d...
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
source_locationt & add_source_location()
bool is_boolean() const
Return whether the expression represents a Boolean.
const source_locationt & source_location() const
bool is_false() const
Return whether the expression is a constant representing false.
bool is_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
The Boolean constant false.
~flag_overridet()
Restore the values of all flags that have been modified via set_flag.
void disable_flag(bool &flag, const irep_idt &flag_name)
Sets the given flag to false, overriding any previous value.
void set_flag(bool &flag, bool new_value, const irep_idt &flag_name)
Store the current value of flag and then set its value to new_value.
std::map< bool *, bool > flags_to_reset
flag_overridet(const source_locationt &source_location)
std::set< bool * > disabled_flags
const source_locationt & source_location
std::optional< std::pair< irep_idt, check_statust > > named_check_statust
optional (named-check, status) pair
named_check_statust match_named_check(const irep_idt &named_check) const
Matches a named-check string of the form.
void goto_check(const irep_idt &function_identifier, goto_functiont &goto_function)
void check_rec(const exprt &expr, const guardt &guard)
Recursively descend into expr and run the appropriate check for each sub-expression,...
void check_rec_logical_op(const exprt &expr, const guardt &guard)
Check a logical operation: check each operand in separation while extending the guarding condition as...
bool enable_float_div_by_zero_check
void check_rec_address(const exprt &expr, const guardt &guard)
Check an address-of expression: if it is a dereference then check the pointer if it is an index then ...
std::function< exprt(exprt)> guardt
std::string array_name(const exprt &)
void collect_allocations(const goto_functionst &goto_functions)
Fill the list of allocations allocationst with <address, size> for every allocation instruction.
bool enable_pointer_check
void memory_leak_check(const irep_idt &function_id)
exprt is_in_bounds_of_some_explicit_allocation(const exprt &pointer, const exprt &size)
std::optional< goto_check_ct::conditiont > get_pointer_is_null_condition(const exprt &address, const exprt &size)
void enum_range_check(const exprt &, const guardt &)
void invalidate(const exprt &lhs)
Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.
void float_div_by_zero_check(const div_exprt &, const guardt &)
check_statust
activation statuses for named checks
void float_overflow_check(const exprt &, const guardt &)
bool enable_pointer_primitive_check
void mod_overflow_check(const mod_exprt &, const guardt &)
check a mod expression for the case INT_MIN % -1
bool requires_pointer_primitive_check(const exprt &expr)
Returns true if the given expression is a pointer primitive that requires validation of the operand t...
std::map< irep_idt, bool * > name_to_flag
Maps a named-check name to the corresponding boolean flag.
std::list< conditiont > conditionst
bool enable_float_overflow_check
bool enable_conversion_check
void check_rec_div(const div_exprt &div_expr, const guardt &guard)
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numb...
bool enable_pointer_overflow_check
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.
void bounds_check_index(const index_exprt &, const guardt &)
bool enable_signed_overflow_check
void check(const exprt &expr)
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
conditionst get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size)
bool check_rec_member(const member_exprt &member, const guardt &guard)
Check that a member expression is valid:
goto_functionst::goto_functiont goto_functiont
void bounds_check(const exprt &, const guardt &)
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.
std::pair< exprt, exprt > allocationt
void pointer_overflow_check(const exprt &, const guardt &)
bool enable_memory_leak_check
void conversion_check(const exprt &, const guardt &)
void check_rec_if(const if_exprt &if_expr, const guardt &guard)
Check an if expression: check the if-condition alone, and then check the true/false-cases with the gu...
void integer_overflow_check(const exprt &, const guardt &)
bool enable_assert_to_assume
bool enable_memory_cleanup_check
void nan_check(const exprt &, const guardt &)
bool enable_undefined_shift_check
std::list< allocationt > allocationst
bool enable_enum_range_check
goto_programt::const_targett current_target
void add_all_checked_named_check_pragmas(source_locationt &source_location) const
Adds "checked" pragmas for all named checks on the given source location (prevents any the instanciat...
void div_by_zero_check(const div_exprt &, const guardt &)
optionst::value_listt error_labelst
void add_active_named_check_pragmas(source_locationt &source_location) const
Adds "checked" pragmas for all currently active named checks on the given source location.
void pointer_rel_check(const binary_exprt &, const guardt &)
goto_check_ct(const namespacet &_ns, const optionst &_options, message_handlert &_message_handler)
conditionst get_pointer_points_to_valid_memory_conditions(const exprt &address, const exprt &size)
bool enable_unsigned_overflow_check
void bounds_check_bit_count(const unary_exprt &, const guardt &)
bool enable_div_by_zero_check
void check_shadow_memory_api_calls(const goto_programt::instructiont &)
error_labelst error_labels
void check_rec_arithmetic_op(const exprt &expr, const guardt &guard)
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers),...
void undefined_shift_check(const shift_exprt &, const guardt &)
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
void mod_by_zero_check(const mod_exprt &, const guardt &)
std::set< std::pair< exprt, exprt > > assertionst
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.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
bool is_end_function() const
const exprt & condition() const
Get the condition of gotos, assume, assert.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
bool is_target() const
Is this node a branch target?
bool is_set_return_value() const
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
bool has_condition() const
Does this instruction have a condition?
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
source_locationt & source_location_nonconst()
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const source_locationt & source_location() const
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
bool is_function_call() const
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void clear()
Clear the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::const_iterator const_targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
IEEE-floating-point equality.
constant_exprt to_expr() const
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
void from_integer(const mp_integer &i)
The trinary if-then-else operator.
bool get_bool(const irep_idt &name) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const std::string & id_string() const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
Evaluates to true if the operand is infinite.
Extract member of struct or union.
const exprt & struct_op() const
Class that provides messages with a built-in verbosity 'level'.
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Binary multiplication Associativity is not specified.
A base class for multi-ary expressions Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
Split an expression into a base object and a (byte) offset.
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...
static const exprt & root_object(const exprt &expr)
bool get_bool_option(const std::string &option) const
const value_listt & get_list_option(const std::string &option) const
std::list< std::string > value_listt
The plus expression Associativity is not specified.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
const exprt & pointer() const
const exprt & pointer() const
A base class for shift and rotate operators.
A side_effect_exprt that returns a non-deterministically chosen value.
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
const irept::named_subt & get_pragmas() const
void add_pragma(const irep_idt &pragma)
static bool is_built_in(const std::string &s)
std::string as_string() const
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Generic base class for unary expressions.
A Boolean expression returning true, iff negation would result in an overflow when applied to the (si...
Fixed-width bit-vector with unsigned binary interpretation.
const constant_exprt & size() const
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
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 boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
bool has_symbol_expr(const exprt &src, const irep_idt &identifier, bool include_bound_symbols)
Returns true if one of the symbol expressions in src has identifier identifier; if include_bound_symb...
API to expression classes for floating-point arithmetic.
void goto_check_c(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
static exprt implication(exprt lhs, exprt rhs)
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Abstract interface to support a programming language.
Field-insensitive, location-sensitive bitvector analysis.
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
API to expression classes for Pointers.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool can_cast_expr< object_size_exprt >(const exprt &base)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const prophecy_r_or_w_ok_exprt & to_prophecy_r_or_w_ok_expr(const exprt &expr)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
bool can_cast_expr< prophecy_r_or_w_ok_exprt >(const exprt &base)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
exprt pointer_offset(const exprt &pointer)
exprt integer_address(const exprt &pointer)
exprt deallocated(const exprt &pointer, const namespacet &ns)
exprt object_size(const exprt &pointer)
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
exprt dead_object(const exprt &pointer, const namespacet &ns)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_object(const exprt &pointer)
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
enum configt::ansi_ct::c_standardt c_standard
enum configt::cppt::cpp_standardt cpp_standard
conditiont(const exprt &_assertion, const std::string &_description)
bool is_static_lifetime() const
bool is_dynamic_local() const
bool is_dynamic_heap() const
bool is_uninitialized() const
bool is_integer_address() const