199 const exprt &src_expr,
220 const exprt &address,
223 const exprt &pointer,
227 const exprt &address,
245 const exprt &asserted_expr,
247 const std::string &property_class,
249 const exprt &src_expr,
368 "Flag " +
id2string(flag_name) +
" set twice at \n" +
370 if(flag != new_value)
385 "Flag " +
id2string(flag_name) +
" disabled twice at \n" +
406 *flag_pair.first = flag_pair.second;
418 if(rhs.
id() == ID_implies)
422 and_exprt(std::move(lhs), rhs_implication.lhs()), rhs_implication.rhs());
434 for(
const auto &instruction : gf_entry.second.body.instructions)
436 if(!instruction.is_function_call())
439 const auto &function = instruction.call_function();
441 function.id() != ID_symbol ||
447 instruction.call_arguments();
449 args.size() != 2 || args[0].type().id() != ID_unsignedbv ||
450 args[1].type().id() != ID_unsignedbv)
455 args[0].type() == args[1].type(),
456 "arguments of allocated_memory must have same type");
464 if(lhs.
id() == ID_index)
466 else if(lhs.
id() == ID_member)
468 else if(lhs.
id() == ID_symbol)
520 for(
const auto &d : pragmas)
522 if(d.first ==
"disable:enum-range-check")
549 if(distance_type.
id() == ID_signedbv)
556 "shift distance is negative",
565 if(op_type.
id() == ID_unsignedbv || op_type.
id() == ID_signedbv)
572 "shift distance too large",
578 if(op_type.
id() == ID_signedbv && expr.
id() == ID_shl)
585 "shift operand is negative",
596 "shift of non-integer type",
633 const auto &type = expr.
type();
635 if(type.id() == ID_signedbv)
649 or_exprt(int_min_neq, minus_one_neq),
650 "result of signed mod is not representable",
666 if(type.
id() != ID_signedbv && type.
id() != ID_unsignedbv)
669 if(expr.
id() == ID_typecast)
674 const typet &old_type = op.type();
676 if(type.
id() == ID_signedbv)
680 if(old_type.
id() == ID_signedbv)
683 if(new_width >= old_width)
693 and_exprt(no_overflow_lower, no_overflow_upper),
694 "arithmetic overflow on signed type conversion",
700 else if(old_type.
id() == ID_unsignedbv)
703 if(new_width >= old_width + 1)
711 "arithmetic overflow on unsigned to signed type conversion",
717 else if(old_type.
id() == ID_floatbv)
731 and_exprt(no_overflow_lower, no_overflow_upper),
732 "arithmetic overflow on float to signed integer type conversion",
739 else if(type.
id() == ID_unsignedbv)
743 if(old_type.
id() == ID_signedbv)
747 if(new_width >= old_width - 1)
755 "arithmetic overflow on signed to unsigned type conversion",
771 and_exprt(no_overflow_lower, no_overflow_upper),
772 "arithmetic overflow on signed to unsigned type conversion",
779 else if(old_type.
id() == ID_unsignedbv)
782 if(new_width >= old_width)
790 "arithmetic overflow on unsigned to unsigned type conversion",
796 else if(old_type.
id() == ID_floatbv)
810 and_exprt(no_overflow_lower, no_overflow_upper),
811 "arithmetic overflow on float to unsigned integer type conversion",
839 if(expr.
id() == ID_div)
842 if(type.
id() == ID_signedbv)
853 "arithmetic overflow on signed division",
862 else if(expr.
id() == ID_unary_minus)
864 if(type.
id() == ID_signedbv)
874 "arithmetic overflow on signed unary minus",
880 else if(type.
id() == ID_unsignedbv)
890 "arithmetic overflow on unsigned unary minus",
899 else if(expr.
id() == ID_shl)
901 if(type.
id() == ID_signedbv)
904 const auto &op = shl_expr.op();
906 const auto op_width = op_type.get_width();
907 const auto &distance = shl_expr.distance();
908 const auto &distance_type = distance.type();
912 exprt neg_value_shift;
914 if(op_type.id() == ID_unsignedbv)
922 exprt neg_dist_shift;
924 if(distance_type.id() == ID_unsignedbv)
935 distance, ID_gt,
from_integer(op_width, distance_type));
940 new_type.set_width(op_width * 2);
951 bool allow_shift_into_sign_bit =
true;
959 allow_shift_into_sign_bit =
false;
962 else if(
mode == ID_cpp)
969 allow_shift_into_sign_bit =
false;
973 const unsigned number_of_top_bits =
974 allow_shift_into_sign_bit ? op_width : op_width + 1;
978 new_type.get_width() - 1,
979 new_type.get_width() - number_of_top_bits,
982 const exprt top_bits_zero =
997 "arithmetic overflow on signed shl",
1015 for(std::size_t i = 1; i < expr.
operands().size(); i++)
1027 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
1031 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
1038 else if(expr.
operands().size() == 2)
1040 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
1045 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
1055 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
1059 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
1075 if(type.
id() != ID_floatbv)
1080 if(expr.
id() == ID_typecast)
1085 if(op.type().id() == ID_floatbv)
1091 std::move(overflow_check),
1092 "arithmetic overflow on floating-point typecast",
1103 "arithmetic overflow on floating-point typecast",
1112 else if(expr.
id() == ID_div)
1119 std::move(overflow_check),
1120 "arithmetic overflow on floating-point division",
1128 else if(expr.
id() == ID_mod)
1133 else if(expr.
id() == ID_unary_minus)
1138 else if(expr.
id() == ID_plus || expr.
id() == ID_mult || expr.
id() == ID_minus)
1148 std::string kind = expr.
id() == ID_plus
1150 : expr.
id() == ID_minus
1152 : expr.
id() == ID_mult ?
"multiplication" :
"";
1155 std::move(overflow_check),
1156 "arithmetic overflow on floating-point " + kind,
1164 else if(expr.
operands().size() >= 3)
1181 if(expr.
type().
id() != ID_floatbv)
1185 expr.
id() != ID_plus && expr.
id() != ID_mult && expr.
id() != ID_div &&
1186 expr.
id() != ID_minus)
1193 if(expr.
id() == ID_div)
1202 div_expr.op0(),
from_integer(0, div_expr.dividend().type())),
1204 div_expr.op1(),
from_integer(0, div_expr.divisor().type())));
1208 isnan =
or_exprt(zero_div_zero, div_inf);
1210 else if(expr.
id() == ID_mult)
1221 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())));
1225 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())),
1228 isnan =
or_exprt(inf_times_zero, zero_times_inf);
1230 else if(expr.
id() == ID_plus)
1251 else if(expr.
id() == ID_minus)
1300 "same object violation",
1306 for(
const auto &pointer : expr.
operands())
1313 for(
const auto &c : conditions)
1317 "pointer relation: " + c.description,
1318 "pointer arithmetic",
1334 if(expr.
id() != ID_plus && expr.
id() != ID_minus)
1339 "pointer arithmetic expected to have exactly 2 operands");
1344 if(object_type.
id() != ID_empty)
1351 exprt offset_operand = binary_expr.
lhs().
type().
id() == ID_pointer
1353 : binary_expr.
lhs();
1371 for(
const auto &c : conditions)
1375 "pointer arithmetic: " + c.description,
1376 "pointer arithmetic",
1385 const exprt &src_expr,
1395 if(expr.
type().
id() == ID_empty)
1407 size = size_of_expr_opt.value();
1412 for(
const auto &c : conditions)
1416 "dereference failure: " + c.description,
1417 "pointer dereference",
1434 const exprt pointer =
1435 (expr.
id() == ID_r_ok || expr.
id() == ID_w_ok || expr.
id() == ID_rw_ok)
1443 if(pointer.
id() == ID_symbol)
1453 for(
const auto &c : conditions)
1458 "pointer primitives",
1478 expr.
id() == ID_w_ok || expr.
id() == ID_rw_ok ||
1480 expr.
id() == ID_is_dynamic_object;
1485 const exprt &address,
1492 conditions.push_front(*maybe_null_condition);
1499 return ::array_name(
ns, expr);
1507 if(expr.
id() == ID_index)
1510 (expr.
id() == ID_count_leading_zeros &&
1512 (expr.
id() == ID_count_trailing_zeros &&
1525 if(array_type.
id() == ID_pointer)
1526 throw "index got pointer as array type";
1527 else if(array_type.
id() != ID_array && array_type.
id() != ID_vector)
1528 throw "bounds check expected array or vector type, got " +
1537 if(index.
type().
id() != ID_unsignedbv)
1541 index.
id() == ID_typecast &&
1550 if(!i.has_value() || *i < 0)
1562 effective_offset, p_offset.
type())};
1569 effective_offset, ID_ge, std::move(zero));
1573 name +
" lower bound",
1597 exprt in_bounds_of_some_explicit_allocation =
1603 std::move(in_bounds_of_some_explicit_allocation), inequality);
1607 name +
" dynamic object upper bound",
1616 const exprt &size = array_type.
id() == ID_array
1620 if(size.
is_nil() && !array_type.
get_bool(ID_C_flexible_array_member))
1625 else if(size.
id() == ID_infinity)
1629 expr.
array().
id() == ID_member &&
1640 const auto type_size_opt =
1651 name +
" upper bound",
1664 name +
" upper bound",
1678 if(expr.
id() == ID_count_leading_zeros)
1680 else if(expr.
id() == ID_count_trailing_zeros)
1687 "count " + name +
" zeros is undefined for value zero",
1695 const exprt &asserted_expr,
1697 const std::string &property_class,
1699 const exprt &src_expr,
1703 exprt simplified_expr =
1713 if(
assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1715 std::string source_expr_string;
1727 std::move(guarded_expr), annotated_location));
1732 std::move(guarded_expr), annotated_location));
1740 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1743 if(expr.
id() == ID_dereference)
1747 else if(expr.
id() == ID_index)
1755 for(
const auto &operand : expr.
operands())
1763 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies);
1766 "'" + expr.
id_string() +
"' must be Boolean, but got " + expr.
pretty());
1770 for(
const auto &op : expr.
operands())
1774 "'" + expr.
id_string() +
"' takes Boolean operands only, but got " +
1777 auto new_guard = [&
guard, &constraints](
exprt expr) {
1781 check_rec(op, new_guard);
1791 "first argument of if must be boolean, but got " + if_expr.
cond().
pretty());
1796 auto new_guard = [&
guard, &if_expr](
exprt expr) {
1799 check_rec(if_expr.
true_case(), new_guard);
1803 auto new_guard = [&
guard, &if_expr](
exprt expr) {
1810bool goto_check_ct::check_rec_member(
1827 if(member_offset_opt.has_value())
1851void goto_check_ct::check_rec_div(
1857 if(div_expr.
type().
id() == ID_signedbv)
1859 else if(div_expr.
type().
id() == ID_floatbv)
1866void goto_check_ct::check_rec_arithmetic_op(
1870 if(expr.
type().
id() == ID_signedbv || expr.
type().
id() == ID_unsignedbv)
1875 expr.
operands().size() == 2 && expr.
id() == ID_minus &&
1876 expr.
operands()[0].type().id() == ID_pointer &&
1877 expr.
operands()[1].type().id() == ID_pointer)
1882 else if(expr.
type().
id() == ID_floatbv)
1887 else if(expr.
type().
id() == ID_pointer)
1895 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1900 auto new_guard = [&
guard, &quantifier_expr](
exprt expr) {
1904 check_rec(quantifier_expr.where(), new_guard);
1907 else if(expr.
id() == ID_address_of)
1912 else if(expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies)
1917 else if(expr.
id() == ID_if)
1923 expr.
id() == ID_member &&
1930 for(
const auto &op : expr.operands())
1931 check_rec(op,
guard);
1933 if(expr.
type().
id() == ID_c_enum_tag)
1936 if(expr.
id() == ID_index)
1940 else if(expr.
id() == ID_div)
1944 else if(expr.
id() == ID_shl || expr.
id() == ID_ashr || expr.
id() == ID_lshr)
1948 if(expr.
id() == ID_shl && expr.
type().
id() == ID_signedbv)
1951 else if(expr.
id() == ID_mod)
1957 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
1958 expr.
id() == ID_unary_minus)
1960 check_rec_arithmetic_op(expr,
guard);
1962 else if(expr.
id() == ID_typecast)
1965 expr.
id() == ID_le || expr.
id() == ID_lt || expr.
id() == ID_ge ||
1968 else if(expr.
id() == ID_dereference)
1977 expr.
id() == ID_count_leading_zeros || expr.
id() == ID_count_trailing_zeros)
2003 "dynamically allocated memory never freed",
2011 const irep_idt &function_identifier,
2014 const auto &function_symbol =
ns.
lookup(function_identifier);
2015 mode = function_symbol.mode;
2022 bool did_something =
false;
2036 for(
const auto &d : pragmas)
2040 if(matched.has_value())
2042 auto named_check = matched.value();
2043 auto name = named_check.first;
2044 auto status = named_check.second;
2049 resetter.
set_flag(*flag,
true, name);
2052 resetter.
set_flag(*flag,
false, name);
2084 annotated_location.
set_comment(
"error label " + label);
2085 annotated_location.
set(
"user-provided",
true);
2103 const irep_idt &statement = code.get_statement();
2105 if(statement == ID_expression)
2109 else if(statement == ID_printf)
2111 for(
const auto &op : code.operands())
2169 (function_identifier ==
"abort" || function_identifier ==
"exit" ||
2170 function_identifier ==
"_Exit" ||
2171 (i.
labels.size() == 1 && i.
labels.front() ==
"__VERIFIER_abort")))
2191 std::move(address_of_expr),
2211 if(instruction.source_location().is_nil())
2213 instruction.source_location_nonconst().id(
irep_idt());
2215 if(!it->source_location().get_file().empty())
2216 instruction.source_location_nonconst().set_file(
2217 it->source_location().get_file());
2219 if(!it->source_location().get_line().empty())
2220 instruction.source_location_nonconst().set_line(
2221 it->source_location().get_line());
2223 if(!it->source_location().get_function().empty())
2224 instruction.source_location_nonconst().set_function(
2225 it->source_location().get_function());
2227 if(!it->source_location().get_column().empty())
2229 instruction.source_location_nonconst().set_column(
2230 it->source_location().get_column());
2271 const exprt &address,
2281 const exprt in_bounds_of_some_explicit_allocation =
2296 in_bounds_of_some_explicit_allocation,
2298 "deallocated dynamic object"));
2305 in_bounds_of_some_explicit_allocation,
2312 const or_exprt object_bounds_violation(
2318 in_bounds_of_some_explicit_allocation,
2320 "pointer outside dynamic object bounds"));
2325 const or_exprt object_bounds_violation(
2331 in_bounds_of_some_explicit_allocation,
2333 "pointer outside object bounds"));
2341 "invalid integer address"));
2349 const exprt &address,
2370 const exprt &pointer,
2384 std::move(upper_bound), ID_le,
plus_exprt{a.first, a.second}};
2386 alloc_disjuncts.push_back(
2387 and_exprt{std::move(lb_check), std::move(ub_check)});
2393 const irep_idt &function_identifier,
2400 goto_check.
goto_check(function_identifier, goto_function);
2415 goto_check.
goto_check(gf_entry.first, gf_entry.second);
2447 auto col = s.find(
":");
2449 if(col == std::string::npos)
2452 auto name = s.substr(col + 1);
2458 if(!s.compare(0, 6,
"enable"))
2460 else if(!s.compare(0, 7,
"disable"))
2462 else if(!s.compare(0, 7,
"checked"))
2468 return std::pair<irep_idt, check_statust>{name, status};
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 count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_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.
API to expression classes that are internal to the C frontend.
static exprt guard(const exprt::operandst &guards, exprt cond)
unsignedbv_typet size_type()
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.
bool is_boolean() const
Return whether the expression represents a Boolean.
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.
const source_locationt & source_location() const
source_locationt & add_source_location()
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
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_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
void memory_leak_check(const irep_idt &function_id)
exprt is_in_bounds_of_some_explicit_allocation(const exprt &pointer, 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.
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
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)
Check that a member expression is valid:
conditionst get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size)
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
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 &)
optionalt< std::pair< irep_idt, check_statust > > named_check_statust
optional (named-check, status) pair
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 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)
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
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
bool has_condition() const
Does this instruction have a condition?
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
const exprt & condition() const
Get the condition of gotos, assume, assert.
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::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
void set(const irep_idt &name, const irep_idt &value)
const std::string & id_string() const
const irep_idt & id() const
Evaluates to true if the operand is infinite.
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Formats the given expression in a language-specific way.
flagst get(const goto_programt::const_targett t, const exprt &src)
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)
void add_pragma(const irep_idt &pragma)
const irept::named_subt & get_pragmas() const
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
bool has_prefix(const std::string &s, const std::string &prefix)
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.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
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)
bool can_cast_expr< object_size_exprt >(const exprt &base)
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 prophecy_r_or_w_ok_exprt & to_prophecy_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< prophecy_r_or_w_ok_exprt >(const exprt &base)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
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 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)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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