191 const exprt &src_expr,
211 const exprt &address,
214 const exprt &pointer,
218 const exprt &address,
237 const exprt &asserted_expr,
239 const std::string &property_class,
241 const exprt &src_expr,
298 for(
const auto &instruction : gf_entry.second.body.instructions)
300 if(!instruction.is_function_call())
312 args[0].type().id()!=ID_unsignedbv ||
313 args[1].type().id()!=ID_unsignedbv)
314 throw "expected two unsigned arguments to "
317 assert(args[0].type()==args[1].type());
325 if(lhs.
id()==ID_index)
327 else if(lhs.
id()==ID_member)
329 else if(lhs.
id()==ID_symbol)
385 std::vector<exprt> disjuncts;
386 for(
const auto &enum_value : enum_values)
415 if(distance_type.
id()==ID_signedbv)
422 "shift distance is negative",
431 if(op_type.
id()==ID_unsignedbv || op_type.
id()==ID_signedbv)
438 "shift distance too large",
444 if(op_type.
id()==ID_signedbv && expr.
id()==ID_shl)
451 "shift operand is negative",
462 "shift of non-integer type",
497 const auto &type = expr.
type();
499 if(type.id() == ID_signedbv)
513 or_exprt(int_min_neq, minus_one_neq),
514 "result of signed mod is not representable",
532 if(type.
id()!=ID_signedbv &&
533 type.
id()!=ID_unsignedbv)
536 if(expr.
id()==ID_typecast)
541 const typet &old_type = op.type();
543 if(type.
id()==ID_signedbv)
547 if(old_type.
id()==ID_signedbv)
550 if(new_width>=old_width)
560 and_exprt(no_overflow_lower, no_overflow_upper),
561 "arithmetic overflow on signed type conversion",
567 else if(old_type.
id()==ID_unsignedbv)
570 if(new_width>=old_width+1)
578 "arithmetic overflow on unsigned to signed type conversion",
584 else if(old_type.
id()==ID_floatbv)
598 and_exprt(no_overflow_lower, no_overflow_upper),
599 "arithmetic overflow on float to signed integer type conversion",
606 else if(type.
id()==ID_unsignedbv)
610 if(old_type.
id()==ID_signedbv)
614 if(new_width>=old_width-1)
622 "arithmetic overflow on signed to unsigned type conversion",
638 and_exprt(no_overflow_lower, no_overflow_upper),
639 "arithmetic overflow on signed to unsigned type conversion",
646 else if(old_type.
id()==ID_unsignedbv)
649 if(new_width>=old_width)
657 "arithmetic overflow on unsigned to unsigned type conversion",
663 else if(old_type.
id()==ID_floatbv)
677 and_exprt(no_overflow_lower, no_overflow_upper),
678 "arithmetic overflow on float to unsigned integer type conversion",
707 if(expr.
id()==ID_div)
710 if(type.
id()==ID_signedbv)
721 "arithmetic overflow on signed division",
730 else if(expr.
id()==ID_unary_minus)
732 if(type.
id()==ID_signedbv)
742 "arithmetic overflow on signed unary minus",
751 else if(expr.
id() == ID_shl)
753 if(type.
id() == ID_signedbv)
756 const auto &op = shl_expr.op();
758 const auto op_width = op_type.get_width();
759 const auto &distance = shl_expr.distance();
760 const auto &distance_type = distance.type();
764 exprt neg_value_shift;
766 if(op_type.id() == ID_unsignedbv)
774 exprt neg_dist_shift;
776 if(distance_type.id() == ID_unsignedbv)
785 distance, ID_gt,
from_integer(op_width, distance_type));
790 new_type.set_width(op_width * 2);
801 bool allow_shift_into_sign_bit =
true;
809 allow_shift_into_sign_bit =
false;
812 else if(
mode == ID_cpp)
818 allow_shift_into_sign_bit =
false;
822 const unsigned number_of_top_bits =
823 allow_shift_into_sign_bit ? op_width : op_width + 1;
827 new_type.get_width() - 1,
828 new_type.get_width() - number_of_top_bits,
831 const exprt top_bits_zero =
845 "arithmetic overflow on signed shl",
863 for(std::size_t i=1; i<expr.
operands().size(); i++)
880 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
884 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
894 type.
id()==ID_unsignedbv?
"unsigned":
"signed";
898 "arithmetic overflow on " + kind +
" " + expr.
id_string(),
916 if(type.
id()!=ID_floatbv)
921 if(expr.
id()==ID_typecast)
926 if(op.type().id() == ID_floatbv)
932 std::move(overflow_check),
933 "arithmetic overflow on floating-point typecast",
944 "arithmetic overflow on floating-point typecast",
953 else if(expr.
id()==ID_div)
960 std::move(overflow_check),
961 "arithmetic overflow on floating-point division",
969 else if(expr.
id()==ID_mod)
974 else if(expr.
id()==ID_unary_minus)
979 else if(expr.
id()==ID_plus || expr.
id()==ID_mult ||
991 expr.
id()==ID_plus?
"addition":
992 expr.
id()==ID_minus?
"subtraction":
993 expr.
id()==ID_mult?
"multiplication":
"";
996 std::move(overflow_check),
997 "arithmetic overflow on floating-point " + kind,
1007 assert(expr.
id()!=ID_minus);
1024 if(expr.
type().
id()!=ID_floatbv)
1027 if(expr.
id()!=ID_plus &&
1028 expr.
id()!=ID_mult &&
1029 expr.
id()!=ID_div &&
1030 expr.
id()!=ID_minus)
1037 if(expr.
id()==ID_div)
1046 div_expr.op0(),
from_integer(0, div_expr.dividend().type())),
1048 div_expr.op1(),
from_integer(0, div_expr.divisor().type())));
1052 isnan=
or_exprt(zero_div_zero, div_inf);
1054 else if(expr.
id()==ID_mult)
1065 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())));
1069 mult_expr.op1(),
from_integer(0, mult_expr.op1().type())),
1072 isnan=
or_exprt(inf_times_zero, zero_times_inf);
1074 else if(expr.
id()==ID_plus)
1095 else if(expr.
id()==ID_minus)
1134 if(expr.
op0().
type().
id()==ID_pointer &&
1143 "same object violation",
1149 for(
const auto &pointer : expr.
operands())
1156 for(
const auto &c : conditions)
1160 "pointer relation: " + c.description,
1161 "pointer arithmetic",
1177 if(expr.
id() != ID_plus && expr.
id() != ID_minus)
1182 "pointer arithmetic expected to have exactly 2 operands");
1188 for(
const auto &c : conditions)
1192 "pointer arithmetic: " + c.description,
1193 "pointer arithmetic",
1202 const exprt &src_expr,
1212 if(expr.
type().
id() == ID_empty)
1224 size = size_of_expr_opt.value();
1229 for(
const auto &c : conditions)
1233 "dereference failure: " + c.description,
1234 "pointer dereference",
1251 const exprt pointer = (expr.
id() == ID_r_ok || expr.
id() == ID_w_ok)
1257 if(pointer.
id() == ID_symbol)
1267 const exprt size = !size_of_expr_opt.has_value()
1269 : size_of_expr_opt.value();
1273 for(
const auto &c : conditions)
1278 "pointer primitives",
1290 return expr.
id() == ID_pointer_object || expr.
id() == ID_pointer_offset ||
1291 expr.
id() == ID_object_size || expr.
id() == ID_r_ok ||
1292 expr.
id() == ID_w_ok || expr.
id() == ID_is_dynamic_object;
1296 const exprt &address,
1303 conditions.push_front(*maybe_null_condition);
1326 if(array_type.
id()==ID_pointer)
1327 throw "index got pointer as array type";
1328 else if(array_type.
id()!=ID_array && array_type.
id()!=ID_vector)
1329 throw "bounds check expected array or vector type, got "
1338 if(index.
type().
id()!=ID_unsignedbv)
1342 index.
id() == ID_typecast &&
1349 const auto i = numeric_cast<mp_integer>(index);
1351 if(!i.has_value() || *i < 0)
1359 assert(p_offset.
type()==effective_offset.
type());
1361 effective_offset=
plus_exprt(p_offset, effective_offset);
1368 effective_offset, ID_ge, std::move(zero));
1372 name +
" lower bound",
1385 const exprt &pointer=
1395 assert(effective_offset.
op0().
type()==effective_offset.
op1().
type());
1397 const auto size_casted =
1402 exprt in_bounds_of_some_explicit_allocation =
1408 std::move(in_bounds_of_some_explicit_allocation),
1414 name +
" dynamic object upper bound",
1422 if(type_size_opt.has_value())
1441 const exprt &size=array_type.
id()==ID_array ?
1450 else if(size.
id()==ID_infinity)
1471 type_size_opt.value());
1475 name +
" upper bound",
1491 name +
" upper bound",
1500 const exprt &asserted_expr,
1502 const std::string &property_class,
1504 const exprt &src_expr,
1508 exprt simplified_expr =
1516 exprt guarded_expr =
1518 ? std::move(simplified_expr)
1521 if(
assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
1525 std::move(guarded_expr), source_location)
1527 std::move(guarded_expr), source_location));
1529 std::string source_expr_string;
1532 t->source_location.set_comment(
comment +
" in " + source_expr_string);
1533 t->source_location.set_property_class(property_class);
1540 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1543 if(expr.
id() == ID_dereference)
1547 else if(expr.
id() == ID_index)
1555 for(
const auto &operand : expr.
operands())
1564 "'" + expr.
id_string() +
"' must be Boolean, but got " + expr.
pretty());
1566 guardt old_guard = guard;
1568 for(
const auto &op : expr.
operands())
1572 "'" + expr.
id_string() +
"' takes Boolean operands only, but got " +
1579 guard = std::move(old_guard);
1586 "first argument of if must be boolean, but got " + if_expr.
cond().
pretty());
1591 guardt old_guard = guard;
1594 guard = std::move(old_guard);
1598 guardt old_guard = guard;
1601 guard = std::move(old_guard);
1620 if(member_offset_opt.has_value())
1647 if(div_expr.
type().
id() == ID_signedbv)
1649 else if(div_expr.
type().
id() == ID_floatbv)
1658 if(expr.
type().
id() == ID_signedbv || expr.
type().
id() == ID_unsignedbv)
1663 expr.
operands().size() == 2 && expr.
id() == ID_minus &&
1664 expr.
operands()[0].type().id() == ID_pointer &&
1665 expr.
operands()[1].type().id() == ID_pointer)
1670 else if(expr.
type().
id() == ID_floatbv)
1675 else if(expr.
type().
id() == ID_pointer)
1684 if(expr.
id() == ID_exists || expr.
id() == ID_forall)
1687 if(expr.
id() == ID_address_of)
1692 else if(expr.
id() == ID_and || expr.
id() == ID_or)
1697 else if(expr.
id() == ID_if)
1703 expr.
id() == ID_member &&
1713 if(expr.
type().
id() == ID_c_enum_tag)
1716 if(expr.
id()==ID_index)
1720 else if(expr.
id()==ID_div)
1724 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr)
1728 if(expr.
id()==ID_shl && expr.
type().
id()==ID_signedbv)
1731 else if(expr.
id()==ID_mod)
1736 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
1737 expr.
id()==ID_mult ||
1738 expr.
id()==ID_unary_minus)
1742 else if(expr.
id()==ID_typecast)
1744 else if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1745 expr.
id()==ID_ge || expr.
id()==ID_gt)
1747 else if(expr.
id()==ID_dereference)
1766 bool modified =
false;
1771 if(op_result.has_value())
1778 if(expr.
id() == ID_r_ok || expr.
id() == ID_w_ok)
1782 expr.
operands().size() == 2,
"r/w_ok must have two operands");
1789 for(
const auto &c : conditions)
1790 conjuncts.push_back(c.assertion);
1795 return std::move(expr);
1808 if(flag != new_value)
1819 *flag_pair.first = flag_pair.second;
1827 const irep_idt &function_identifier,
1832 const auto &function_symbol =
ns.
lookup(function_identifier);
1833 mode = function_symbol.mode;
1835 bool did_something =
false;
1838 util_make_unique<local_bitvector_analysist>(goto_function,
ns);
1849 for(
const auto &d : pragmas)
1851 if(d.first ==
"disable:bounds-check")
1853 else if(d.first ==
"disable:pointer-check")
1855 else if(d.first ==
"disable:memory-leak-check")
1857 else if(d.first ==
"disable:div-by-zero-check")
1859 else if(d.first ==
"disable:enum-range-check")
1861 else if(d.first ==
"disable:signed-overflow-check")
1863 else if(d.first ==
"disable:unsigned-overflow-check")
1865 else if(d.first ==
"disable:pointer-overflow-check")
1867 else if(d.first ==
"disable:float-overflow-check")
1869 else if(d.first ==
"disable:conversion-check")
1871 else if(d.first ==
"disable:undefined-shift-check")
1873 else if(d.first ==
"disable:nan-check")
1875 else if(d.first ==
"disable:pointer-primitive-check")
1893 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1897 if(rw_ok_cond.has_value())
1912 t->source_location.set_property_class(
"error label");
1913 t->source_location.set_comment(
"error label "+label);
1914 t->source_location.set(
"user-provided",
true);
1921 const irep_idt &statement = code.get_statement();
1923 if(statement==ID_expression)
1927 else if(statement==ID_printf)
1929 for(
const auto &op : code.operands())
1950 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
1955 if(rw_ok_cond.has_value())
1968 !code_function_call.
arguments().empty() &&
1985 "this is null on method invocation",
1986 "pointer dereference",
1993 for(
const auto &op : code_function_call.
operands())
2006 return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
2011 if(rw_ok_cond.has_value())
2012 return_value = *rw_ok_cond;
2031 "pointer dereference",
2049 did_something =
true;
2057 did_something =
true;
2076 std::move(address_of_expr),
2105 "dynamically allocated memory never freed",
2115 if(instruction.source_location.is_nil())
2117 instruction.source_location.id(
irep_idt());
2119 if(!it->source_location.get_file().empty())
2120 instruction.source_location.set_file(it->source_location.get_file());
2122 if(!it->source_location.get_line().empty())
2123 instruction.source_location.set_line(it->source_location.get_line());
2125 if(!it->source_location.get_function().empty())
2126 instruction.source_location.set_function(
2127 it->source_location.get_function());
2129 if(!it->source_location.get_column().empty())
2131 instruction.source_location.set_column(
2132 it->source_location.get_column());
2135 if(!it->source_location.get_java_bytecode_index().empty())
2137 instruction.source_location.set_java_bytecode_index(
2138 it->source_location.get_java_bytecode_index());
2160 const exprt &address,
2176 const exprt in_bounds_of_some_explicit_allocation =
2191 in_bounds_of_some_explicit_allocation,
2193 "deallocated dynamic object"));
2200 in_bounds_of_some_explicit_allocation,
2207 const or_exprt object_bounds_violation(
2213 in_bounds_of_some_explicit_allocation,
2216 "pointer outside dynamic object bounds"));
2221 const or_exprt object_bounds_violation(
2227 in_bounds_of_some_explicit_allocation,
2231 "pointer outside object bounds"));
2239 "invalid integer address"));
2246 const exprt &address,
2259 return {
conditiont{not_eq_null,
"reference is null"}};
2273 const exprt &pointer,
2287 std::move(upper_bound), ID_le,
plus_exprt{a.first, a.second}};
2289 alloc_disjuncts.push_back(
2290 and_exprt{std::move(lb_check), std::move(ub_check)});
2296 const irep_idt &function_identifier,
2302 goto_check.goto_check(function_identifier, goto_function);
2312 goto_check.collect_allocations(goto_functions);
2316 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 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.
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 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
C enum tag type, i.e., c_enum_typet with an identifier.
const memberst & members() const
std::vector< c_enum_membert > memberst
A codet representing an assignment in the program.
codet representation of a function call statement.
exprt::operandst argumentst
const irep_idt & get_statement() const
struct configt::ansi_ct ansi_c
A constant literal expression.
const irep_idt & get_value() 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.
source_locationt & add_source_location()
bool is_boolean() const
Return whether the expression represents a Boolean.
const source_locationt & source_location() const
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.
Set a Boolean flag to a new value (via set_flag) and restore the previous value when the entire objec...
std::list< std::pair< bool *, bool > > flags_to_reset
void set_flag(bool &flag, bool new_value)
Store the current value of flag and then set its value to new_value.
~flag_resett()
Restore the values of all flags that have been modified via set_flag.
void mod_by_zero_check(const mod_exprt &, const guardt &)
std::set< std::pair< exprt, exprt > > assertionst
void pointer_overflow_check(const exprt &, const guardt &)
bool enable_unsigned_overflow_check
goto_functionst::goto_functiont goto_functiont
std::string array_name(const exprt &)
bool enable_signed_overflow_check
bool enable_built_in_assertions
void goto_check(const irep_idt &function_identifier, goto_functiont &goto_function)
bool is_pointer_primitive(const exprt &expr)
Returns true if the given expression is a pointer primitive such as __CPROVER_r_ok()
conditionst get_pointer_points_to_valid_memory_conditions(const exprt &address, const exprt &size)
void check(const exprt &expr)
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.
std::unique_ptr< local_bitvector_analysist > local_bitvector_analysis
bool check_rec_member(const member_exprt &member, guardt &guard)
Check that a member expression is valid:
void check_rec_address(const exprt &expr, guardt &guard)
Check an address-of expression: if it is a dereference then check the pointer if it is an index then ...
bool enable_enum_range_check
goto_programt::const_targett current_target
void check_rec_logical_op(const exprt &expr, guardt &guard)
Check a logical operation: check each operand in separation while extending the guarding condition as...
bool enable_undefined_shift_check
std::list< conditiont > conditionst
std::pair< exprt, exprt > allocationt
void check_rec_arithmetic_op(const exprt &expr, guardt &guard)
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers),...
void integer_overflow_check(const exprt &, const guardt &)
bool enable_assert_to_assume
void float_overflow_check(const exprt &, const guardt &)
goto_checkt(const namespacet &_ns, const optionst &_options)
guard_managert guard_manager
optionalt< goto_checkt::conditiont > get_pointer_is_null_condition(const exprt &address, const exprt &size)
conditionst get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size)
void bounds_check(const index_exprt &, const guardt &)
exprt is_in_bounds_of_some_explicit_allocation(const exprt &pointer, const exprt &size)
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.
void check_rec_if(const if_exprt &if_expr, guardt &guard)
Check an if expression: check the if-condition alone, and then check the true/false-cases with the gu...
void nan_check(const exprt &, const guardt &)
void check_rec_div(const div_exprt &div_expr, guardt &guard)
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numb...
bool enable_pointer_primitive_check
void undefined_shift_check(const shift_exprt &, const guardt &)
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.
bool enable_pointer_overflow_check
optionst::value_listt error_labelst
void mod_overflow_check(const mod_exprt &, const guardt &)
check a mod expression for the case INT_MIN % -1
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.
void div_by_zero_check(const div_exprt &, const guardt &)
bool enable_conversion_check
void pointer_rel_check(const binary_exprt &, const guardt &)
optionalt< exprt > rw_ok_check(exprt)
expand the r_ok and w_ok predicates
bool enable_div_by_zero_check
void collect_allocations(const goto_functionst &goto_functions)
Fill the list of allocations allocationst with <address, size> for every allocation instruction.
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.
error_labelst error_labels
bool enable_pointer_check
bool enable_memory_leak_check
bool enable_float_overflow_check
void conversion_check(const exprt &, const guardt &)
void check_rec(const exprt &expr, guardt &guard)
Recursively descend into expr and run the appropriate check for each sub-expression,...
std::list< allocationt > allocationst
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.
bool is_end_function() const
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?
codet code
Do not read or modify directly – use get_X() instead.
const codet & get_other() const
Get the statement for OTHER.
source_locationt source_location
The location of the instruction in the source file.
bool has_condition() const
Does this instruction have a condition?
const exprt & return_value() const
Get the return value of a RETURN instruction.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
bool is_function_call() 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())
void add(const exprt &expr)
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
bool get_bool(const irep_namet &name) const
const irept & find(const irep_namet &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
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.
const exprt & root_object() const
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...
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 ...
A base class for shift and rotate operators.
A side_effect_exprt that returns a non-deterministically chosen value.
const irept::named_subt & get_pragmas() const
const irep_idt & get_property_class() const
static bool is_built_in(const std::string &s)
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.
const irep_idt & get_identifier() const
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
Fixed-width bit-vector with unsigned binary interpretation.
const constant_exprt & size() const
bool has_prefix(const std::string &s, const std::string &prefix)
#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)
#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< 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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< 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 malloc_object(const exprt &pointer, const namespacet &ns)
exprt dynamic_size(const namespacet &ns)
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 dynamic_object(const exprt &pointer)
exprt null_object(const exprt &pointer)
exprt null_pointer(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)
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
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 if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_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 member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
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 mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
enum configt::ansi_ct::c_standardt c_standard
enum configt::cppt::cpp_standardt cpp_standard
conditiont(const exprt &_assertion, const std::string &_description)
This is unused by this implementation of guards, but can be used by other implementations of the same...
bool is_static_lifetime() const
bool is_dynamic_local() const
bool is_dynamic_heap() const
bool is_uninitialized() const
bool is_integer_address() const