61 _options.get_bool_option(
"memory-cleanup-check");
65 _options.get_bool_option(
"signed-overflow-check");
67 _options.get_bool_option(
"unsigned-overflow-check");
69 _options.get_bool_option(
"pointer-overflow-check");
72 _options.get_bool_option(
"undefined-shift-check");
74 _options.get_bool_option(
"float-overflow-check");
81 _options.get_bool_option(
"pointer-primitive-check");
220 const exprt &address,
223 const exprt &pointer,
227 const exprt &address,
247 const std::string &property_class,
370 if(flag != new_value)
434 for(
const auto &instruction :
gf_entry.second.body.instructions)
436 if(!instruction.is_function_call())
439 const auto &function = instruction.call_function();
447 instruction.call_arguments();
455 args[0].type() == args[1].type(),
456 "arguments of allocated_memory must have same type");
522 if(d.first ==
"disable:enum-range-check")
556 "shift distance is negative",
572 "shift distance too large",
585 "shift operand is negative",
596 "shift of non-integer type",
633 const auto &type = expr.
type();
650 "result of signed mod is not representable",
694 "arithmetic overflow on signed type conversion",
711 "arithmetic overflow on unsigned to signed type conversion",
732 "arithmetic overflow on float to signed integer type conversion",
755 "arithmetic overflow on signed to unsigned type conversion",
772 "arithmetic overflow on signed to unsigned type conversion",
790 "arithmetic overflow on unsigned to unsigned type conversion",
811 "arithmetic overflow on float to unsigned integer type conversion",
853 "arithmetic overflow on signed division",
874 "arithmetic overflow on signed unary minus",
890 "arithmetic overflow on unsigned unary minus",
907 const auto &distance =
shl_expr.distance();
997 "arithmetic overflow on signed shl",
1015 for(std::size_t i = 1; i < expr.
operands().size(); i++)
1024 tmp.operands().resize(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(),
1092 "arithmetic overflow on floating-point typecast",
1103 "arithmetic overflow on floating-point typecast",
1120 "arithmetic overflow on floating-point division",
1152 : expr.
id() ==
ID_mult ?
"multiplication" :
"";
1156 "arithmetic overflow on floating-point " + kind,
1164 else if(expr.
operands().size() >= 3)
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",
1339 "pointer arithmetic expected to have exactly 2 operands");
1371 for(
const auto &
c : conditions)
1375 "pointer arithmetic: " +
c.description,
1376 "pointer arithmetic",
1412 for(
const auto &
c : conditions)
1416 "dereference failure: " +
c.description,
1417 "pointer dereference",
1434 const exprt pointer =
1453 for(
const auto &
c : conditions)
1458 "pointer primitives",
1485 const exprt &address,
1499 return ::array_name(
ns, expr);
1526 throw "index got pointer as array type";
1528 throw "bounds check expected array or vector type, got " +
1535 ode.build(expr,
ns);
1550 if(!i.has_value() || *i < 0)
1573 name +
" lower bound",
1607 name +
" dynamic object upper bound",
1651 name +
" upper bound",
1664 name +
" upper bound",
1687 "count " + name +
" zeros is undefined for value zero",
1697 const std::string &property_class,
1703 exprt simplified_expr =
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 " +
1791 "first argument of if must be boolean, but got " +
if_expr.cond().pretty());
1930 for(
const auto &op : expr.
operands())
2003 "dynamically allocated memory never freed",
2011 const irep_idt &function_identifier,
2049 resetter.set_flag(*flag,
true, name);
2052 resetter.set_flag(*flag,
false, name);
2055 resetter.disable_flag(*flag, name);
2103 const irep_idt &statement = code.get_statement();
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")))
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,
2298 "deallocated dynamic object"));
2320 "pointer outside dynamic object bounds"));
2333 "pointer outside object bounds"));
2341 "invalid integer address"));
2349 const exprt &address,
2370 const exprt &pointer,
2393 const irep_idt &function_identifier,
2400 goto_check.
goto_check(function_identifier, goto_function);
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.
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
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
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
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
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 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)
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.
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.
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...
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.
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.
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)
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.
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