201 const exprt &src_expr,
222 const exprt &address,
225 const exprt &pointer,
229 const exprt &address,
248 const exprt &asserted_expr,
250 const std::string &property_class,
252 const exprt &src_expr,
346 if(rhs.
id() == ID_implies)
350 and_exprt(std::move(lhs), rhs_implication.lhs()), rhs_implication.rhs());
362 for(
const auto &instruction : gf_entry.second.body.instructions)
364 if(!instruction.is_function_call())
367 const auto &function = instruction.call_function();
369 function.id() != ID_symbol ||
375 instruction.call_arguments();
377 args.size() != 2 || args[0].type().id() != ID_unsignedbv ||
378 args[1].type().id() != ID_unsignedbv)
383 args[0].type() == args[1].type(),
384 "arguments of allocated_memory must have same type");
392 if(lhs.
id() == ID_index)
394 else if(lhs.
id() == ID_member)
396 else if(lhs.
id() == ID_symbol)
452 std::vector<exprt> disjuncts;
453 for(
const auto &enum_value : enum_values)
482 if(distance_type.
id() == ID_signedbv)
489 "shift distance is negative",
498 if(op_type.
id() == ID_unsignedbv || op_type.
id() == ID_signedbv)
505 "shift distance too large",
511 if(op_type.
id() == ID_signedbv && expr.
id() == ID_shl)
518 "shift operand is negative",
529 "shift of non-integer type",
566 const auto &type = expr.
type();
568 if(type.id() == ID_signedbv)
582 or_exprt(int_min_neq, minus_one_neq),
583 "result of signed mod is not representable",
599 if(type.
id() != ID_signedbv && type.
id() != ID_unsignedbv)
602 if(expr.
id() == ID_typecast)
607 const typet &old_type = op.type();
609 if(type.
id() == ID_signedbv)
613 if(old_type.
id() == ID_signedbv)
616 if(new_width >= old_width)
626 and_exprt(no_overflow_lower, no_overflow_upper),
627 "arithmetic overflow on signed type conversion",
633 else if(old_type.
id() == ID_unsignedbv)
636 if(new_width >= old_width + 1)
644 "arithmetic overflow on unsigned to signed type conversion",
650 else if(old_type.
id() == ID_floatbv)
664 and_exprt(no_overflow_lower, no_overflow_upper),
665 "arithmetic overflow on float to signed integer type conversion",
672 else if(type.
id() == ID_unsignedbv)
676 if(old_type.
id() == ID_signedbv)
680 if(new_width >= old_width - 1)
688 "arithmetic overflow on signed to unsigned type conversion",
704 and_exprt(no_overflow_lower, no_overflow_upper),
705 "arithmetic overflow on signed to unsigned type conversion",
712 else if(old_type.
id() == ID_unsignedbv)
715 if(new_width >= old_width)
723 "arithmetic overflow on unsigned to unsigned type conversion",
729 else if(old_type.
id() == ID_floatbv)
743 and_exprt(no_overflow_lower, no_overflow_upper),
744 "arithmetic overflow on float to unsigned integer type conversion",
772 if(expr.
id() == ID_div)
775 if(type.
id() == ID_signedbv)
786 "arithmetic overflow on signed division",
795 else if(expr.
id() == ID_unary_minus)
797 if(type.
id() == ID_signedbv)
807 "arithmetic overflow on signed unary minus",
813 else if(type.
id() == ID_unsignedbv)
823 "arithmetic overflow on unsigned unary minus",
832 else if(expr.
id() == ID_shl)
834 if(type.
id() == ID_signedbv)
837 const auto &op = shl_expr.op();
839 const auto op_width = op_type.get_width();
840 const auto &distance = shl_expr.distance();
841 const auto &distance_type = distance.type();
845 exprt neg_value_shift;
847 if(op_type.id() == ID_unsignedbv)
855 exprt neg_dist_shift;
857 if(distance_type.id() == ID_unsignedbv)
868 distance, ID_gt,
from_integer(op_width, distance_type));
873 new_type.set_width(op_width * 2);
884 bool allow_shift_into_sign_bit =
true;
892 allow_shift_into_sign_bit =
false;
895 else if(
mode == ID_cpp)
902 allow_shift_into_sign_bit =
false;
906 const unsigned number_of_top_bits =
907 allow_shift_into_sign_bit ? op_width : op_width + 1;
911 new_type.get_width() - 1,
912 new_type.get_width() - number_of_top_bits,
915 const exprt top_bits_zero =
929 "arithmetic overflow on signed shl",
947 for(std::size_t i = 1; i < expr.
operands().size(); i++)
959 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
963 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
970 else if(expr.
operands().size() == 2)
972 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
977 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
987 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
991 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
1007 if(type.
id() != ID_floatbv)
1012 if(expr.
id() == ID_typecast)
1017 if(op.type().id() == ID_floatbv)
1023 std::move(overflow_check),
1024 "arithmetic overflow on floating-point typecast",
1035 "arithmetic overflow on floating-point typecast",
1044 else if(expr.
id() == ID_div)
1051 std::move(overflow_check),
1052 "arithmetic overflow on floating-point division",
1060 else if(expr.
id() == ID_mod)
1065 else if(expr.
id() == ID_unary_minus)
1070 else if(expr.
id() == ID_plus || expr.
id() == ID_mult || expr.
id() == ID_minus)
1080 std::string kind = expr.
id() == ID_plus
1082 : expr.
id() == ID_minus
1084 : expr.
id() == ID_mult ?
"multiplication" :
"";
1087 std::move(overflow_check),
1088 "arithmetic overflow on floating-point " + kind,
1096 else if(expr.
operands().size() >= 3)
1113 if(expr.
type().
id() != ID_floatbv)
1117 expr.
id() != ID_plus && expr.
id() != ID_mult && expr.
id() != ID_div &&
1118 expr.
id() != ID_minus)
1125 if(expr.
id() == ID_div)
1134 div_expr.op0(),
from_integer(0, div_expr.dividend().type())),
1136 div_expr.op1(),
from_integer(0, div_expr.divisor().type())));
1140 isnan =
or_exprt(zero_div_zero, div_inf);
1142 else if(expr.
id() == ID_mult)
1153 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())));
1157 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())),
1160 isnan =
or_exprt(inf_times_zero, zero_times_inf);
1162 else if(expr.
id() == ID_plus)
1183 else if(expr.
id() == ID_minus)
1232 "same object violation",
1238 for(
const auto &pointer : expr.
operands())
1245 for(
const auto &c : conditions)
1249 "pointer relation: " + c.description,
1250 "pointer arithmetic",
1266 if(expr.
id() != ID_plus && expr.
id() != ID_minus)
1271 "pointer arithmetic expected to have exactly 2 operands");
1277 for(
const auto &c : conditions)
1281 "pointer arithmetic: " + c.description,
1282 "pointer arithmetic",
1291 const exprt &src_expr,
1301 if(expr.
type().
id() == ID_empty)
1313 size = size_of_expr_opt.value();
1318 for(
const auto &c : conditions)
1322 "dereference failure: " + c.description,
1323 "pointer dereference",
1340 const exprt pointer =
1341 (expr.
id() == ID_r_ok || expr.
id() == ID_w_ok || expr.
id() == ID_rw_ok)
1347 if(pointer.
id() == ID_symbol)
1355 const auto size_of_expr_opt =
1358 const exprt size = !size_of_expr_opt.has_value()
1360 : size_of_expr_opt.value();
1364 for(
const auto &c : conditions)
1369 "pointer primitives",
1388 return expr.
id() == ID_object_size || expr.
id() == ID_r_ok ||
1389 expr.
id() == ID_w_ok || expr.
id() == ID_rw_ok ||
1390 expr.
id() == ID_is_dynamic_object;
1395 const exprt &address,
1402 conditions.push_front(*maybe_null_condition);
1424 if(expr.
id() == ID_index)
1427 expr.
id() == ID_count_leading_zeros || expr.
id() == ID_count_trailing_zeros)
1439 if(array_type.
id() == ID_pointer)
1440 throw "index got pointer as array type";
1441 else if(array_type.
id() != ID_array && array_type.
id() != ID_vector)
1442 throw "bounds check expected array or vector type, got " +
1451 if(index.
type().
id() != ID_unsignedbv)
1455 index.
id() == ID_typecast &&
1462 const auto i = numeric_cast<mp_integer>(index);
1464 if(!i.has_value() || *i < 0)
1475 effective_offset, p_offset.
type())};
1482 effective_offset, ID_ge, std::move(zero));
1486 name +
" lower bound",
1510 exprt in_bounds_of_some_explicit_allocation =
1516 std::move(in_bounds_of_some_explicit_allocation), inequality);
1520 name +
" dynamic object upper bound",
1529 const exprt &size = array_type.
id() == ID_array
1538 else if(size.
id() == ID_infinity)
1558 type_size_opt.value());
1562 name +
" upper bound",
1575 name +
" upper bound",
1589 if(expr.
id() == ID_count_leading_zeros)
1591 else if(expr.
id() == ID_count_trailing_zeros)
1598 "count " + name +
" zeros is undefined for value zero",
1606 const exprt &asserted_expr,
1608 const std::string &property_class,
1610 const exprt &src_expr,
1614 exprt simplified_expr =
1622 exprt guarded_expr = guard(simplified_expr);
1624 if(
assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1628 std::move(guarded_expr), source_location)
1630 std::move(guarded_expr), source_location));
1632 std::string source_expr_string;
1635 t->source_location_nonconst().set_comment(
1636 comment +
" in " + source_expr_string);
1637 t->source_location_nonconst().set_property_class(property_class);
1646 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1649 if(expr.
id() == ID_dereference)
1653 else if(expr.
id() == ID_index)
1661 for(
const auto &operand : expr.
operands())
1669 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies);
1672 "'" + expr.
id_string() +
"' must be Boolean, but got " + expr.
pretty());
1676 for(
const auto &op : expr.
operands())
1680 "'" + expr.
id_string() +
"' takes Boolean operands only, but got " +
1683 auto new_guard = [&guard, &constraints](
exprt expr) {
1697 "first argument of if must be boolean, but got " + if_expr.
cond().
pretty());
1702 auto new_guard = [&guard, &if_expr](
exprt expr) {
1709 auto new_guard = [&guard, &if_expr](
exprt expr) {
1733 if(member_offset_opt.has_value())
1762 if(div_expr.
type().
id() == ID_signedbv)
1764 else if(div_expr.
type().
id() == ID_floatbv)
1775 if(expr.
type().
id() == ID_signedbv || expr.
type().
id() == ID_unsignedbv)
1780 expr.
operands().size() == 2 && expr.
id() == ID_minus &&
1781 expr.
operands()[0].type().id() == ID_pointer &&
1782 expr.
operands()[1].type().id() == ID_pointer)
1787 else if(expr.
type().
id() == ID_floatbv)
1792 else if(expr.
type().
id() == ID_pointer)
1800 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1805 auto new_guard = [&guard, &quantifier_expr](
exprt expr) {
1806 return guard(
forall_exprt(quantifier_expr.symbol(), expr));
1809 check_rec(quantifier_expr.where(), new_guard);
1812 else if(expr.
id() == ID_address_of)
1817 else if(expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies)
1822 else if(expr.
id() == ID_if)
1828 expr.
id() == ID_member &&
1838 if(expr.
type().
id() == ID_c_enum_tag)
1841 if(expr.
id() == ID_index)
1845 else if(expr.
id() == ID_div)
1849 else if(expr.
id() == ID_shl || expr.
id() == ID_ashr || expr.
id() == ID_lshr)
1853 if(expr.
id() == ID_shl && expr.
type().
id() == ID_signedbv)
1856 else if(expr.
id() == ID_mod)
1862 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
1863 expr.
id() == ID_unary_minus)
1867 else if(expr.
id() == ID_typecast)
1870 expr.
id() == ID_le || expr.
id() == ID_lt || expr.
id() == ID_ge ||
1873 else if(expr.
id() == ID_dereference)
1882 expr.
id() == ID_count_leading_zeros || expr.
id() == ID_count_trailing_zeros)
1896 bool modified =
false;
1901 if(op_result.has_value())
1908 if(expr.
id() == ID_r_ok || expr.
id() == ID_w_ok || expr.
id() == ID_rw_ok)
1912 expr.
operands().size() == 2,
"r/w_ok must have two operands");
1919 for(
const auto &c : conditions)
1920 conjuncts.push_back(c.assertion);
1928 return std::move(expr);
1962 "Flag " +
id2string(flag_name) +
" set twice at \n" +
1964 if(flag != new_value)
1979 "Flag " +
id2string(flag_name) +
" disabled twice at \n" +
2000 *flag_pair.first = flag_pair.second;
2010 const irep_idt &function_identifier,
2013 const auto &function_symbol =
ns.
lookup(function_identifier);
2014 mode = function_symbol.mode;
2021 bool did_something =
false;
2024 util_make_unique<local_bitvector_analysist>(goto_function,
ns);
2035 for(
const auto &d : pragmas)
2039 if(matched.has_value())
2041 auto named_check = matched.value();
2042 auto name = named_check.first;
2043 auto status = named_check.second;
2047 case check_statust::ENABLE:
2048 resetter.
set_flag(*flag,
true, name);
2050 case check_statust::DISABLE:
2051 resetter.
set_flag(*flag,
false, name);
2053 case check_statust::CHECKED:
2087 t->source_location_nonconst().set_property_class(
"error label");
2088 t->source_location_nonconst().set_comment(
"error label " + label);
2089 t->source_location_nonconst().set(
"user-provided",
true);
2096 const irep_idt &statement = code.get_statement();
2098 if(statement == ID_expression)
2102 else if(statement == ID_printf)
2104 for(
const auto &op : code.operands())
2160 "pointer dereference",
2179 did_something =
true;
2187 did_something =
true;
2205 std::move(address_of_expr),
2214 variable.
type().
id() == ID_pointer &&
2215 function_identifier !=
"alloca" &&
2217 "return_value___builtin_alloca" ||
2219 "return_value_alloca"))
2223 exprt alloca_result =
2227 std::move(alloca_result),
2255 "dynamically allocated memory never freed",
2267 if(instruction.source_location().is_nil())
2269 instruction.source_location_nonconst().id(
irep_idt());
2271 if(!it->source_location().get_file().empty())
2272 instruction.source_location_nonconst().set_file(
2273 it->source_location().get_file());
2275 if(!it->source_location().get_line().empty())
2276 instruction.source_location_nonconst().set_line(
2277 it->source_location().get_line());
2279 if(!it->source_location().get_function().empty())
2280 instruction.source_location_nonconst().set_function(
2281 it->source_location().get_function());
2283 if(!it->source_location().get_column().empty())
2285 instruction.source_location_nonconst().set_column(
2286 it->source_location().get_column());
2308 const exprt &address,
2318 const exprt in_bounds_of_some_explicit_allocation =
2333 in_bounds_of_some_explicit_allocation,
2335 "deallocated dynamic object"));
2342 in_bounds_of_some_explicit_allocation,
2349 const or_exprt object_bounds_violation(
2355 in_bounds_of_some_explicit_allocation,
2357 "pointer outside dynamic object bounds"));
2362 const or_exprt object_bounds_violation(
2368 in_bounds_of_some_explicit_allocation,
2370 "pointer outside object bounds"));
2378 "invalid integer address"));
2386 const exprt &address,
2406 const exprt &pointer,
2420 std::move(upper_bound), ID_le,
plus_exprt{a.first, a.second}};
2422 alloc_disjuncts.push_back(
2423 and_exprt{std::move(lb_check), std::move(ub_check)});
2429 const irep_idt &function_identifier,
2436 goto_check.goto_check(function_identifier, goto_function);
2447 goto_check.collect_allocations(goto_functions);
2451 goto_check.goto_check(gf_entry.first, gf_entry.second);
2483 auto col = s.find(
":");
2485 if(col == std::string::npos)
2488 auto name = s.substr(col + 1);
2494 if(!s.compare(0, 6,
"enable"))
2495 status = check_statust::ENABLE;
2496 else if(!s.compare(0, 7,
"disable"))
2497 status = check_statust::DISABLE;
2498 else if(!s.compare(0, 7,
"checked"))
2499 status = check_statust::CHECKED;
2504 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 shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
signedbv_typet pointer_diff_type()
bitvector_typet char_type()
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
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
C enum tag type, i.e., c_enum_typet with an identifier.
const memberst & members() const
std::vector< c_enum_membert > memberst
exprt::operandst argumentst
const irep_idt & get_statement() const
struct configt::ansi_ct ansi_c
A constant literal expression.
const irep_idt & get_value() const
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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.
bool is_boolean() const
Return whether the expression represents a Boolean.
bool is_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
The Boolean constant false.
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.
flag_resett(const goto_programt::instructiont &_instruction)
void disable_flag(bool &flag, const irep_idt &flag_name)
Sets the given flag to false, overriding any previous value.
std::set< bool * > disabled_flags
std::map< bool *, bool > flags_to_reset
~flag_resett()
Restore the values of all flags that have been modified via set_flag.
const goto_programt::instructiont & instruction
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...
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
exprt is_in_bounds_of_some_explicit_allocation(const exprt &pointer, const exprt &size)
optionalt< exprt > rw_ok_check(exprt)
expand the r_ok, w_ok and rw_ok predicates
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.
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:
optionalt< goto_check_ct::conditiont > get_pointer_is_null_condition(const exprt &address, const exprt &size)
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
void nan_check(const exprt &, const guardt &)
bool enable_built_in_assertions
bool enable_undefined_shift_check
std::list< allocationt > allocationst
bool enable_enum_range_check
goto_programt::const_targett current_target
void div_by_zero_check(const div_exprt &, const guardt &)
optionalt< std::pair< irep_idt, check_statust > > named_check_statust
optional (named-check, status) pair
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)
void add_all_disable_named_check_pragmas(source_locationt &source_location) const
Adds "disable" pragmas for all named checks on the given source location.
bool enable_unsigned_overflow_check
void bounds_check_bit_count(const unary_exprt &, const guardt &)
bool enable_div_by_zero_check
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.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
bool is_end_function() const
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
bool is_target() const
Is this node a branch target?
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
bool is_set_return_value() const
const codet & get_code() const
Get the code represented by this instruction.
bool has_condition() const
Does this instruction have a condition?
const codet & get_other() const
Get the statement for OTHER.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
bool is_function_call() const
source_locationt & source_location_nonconst()
const source_locationt & source_location() const
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::iterator targett
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 irept & find(const irep_idt &name) const
const std::string & id_string() const
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)).
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
A base class for shift and rotate operators.
A side_effect_exprt that returns a non-deterministically chosen value.
void add_pragma(const irep_idt &pragma)
const irep_idt & get_property_class() const
const irept::named_subt & get_pragmas() const
static bool is_built_in(const std::string &s)
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.
const irep_idt & get_identifier() const
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 operation kind would result in an overflow when applied to t...
Fixed-width bit-vector with unsigned binary interpretation.
const constant_exprt & size() const
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
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(const exprt &src, const find_symbols_sett &symbols, bool current, bool next)
std::unordered_set< irep_idt > find_symbols_sett
API to expression classes for floating-point arithmetic.
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
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.
nonstd::optional< T > optionalt
API to expression classes for Pointers.
const r_or_w_ok_exprt & to_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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
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 null_pointer(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
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#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 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 mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_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 unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_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