Go to the documentation of this file.
29 auto p = util_make_unique<invariant_set_domaint>(
33 return std::unique_ptr<statet>(p.release());
46 value_sets(_value_sets),
79 typedef std::unordered_map<irep_idt, object_listt> object_cachet;
80 object_cachet object_cache;
87 is.add_objects(globals);
90 for(
const auto &local : locals)
93 object_cachet::const_iterator e_it=object_cache.find(local);
95 if(e_it==object_cache.end())
102 is.add_objects(objects);
107 is.add_objects(e_it->second);
117 std::list<exprt> object_list;
121 for(
const auto &expr : object_list)
127 std::list<exprt> &dest)
132 t.
id() == ID_struct || t.
id() == ID_union || t.
id() == ID_struct_tag ||
133 t.
id() == ID_union_tag)
145 else if(t.
id()==ID_array)
166 std::set<irep_idt> locals;
172 typedef std::unordered_map<irep_idt, object_listt> object_cachet;
173 object_cachet object_cache;
180 is.add_objects(globals);
183 for(
const auto &local : locals)
186 object_cachet::const_iterator e_it=object_cache.find(local);
188 if(e_it==object_cache.end())
195 is.add_objects(objects);
200 is.add_objects(e_it->second);
213 if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
222 if(type.
id()==ID_pointer)
225 type.
id() == ID_struct || type.
id() == ID_union ||
226 type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
228 else if(type.
id()==ID_array)
230 else if(type.
id()==ID_unsignedbv ||
231 type.
id()==ID_signedbv)
233 else if(type.
id()==ID_bool)
258 if(!i_it->is_assert())
262 const auto &d = (*this)[i_it];
268 exprt simplified_guard(i_it->get_condition());
270 invariant_set.
simplify(simplified_guard);
#define Forall_goto_program_instructions(it, program)
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
tvt implies(const exprt &expr) const
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
std::list< unsigned > object_listt
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
Base type for structs and unions.
Pass the necessary arguments to the invariant_set_domaint's when constructed.
state_mapt & internal(void)
std::unique_ptr< statet > make(locationt l) const override
Base class for all expressions.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
void get_objects(const symbolt &symbol, object_listt &dest)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::unique_ptr< T > util_make_unique(Ts &&... ts)
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
unsigned add(const exprt &expr)
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
void add_objects(const goto_programt &goto_program)
bool check_type(const typet &type) const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
invariant_propagationt(const namespacet &_ns, value_setst &_value_sets)
void get_globals(object_listt &globals)
void simplify(goto_programt &goto_program)
const irep_idt & id() const
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...
invariant_set_domain_factoryt(invariant_propagationt &_ip)
The most conventional storage; one domain per location.
#define Forall_goto_functions(it, functions)
invariant_propagationt & ip
Extract member of struct or union.
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
A collection of goto functions.
invariant_sett invariant_set
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
inv_object_storet object_store
const symbolst & symbols
Read-only field, used to look up symbols given their names.
void simplify(exprt &expr) const
A generic container class for the GOTO intermediate representation of one function.
ai_domain_baset::locationt locationt
#define forall_goto_functions(it, functions)
The Boolean constant true.
std::set< irep_idt > decl_identifierst
void initialize(const irep_idt &function, const goto_programt &goto_program) override
Initialize all the abstract states for a single function.
API to expression classes.
#define forall_goto_program_instructions(it, program)