30 for(std::size_t i=0; i<
entries.size(); i++)
31 out <<
"STORE " << i <<
": " <<
to_string(i,
"") <<
'\n';
96 if(expr.
id()==ID_typecast)
100 if(expr.
type().
id()==ID_signedbv ||
101 expr.
type().
id()==ID_unsignedbv)
103 if(expr.
op0().
type().
id()==ID_signedbv ||
122 if(expr.
type().
id()==ID_pointer)
123 if(expr.
get(ID_value)==ID_NULL)
139 if(expr.
id()==ID_member)
145 if(expr.
id()==ID_symbol)
161 if(expr.
id()==ID_address_of)
170 if(expr.
id()==ID_symbol)
172 else if(expr.
id()==ID_member)
177 else if(expr.
id()==ID_index)
188 const std::pair<unsigned, unsigned> &p,
204 dest.insert(std::pair<unsigned, unsigned>(f, s));
216 bool constant_seen=
false;
239 for(
const auto &le :
le_set)
242 for(
const auto &ne :
ne_set)
248 const std::pair<unsigned, unsigned> &eq,
249 const std::pair<unsigned, unsigned> &ineq)
251 std::pair<unsigned, unsigned> n;
255 if(eq.first==ineq.first)
262 if(eq.first==ineq.second)
269 if(eq.second==ineq.first)
276 if(eq.second==ineq.second)
286 std::pair<unsigned, unsigned> s=p;
287 std::swap(s.first, s.second);
300 std::pair<unsigned, unsigned> s=p;
301 std::swap(s.first, s.second);
318 std::ostream &out)
const 350 out <<
to_string(bounds.first, identifier)
351 <<
" in " << bounds.second
355 for(
const auto &le :
le_set)
358 <<
" <= " <<
to_string(le.second, identifier)
362 for(
const auto &ne :
ne_set)
365 <<
" != " <<
to_string(ne.second, identifier)
372 if(expr.
type()==type)
375 if(type.
id()==ID_unsignedbv)
399 if(expr.
type().
id()!=ID_bool)
400 throw "non-Boolean argument to strengthen()";
403 std::cout <<
"S: " <<
from_expr(*
ns,
"", expr) <<
'\n';
421 else if(expr.
id()==ID_not)
425 else if(expr.
id()==ID_and)
430 else if(expr.
id()==ID_le ||
438 if(expr.
op1().
id()==ID_bitand)
452 std::pair<unsigned, unsigned> p;
471 else if(expr.
id()==ID_lt)
486 else if(expr.
id()==ID_equal)
492 if(op_type.id()==ID_struct)
497 for(
const auto &comp : struct_type.
components())
500 expr.
op0(), comp.get_name(), comp.
type());
502 expr.
op1(), comp.get_name(), comp.
type());
504 const equal_exprt equality(lhs_member_expr, rhs_member_expr);
516 if(expr.
op1().
id()==ID_bitand)
530 else if(expr.
op0().
id()==ID_bitand)
533 std::swap(tmp.
op0(), tmp.
op1());
539 if(expr.
op1().
id()==ID_typecast)
544 else if(expr.
op0().
id()==ID_typecast)
550 std::pair<unsigned, unsigned> p, s;
564 std::swap(s.first, s.second);
572 else if(expr.
id()==ID_notequal)
576 std::pair<unsigned, unsigned> p;
599 if(expr.
type().
id()!=ID_bool)
600 throw "implies: non-Boolean expression";
603 std::cout <<
"I: " <<
from_expr(*
ns,
"", expr) <<
'\n';
611 else if(expr.
id()==ID_not)
615 else if(expr.
id()==ID_and)
623 else if(expr.
id()==ID_or)
629 else if(expr.
id()==ID_le ||
631 expr.
id()==ID_equal ||
632 expr.
id()==ID_notequal)
636 std::pair<unsigned, unsigned> p;
658 else if(expr.
id()==ID_lt)
670 else if(expr.
id()==ID_equal)
672 else if(expr.
id()==ID_notequal)
695 if(e_a.
type().
id()==ID_unsignedbv)
699 bounds_mapt::const_iterator it=
bounds_map.find(a);
707 if(expr.
type().
id()!=ID_bool)
708 throw "nnf: non-Boolean expression";
720 else if(expr.
id()==ID_not)
728 else if(expr.
id()==ID_and)
736 else if(expr.
id()==ID_or)
744 else if(expr.
id()==ID_typecast)
748 if(expr.
op0().
type().
id()==ID_unsignedbv ||
763 else if(expr.
id()==ID_le)
769 std::swap(expr.
op0(), expr.
op1());
772 else if(expr.
id()==ID_lt)
778 std::swap(expr.
op0(), expr.
op1());
781 else if(expr.
id()==ID_ge)
788 std::swap(expr.
op0(), expr.
op1());
791 else if(expr.
id()==ID_gt)
798 std::swap(expr.
op0(), expr.
op1());
801 else if(expr.
id()==ID_equal)
804 expr.
id(ID_notequal);
806 else if(expr.
id()==ID_notequal)
821 if(expr.
id()==ID_address_of)
827 if(expr.
id()==ID_symbol ||
828 expr.
id()==ID_member)
843 bounds_mapt::const_iterator it=
bounds_map.find(a);
847 if(it->second.singleton())
864 if(expr.
type().
id()==ID_pointer)
933 std::size_t old_ne_set=
ne_set.size();
934 std::size_t old_le_set=
le_set.size();
944 old_ne_set!=
ne_set.size() ||
945 old_le_set!=
le_set.size())
955 for(bounds_mapt::iterator
960 bounds_mapt::const_iterator o_it=other.find(it->first);
962 if(o_it==other.end())
964 bounds_mapt::iterator next(it);
973 it->second.approx_union_with(o_it->second);
993 if(lhs.
id()==ID_symbol ||
1000 else if(lhs.
id()==ID_index)
1004 else if(lhs.
id()==ID_dereference)
1009 else if(lhs.
id()==
"object_value")
1014 else if(lhs.
id()==ID_if)
1021 else if(lhs.
id()==ID_typecast)
1027 else if(lhs.
id()==
"valid_object")
1030 else if(lhs.
id()==
"dynamic_size")
1033 else if(lhs.
id()==ID_byte_extract_little_endian ||
1034 lhs.
id()==ID_byte_extract_big_endian)
1040 else if(lhs.
id() == ID_null_object ||
1041 lhs.
id() ==
"is_zero_string" ||
1042 lhs.
id() ==
"zero_string" ||
1043 lhs.
id() ==
"zero_string_length")
1048 throw "modifies: unexpected lhs: "+lhs.
id_string();
1074 if(statement==ID_block)
1079 else if(statement==ID_assign ||
1083 throw "assignment expected to have two operands";
1087 else if(statement==ID_decl)
1094 else if(statement==ID_expression)
1098 else if(statement==ID_function_call)
1103 else if(statement==ID_cpp_delete ||
1104 statement==ID_cpp_delete_array)
1108 else if(statement==ID_free)
1112 else if(statement==ID_printf)
1116 else if(statement==
"lock" ||
1117 statement==
"unlock" ||
1124 std::cerr << code.
pretty() <<
'\n';
1125 throw "invariant_sett: unexpected statement: "+
id2string(statement);
const irept & get_nil_irep()
void get_bounds(unsigned a, boundst &dest) const
The type of an expression.
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
tvt is_lt(std::pair< unsigned, unsigned > p) const
void strengthen_rec(const exprt &expr)
number_type number(const key_type &a)
const std::string & id2string(const irep_idt &d)
static bool is_constant_address(const exprt &expr)
static void nnf(exprt &expr, bool negate=false)
const std::string integer2string(const mp_integer &n, unsigned base)
static void intersection(ineq_sett &dest, const ineq_sett &other)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
void strengthen(const exprt &expr)
bool make_union(const invariant_sett &other_invariants)
const irep_idt & get_identifier() const
void add_ne(const std::pair< unsigned, unsigned > &p)
const exprt & get_expr(unsigned n) const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool get(const exprt &expr, unsigned &n)
The null pointer constant.
const componentst & components() const
void add(const std::pair< unsigned, unsigned > &p, ineq_sett &dest)
tvt is_eq(std::pair< unsigned, unsigned > p) const
std::string build_string(const exprt &expr) const
void add_type_bounds(const exprt &expr, const typet &type)
size_type count_roots() const
void add_bounds(unsigned a, const boundst &bound)
void assignment(const exprt &lhs, const exprt &rhs)
Extract member of struct or union.
exprt get_constant(const exprt &expr) const
void make_union(size_type a, size_type b)
interval_templatet< T > upper_interval(const T &u)
void output(std::ostream &out) const
tvt implies(const exprt &expr) const
bool is_root(size_type a) const
size_type find(size_type a) const
const irep_idt & id() const
The boolean constant true.
bool has_eq(const std::pair< unsigned, unsigned > &p) const
optionalt< number_type > get_number(const key_type &a) const
void apply_code(const codet &code)
API to expression classes.
size_type count(size_type a) const
const irep_idt & get(const irep_namet &name) const
#define PRECONDITION(CONDITION)
unsigned add(const exprt &expr)
bool is_constant(unsigned n) const
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
unsigned_union_find eq_set
const typet & follow(const typet &) const
std::map< unsigned, boundst > bounds_mapt
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
typename Map::mapped_type number_type
std::string to_string(unsigned n, const irep_idt &identifier) const
interval_templatet< mp_integer > boundst
tvt is_ne(std::pair< unsigned, unsigned > p) const
void isolate(size_type a)
The boolean constant false.
std::size_t get_width() const
void check_index(size_type a)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
void simplify(exprt &expr) const
bool has_ne(const std::pair< unsigned, unsigned > &p) const
Base class for all expressions.
inv_object_storet * object_store
std::string to_string(unsigned a, const irep_idt &identifier) const
void add_eq(const std::pair< unsigned, unsigned > &eq)
const std::string & get_string(const irep_namet &name) const
static bool is_constant_address_rec(const exprt &expr)
std::vector< entryt > entries
const std::string & id_string() const
#define Forall_operands(it, expr)
bool make_union_bounds_map(const bounds_mapt &other)
const codet & to_code(const exprt &expr)
std::set< std::pair< unsigned, unsigned > > ineq_sett
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
tvt implies_rec(const exprt &expr) const
A statement in a programming language.
void modifies(const exprt &lhs)
bool has_le(const std::pair< unsigned, unsigned > &p) const
Generic exception types primarily designed for use with invariants.
void intersection(const unsigned_union_find &other)
bool get_object(const exprt &expr, unsigned &n) const
void output(const irep_idt &identifier, std::ostream &out) const
interval_templatet< T > lower_interval(const T &l)
tvt is_le(std::pair< unsigned, unsigned > p) const
void add_le(const std::pair< unsigned, unsigned > &p)