154 const exprt &address,
171 const exprt &asserted_expr,
173 const std::string &property_class,
175 const exprt &src_expr);
209 if(lhs.
id() == ID_index)
211 else if(lhs.
id() == ID_member)
213 else if(lhs.
id() == ID_symbol)
261 const auto &type = expr.
type();
263 if(type.id() == ID_signedbv)
277 or_exprt(int_min_neq, minus_one_neq),
278 "result of signed mod is not representable",
293 if(type.
id() != ID_signedbv && type.
id() != ID_unsignedbv)
296 if(expr.
id() == ID_typecast)
301 const typet &old_type = op.type();
303 if(type.
id() == ID_signedbv)
307 if(old_type.
id() == ID_signedbv)
310 if(new_width >= old_width)
320 and_exprt(no_overflow_lower, no_overflow_upper),
321 "arithmetic overflow on signed type conversion",
326 else if(old_type.
id() == ID_unsignedbv)
329 if(new_width >= old_width + 1)
337 "arithmetic overflow on unsigned to signed type conversion",
342 else if(old_type.
id() == ID_floatbv)
356 and_exprt(no_overflow_lower, no_overflow_upper),
357 "arithmetic overflow on float to signed integer type conversion",
363 else if(type.
id() == ID_unsignedbv)
367 if(old_type.
id() == ID_signedbv)
371 if(new_width >= old_width - 1)
379 "arithmetic overflow on signed to unsigned type conversion",
394 and_exprt(no_overflow_lower, no_overflow_upper),
395 "arithmetic overflow on signed to unsigned type conversion",
401 else if(old_type.
id() == ID_unsignedbv)
404 if(new_width >= old_width)
412 "arithmetic overflow on unsigned to unsigned type conversion",
417 else if(old_type.
id() == ID_floatbv)
431 and_exprt(no_overflow_lower, no_overflow_upper),
432 "arithmetic overflow on float to unsigned integer type conversion",
457 if(expr.
id() == ID_div)
460 if(type.
id() == ID_signedbv)
471 "arithmetic overflow on signed division",
479 else if(expr.
id() == ID_unary_minus)
481 if(type.
id() == ID_signedbv)
491 "arithmetic overflow on signed unary minus",
496 else if(type.
id() == ID_unsignedbv)
506 "arithmetic overflow on unsigned unary minus",
514 else if(expr.
id() == ID_shl)
516 if(type.
id() == ID_signedbv)
519 const auto &op = shl_expr.op();
521 const auto op_width = op_type.get_width();
522 const auto &distance = shl_expr.distance();
523 const auto &distance_type = distance.type();
527 exprt neg_value_shift;
529 if(op_type.id() == ID_unsignedbv)
537 exprt neg_dist_shift;
539 if(distance_type.id() == ID_unsignedbv)
550 distance, ID_gt,
from_integer(op_width, distance_type));
555 new_type.set_width(op_width * 2);
566 bool allow_shift_into_sign_bit =
true;
568 const unsigned number_of_top_bits =
569 allow_shift_into_sign_bit ? op_width : op_width + 1;
573 new_type.get_width() - 1,
574 new_type.get_width() - number_of_top_bits,
577 const exprt top_bits_zero =
591 "arithmetic overflow on signed shl",
608 for(std::size_t i = 1; i < expr.
operands().size(); i++)
620 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
624 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
630 else if(expr.
operands().size() == 2)
632 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
637 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
646 std::string kind = type.
id() == ID_unsignedbv ?
"unsigned" :
"signed";
650 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
665 if(type.
id() != ID_floatbv)
670 if(expr.
id() == ID_typecast)
675 if(op.type().id() == ID_floatbv)
681 std::move(overflow_check),
682 "arithmetic overflow on floating-point typecast",
692 "arithmetic overflow on floating-point typecast",
700 else if(expr.
id() == ID_div)
707 std::move(overflow_check),
708 "arithmetic overflow on floating-point division",
715 else if(expr.
id() == ID_mod)
720 else if(expr.
id() == ID_unary_minus)
725 else if(expr.
id() == ID_plus || expr.
id() == ID_mult || expr.
id() == ID_minus)
735 std::string kind = expr.
id() == ID_plus
737 : expr.
id() == ID_minus
739 : expr.
id() == ID_mult ?
"multiplication" :
"";
742 std::move(overflow_check),
743 "arithmetic overflow on floating-point " + kind,
750 else if(expr.
operands().size() >= 3)
767 if(expr.
type().
id() != ID_floatbv)
771 expr.
id() != ID_plus && expr.
id() != ID_mult && expr.
id() != ID_div &&
772 expr.
id() != ID_minus)
779 if(expr.
id() == ID_div)
788 div_expr.op0(),
from_integer(0, div_expr.dividend().type())),
790 div_expr.op1(),
from_integer(0, div_expr.divisor().type())));
794 isnan =
or_exprt(zero_div_zero, div_inf);
796 else if(expr.
id() == ID_mult)
807 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())));
811 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())),
814 isnan =
or_exprt(inf_times_zero, zero_times_inf);
816 else if(expr.
id() == ID_plus)
837 else if(expr.
id() == ID_minus)
870 const exprt &src_expr)
879 if(expr.
type().
id() == ID_empty)
891 size = size_of_expr_opt.value();
896 for(
const auto &c : conditions)
900 "dereference failure: " + c.description,
901 "pointer dereference",
909 const exprt &address,
914 if(maybe_null_condition.has_value())
915 return {*maybe_null_condition};
937 if(expr.
id() == ID_index)
945 if(array_type.
id() == ID_pointer)
946 throw "index got pointer as array type";
947 else if(array_type.
id() != ID_array && array_type.
id() != ID_vector)
948 throw "bounds check expected array or vector type, got " +
957 if(index.
type().
id() != ID_unsignedbv)
961 index.
id() == ID_typecast &&
968 const auto i = numeric_cast<mp_integer>(index);
970 if(!i.has_value() || *i < 0)
981 effective_offset, p_offset.
type())};
988 effective_offset, ID_ge, std::move(zero));
992 name +
" lower bound",
1017 name +
" dynamic object upper bound",
1025 const exprt &size = array_type.
id() == ID_array
1034 else if(size.
id() == ID_infinity)
1054 type_size_opt.value());
1058 name +
" upper bound",
1070 name +
" upper bound",
1078 const exprt &asserted_expr,
1080 const std::string &property_class,
1082 const exprt &src_expr)
1085 exprt simplified_expr =
1092 if(
assertions.insert(std::make_pair(src_expr, simplified_expr)).second)
1096 std::move(simplified_expr), source_location)
1098 std::move(simplified_expr), source_location));
1100 std::string source_expr_string;
1102 src_expr, source_expr_string,
ns);
1104 t->source_location_nonconst().set_comment(
1105 comment +
" in " + source_expr_string);
1106 t->source_location_nonconst().set_property_class(property_class);
1113 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1116 if(expr.
id() == ID_dereference)
1120 else if(expr.
id() == ID_index)
1128 for(
const auto &operand : expr.
operands())
1148 if(member_offset_opt.has_value())
1175 if(div_expr.
type().
id() == ID_signedbv)
1177 else if(div_expr.
type().
id() == ID_floatbv)
1186 if(expr.
type().
id() == ID_signedbv || expr.
type().
id() == ID_unsignedbv)
1190 else if(expr.
type().
id() == ID_floatbv)
1200 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1203 if(expr.
id() == ID_address_of)
1209 expr.
id() == ID_member &&
1219 if(expr.
id() == ID_index)
1223 else if(expr.
id() == ID_div)
1227 else if(expr.
id() == ID_shl)
1229 if(expr.
type().
id() == ID_signedbv)
1232 else if(expr.
id() == ID_mod)
1237 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
1238 expr.
id() == ID_unary_minus)
1242 else if(expr.
id() == ID_typecast)
1244 else if(expr.
id() == ID_dereference)
1258 bool modified =
false;
1263 if(op_result.has_value())
1270 if(expr.
id() == ID_r_ok || expr.
id() == ID_w_ok || expr.
id() == ID_rw_ok)
1274 expr.
operands().size() == 2,
"r/w_ok must have two operands");
1281 for(
const auto &c : conditions)
1282 conjuncts.push_back(c.assertion);
1287 return std::move(expr);
1293 const irep_idt &function_identifier,
1296 const auto &function_symbol =
ns.
lookup(function_identifier);
1298 if(function_symbol.mode != ID_java)
1303 bool did_something =
false;
1306 util_make_unique<local_bitvector_analysist>(goto_function,
ns);
1328 return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
1329 expr.id() == ID_rw_ok;
1333 if(rw_ok_cond.has_value())
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);
1358 const irep_idt &statement = code.get_statement();
1360 if(statement == ID_expression)
1364 else if(statement == ID_printf)
1366 for(
const auto &op : code.operands())
1382 return expr.
id() == ID_r_ok || expr.
id() == ID_w_ok ||
1383 expr.
id() == ID_rw_ok;
1387 if(rw_ok_cond.has_value())
1399 function.type().id() == ID_code &&
1414 "this is null on method invocation",
1415 "pointer dereference",
1437 return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
1438 expr.id() == ID_rw_ok;
1443 if(rw_ok_cond.has_value())
1444 return_value = *rw_ok_cond;
1464 "pointer dereference",
1482 did_something =
true;
1490 did_something =
true;
1508 std::move(address_of_expr),
1517 variable.
type().
id() == ID_pointer &&
1518 function_identifier !=
"alloca" &&
1520 "return_value___builtin_alloca" ||
1522 "return_value_alloca"))
1526 exprt alloca_result =
1530 std::move(alloca_result),
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,
1601 return {
conditiont{not_eq_null,
"reference is null"}};
1608 const irep_idt &function_identifier,
1615 goto_check.goto_check(function_identifier, goto_function);
1628 goto_check.goto_check(gf_entry.first, gf_entry.second);
std::string array_name(const namespacet &ns, const exprt &expr)
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.
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
const irep_idt & get_statement() 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.
const source_locationt & source_location() const
source_locationt & add_source_location()
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.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
bool is_target() const
Is this node a branch target?
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
bool is_set_return_value() const
const codet & get_code() const
Get the code represented by this instruction.
bool has_condition() const
Does this instruction have a condition?
const codet & get_other() const
Get the statement for OTHER.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
bool is_function_call() const
exprt & assign_rhs_nonconst()
Get the rhs of the assignment for ASSIGN.
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void clear()
Clear the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
instructionst::const_iterator const_targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
IEEE-floating-point equality.
constant_exprt to_expr() const
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
void from_integer(const mp_integer &i)
The trinary if-then-else operator.
bool get_bool(const irep_idt &name) const
const irept & find(const irep_idt &name) const
const std::string & id_string() const
const irep_idt & id() const
Evaluates to true if the operand is infinite.
Extract member of struct or union.
const exprt & struct_op() const
Class that provides messages with a built-in verbosity 'level'.
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
A base class for multi-ary expressions Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
Split an expression into a base object and a (byte) offset.
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
bool get_bool_option(const std::string &option) const
const value_listt & get_list_option(const std::string &option) const
std::list< std::string > value_listt
The plus expression Associativity is not specified.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
A side_effect_exprt that returns a non-deterministically chosen value.
const irep_idt & get_property_class() const
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.
nonstd::optional< T > optionalt
API to expression classes for Pointers.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt 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)