59 _options.get_bool_option(
"signed-overflow-check");
61 _options.get_bool_option(
"unsigned-overflow-check");
64 _options.get_bool_option(
"float-overflow-check");
71 _options.get_bool_option(
"built-in-assertions");
154 const exprt &address,
173 const std::string &property_class,
261 const auto &type = expr.
type();
278 "result of signed mod is not representable",
321 "arithmetic overflow on signed type conversion",
337 "arithmetic overflow on unsigned to signed type conversion",
357 "arithmetic overflow on float to signed integer type conversion",
379 "arithmetic overflow on signed to unsigned type conversion",
395 "arithmetic overflow on signed to unsigned type conversion",
412 "arithmetic overflow on unsigned to unsigned type conversion",
432 "arithmetic overflow on float to unsigned integer type conversion",
471 "arithmetic overflow on signed division",
491 "arithmetic overflow on signed unary minus",
506 "arithmetic overflow on unsigned unary minus",
522 const auto &distance =
shl_expr.distance();
591 "arithmetic overflow on signed shl",
608 for(std::size_t
i = 1;
i < expr.
operands().size();
i++)
617 tmp.operands().resize(
i);
624 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
630 else if(expr.
operands().size() == 2)
637 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
650 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
682 "arithmetic overflow on floating-point typecast",
692 "arithmetic overflow on floating-point typecast",
708 "arithmetic overflow on floating-point division",
739 : expr.
id() ==
ID_mult ?
"multiplication" :
"";
743 "arithmetic overflow on floating-point " + kind,
750 else if(expr.
operands().size() >= 3)
896 for(
const auto &
c : conditions)
900 "dereference failure: " +
c.description,
901 "pointer dereference",
909 const exprt &address,
922 return ::array_name(
ns, expr);
946 throw "index got pointer as array type";
948 throw "bounds check expected array or vector type, got " +
970 if(!
i.has_value() || *
i < 0)
992 name +
" lower bound",
1017 name +
" dynamic object upper bound",
1058 name +
" upper bound",
1070 name +
" upper bound",
1080 const std::string &property_class,
1085 exprt simplified_expr =
1096 std::move(simplified_expr), source_location)
1098 std::move(simplified_expr), source_location));
1104 t->source_location_nonconst().set_comment(
1106 t->source_location_nonconst().set_property_class(property_class);
1258 bool modified =
false;
1274 expr.
operands().size() == 2,
"r/w_ok must have two operands");
1281 for(
const auto &
c : conditions)
1287 return std::move(expr);
1293 const irep_idt &function_identifier,
1323 if(
i.has_condition())
1325 check(
i.get_condition());
1328 return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
1329 expr.id() == ID_rw_ok;
1341 if(std::find(
i.labels.begin(),
i.labels.end(), label) !=
i.labels.end())
1349 t->source_location_nonconst().set_property_class(
"error label");
1350 t->source_location_nonconst().set_comment(
"error label " + label);
1351 t->source_location_nonconst().set(
"user-provided",
true);
1357 const auto &code =
i.get_other();
1358 const irep_idt &statement = code.get_statement();
1366 for(
const auto &op : code.operands())
1370 else if(
i.is_assign())
1372 const exprt &assign_lhs =
i.assign_lhs();
1373 const exprt &assign_rhs =
i.assign_rhs();
1391 else if(
i.is_function_call())
1393 const auto &function =
i.call_function();
1399 function.type().id() ==
ID_code &&
1402 exprt pointer =
i.call_arguments()[0];
1414 "this is null on method invocation",
1415 "pointer dereference",
1416 i.source_location(),
1422 check(
i.call_function());
1424 for(
const auto &arg :
i.call_arguments())
1430 else if(
i.is_set_return_value())
1437 return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
1438 expr.id() == ID_rw_ok;
1441 exprt &return_value =
i.return_value();
1447 else if(
i.is_throw())
1451 i.get_code().operands().size() == 1 &&
1452 i.get_code().op0().operands().size() == 1)
1464 "pointer dereference",
1465 i.source_location(),
1472 else if(
i.is_assert())
1478 i.source_location().get_property_class() !=
"error label") ||
1485 else if(
i.is_assume())
1493 else if(
i.is_dead())
1512 std::move(lhs), std::move(rhs),
i.source_location()));
1513 t->code_nonconst().add_source_location() =
i.source_location();
1518 function_identifier !=
"alloca" &&
1520 "return_value___builtin_alloca" ||
1522 "return_value_alloca"))
1534 std::move(lhs), std::move(rhs),
i.source_location()));
1535 t->code_nonconst().add_source_location() =
i.source_location();
1542 if(instruction.source_location().is_nil())
1544 instruction.source_location_nonconst().id(
irep_idt());
1546 if(!it->source_location().get_file().empty())
1547 instruction.source_location_nonconst().set_file(
1548 it->source_location().get_file());
1550 if(!it->source_location().get_line().empty())
1551 instruction.source_location_nonconst().set_line(
1552 it->source_location().get_line());
1554 if(!it->source_location().get_function().empty())
1555 instruction.source_location_nonconst().set_function(
1556 it->source_location().get_function());
1558 if(!it->source_location().get_column().empty())
1560 instruction.source_location_nonconst().set_column(
1561 it->source_location().get_column());
1564 if(!it->source_location().get_java_bytecode_index().empty())
1566 instruction.source_location_nonconst().set_java_bytecode_index(
1567 it->source_location().get_java_bytecode_index());
1589 const exprt &address,
1608 const irep_idt &function_identifier,
1615 goto_check.goto_check(function_identifier, goto_function);
API to expression classes for bitvectors.
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()
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...
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
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_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
The Boolean constant false.
goto_check_javat(const namespacet &_ns, const optionst &_options, message_handlert &_message_handler)
bool enable_assert_to_assume
void check(const exprt &expr)
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
bool check_rec_member(const member_exprt &member)
Check that a member expression is valid:
bool enable_signed_overflow_check
bool enable_unsigned_overflow_check
void goto_check(const irep_idt &function_identifier, goto_functiont &goto_function)
void check_rec(const exprt &expr)
Recursively descend into expr and run the appropriate check for each sub-expression,...
bool enable_pointer_overflow_check
bool enable_conversion_check
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
bool enable_div_by_zero_check
void invalidate(const exprt &lhs)
Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.
void integer_overflow_check(const exprt &)
void float_overflow_check(const exprt &)
void mod_overflow_check(const mod_exprt &)
check a mod expression for the case INT_MIN % -1
bool enable_built_in_assertions
optionst::value_listt error_labelst
void add_property(const exprt &asserted_expr, const std::string &comment, const std::string &property_class, const source_locationt &source_location, const exprt &src_expr)
Include the asserted_expr in the code conditioned by the guard.
goto_functionst::goto_functiont goto_functiont
std::list< conditiont > conditionst
void bounds_check(const exprt &)
std::string array_name(const exprt &)
goto_programt::const_targett current_target
optionalt< goto_check_javat::conditiont > get_pointer_is_null_condition(const exprt &address, const exprt &size)
void pointer_validity_check(const dereference_exprt &expr, const exprt &src_expr)
Generates VCCs for the validity of the given dereferencing operation.
optionalt< exprt > rw_ok_check(exprt)
expand the r_ok, w_ok and rw_ok predicates
bool enable_pointer_check
void nan_check(const exprt &)
void check_rec_arithmetic_op(const exprt &expr)
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers),...
error_labelst error_labels
void check_rec_div(const div_exprt &div_expr)
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numb...
conditionst get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size)
bool enable_float_overflow_check
void bounds_check_index(const index_exprt &)
void check_rec_address(const exprt &expr)
Check an address-of expression: if it is a dereference then check the pointer if it is an index then ...
std::set< std::pair< exprt, exprt > > assertionst
void div_by_zero_check(const div_exprt &)
void conversion_check(const exprt &)
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
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.
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
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.
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 side_effect_exprt that returns a non-deterministically chosen value.
Expression to hold a symbol (variable)
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.
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
#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_java(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
Check for Errors in Java Programs.
#define Forall_goto_program_instructions(it, program)
Abstract interface to support a programming language.
Field-insensitive, location-sensitive bitvector analysis.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
API to expression classes for Pointers.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
const 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 object_size(const exprt &pointer)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
API to expression classes.
const 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 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 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 code_typet & to_code_type(const typet &type)
Cast a typet to a code_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)