58 _options.get_bool_option(
"memory-cleanup-check");
61 _options.get_bool_option(
"float-div-by-zero-check");
64 _options.get_bool_option(
"signed-overflow-check");
66 _options.get_bool_option(
"unsigned-overflow-check");
68 _options.get_bool_option(
"pointer-overflow-check");
71 _options.get_bool_option(
"undefined-shift-check");
73 _options.get_bool_option(
"float-overflow-check");
80 _options.get_bool_option(
"pointer-primitive-check");
219 std::optional<goto_check_ct::conditiont>
222 const exprt &address,
225 const exprt &pointer,
229 const exprt &address,
250 const std::string &property_class,
376 if(flag != new_value)
440 for(
const auto &instruction :
gf_entry.second.body.instructions)
442 if(!instruction.is_function_call())
445 const auto &function = instruction.call_function();
453 instruction.call_arguments();
461 args[0].type() == args[1].type(),
462 "arguments of allocated_memory must have same type");
534 "floating-point division by zero",
535 "float-division-by-zero",
557 if(d.first ==
"disable:enum-range-check")
592 "shift distance is negative",
609 "shift distance too large",
623 "shift operand is negative",
635 "shift of non-integer type",
674 const auto &type = expr.
type();
691 "result of signed mod is not representable",
736 "arithmetic overflow on signed type conversion",
754 "arithmetic overflow on unsigned to signed type conversion",
777 "arithmetic overflow on float to signed integer type conversion",
801 "arithmetic overflow on signed to unsigned type conversion",
819 "arithmetic overflow on signed to unsigned type conversion",
838 "arithmetic overflow on unsigned to unsigned type conversion",
861 "arithmetic overflow on float to unsigned integer type conversion",
904 "arithmetic overflow on signed division",
926 "arithmetic overflow on signed unary minus",
943 "arithmetic overflow on unsigned unary minus",
961 const auto &distance =
shl_expr.distance();
1050 "arithmetic overflow on signed shl",
1069 for(std::size_t i = 1; i < expr.
operands().size(); i++)
1078 tmp.operands().resize(i);
1081 std::string kind = type.
id() ==
ID_unsignedbv ?
"unsigned" :
"signed";
1085 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
1093 else if(expr.
operands().size() == 2)
1095 std::string kind = type.
id() ==
ID_unsignedbv ?
"unsigned" :
"signed";
1100 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
1111 std::string kind = type.
id() ==
ID_unsignedbv ?
"unsigned" :
"signed";
1115 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
1149 "arithmetic overflow on floating-point typecast",
1161 "arithmetic overflow on floating-point typecast",
1179 "arithmetic overflow on floating-point division",
1208 std::string kind = expr.
id() ==
ID_plus ?
"addition"
1210 : expr.
id() ==
ID_mult ?
"multiplication"
1215 "arithmetic overflow on floating-point " + kind,
1224 else if(expr.
operands().size() >= 3)
1361 "same object violation",
1368 for(
const auto &pointer : expr.
operands())
1375 for(
const auto &
c : conditions)
1379 "pointer relation: " +
c.description,
1380 "pointer arithmetic",
1402 "pointer arithmetic expected to have exactly 2 operands");
1434 for(
const auto &
c : conditions)
1438 "pointer arithmetic: " +
c.description,
1439 "pointer arithmetic",
1476 for(
const auto &
c : conditions)
1480 "dereference failure: " +
c.description,
1481 "pointer dereference",
1499 const exprt pointer =
1518 for(
const auto &
c : conditions)
1523 "pointer primitives",
1551 const exprt &address,
1565 return ::array_name(
ns, expr);
1592 throw "index got pointer as array type";
1594 throw "bounds check expected array or vector type, got " +
1601 ode.build(expr,
ns);
1616 if(!i.has_value() || *i < 0)
1639 name +
" lower bound",
1674 name +
" dynamic object upper bound",
1719 name +
" upper bound",
1733 name +
" upper bound",
1757 "count " + name +
" zeros is undefined for value zero",
1768 const std::string &property_class,
1775 exprt simplified_expr =
1841 "'" + expr.
id_string() +
"' must be Boolean, but got " + expr.
pretty());
1845 for(
const auto &op : expr.
operands())
1849 "'" + expr.
id_string() +
"' takes Boolean operands only, but got " +
1866 "first argument of if must be boolean, but got " +
if_expr.cond().pretty());
2022 for(
const auto &op : expr.
operands())
2095 "dynamically allocated memory never freed",
2104 const irep_idt &function_identifier,
2118 std::make_unique<local_bitvector_analysist>(goto_function,
ns);
2142 resetter.set_flag(*flag,
true, name);
2145 resetter.set_flag(*flag,
false, name);
2148 resetter.disable_flag(*flag, name);
2196 const irep_idt &statement = code.get_statement();
2204 for(
const auto &op : code.operands())
2213 check(assign_lhs,
true);
2214 check(assign_rhs,
false);
2249 (function_identifier ==
"abort" || function_identifier ==
"exit" ||
2250 function_identifier ==
"_Exit" ||
2251 (i.
labels.size() == 1 && i.
labels.front() ==
"__VERIFIER_abort")))
2291 if(instruction.source_location().is_nil())
2293 instruction.source_location_nonconst().id(
irep_idt());
2295 if(!it->source_location().get_file().empty())
2296 instruction.source_location_nonconst().set_file(
2297 it->source_location().get_file());
2299 if(!it->source_location().get_line().empty())
2300 instruction.source_location_nonconst().set_line(
2301 it->source_location().get_line());
2303 if(!it->source_location().get_function().empty())
2304 instruction.source_location_nonconst().set_function(
2305 it->source_location().get_function());
2307 if(!it->source_location().get_column().empty())
2309 instruction.source_location_nonconst().set_column(
2310 it->source_location().get_column());
2351 const exprt &address,
2378 "deallocated dynamic object"));
2400 "pointer outside dynamic object bounds"));
2413 "pointer outside object bounds"));
2421 "invalid integer address"));
2427std::optional<goto_check_ct::conditiont>
2429 const exprt &address,
2450 const exprt &pointer,
2473 const irep_idt &function_identifier,
2480 goto_check.
goto_check(function_identifier, goto_function);
2527 auto col = s.find(
":");
2529 if(
col == std::string::npos)
2532 auto name = s.substr(
col + 1);
2538 if(!s.compare(0, 6,
"enable"))
2540 else if(!s.compare(0, 7,
"disable"))
2542 else if(!s.compare(0, 7,
"checked"))
2548 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)
pointer_typet pointer_type(const typet &subtype)
signedbv_typet pointer_diff_type()
bitvector_typet char_type()
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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.
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_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
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_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 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
conditionst get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size)
void check_rec(const exprt &expr, const guardt &guard, bool is_assigned)
Recursively descend into expr and run the appropriate check for each sub-expression,...
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 check(const exprt &expr, bool is_assigned)
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
std::pair< exprt, exprt > allocationt
void pointer_overflow_check(const exprt &, const guardt &)
bool enable_memory_leak_check
void add_guarded_property(const exprt &asserted_expr, const std::string &comment, const std::string &property_class, bool is_fatal, const source_locationt &source_location, const exprt &src_expr, const guardt &guard)
Include the asserted_expr in the code conditioned by the guard.
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 enum_range_check(const exprt &, const guardt &, bool is_assigned)
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.
static ieee_float_valuet minus_infinity(const ieee_float_spect &_spec)
constant_exprt to_expr() const
static ieee_float_valuet plus_infinity(const ieee_float_spect &_spec)
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
void from_integer(const mp_integer &i)
The trinary if-then-else operator.
std::string pretty(unsigned indent=0, unsigned max_indent=0) 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)).
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...
The null pointer constant.
Split an expression into a base object and a (byte) offset.
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 ...
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)
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
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.
static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
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)
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)
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.
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)
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.
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