Go to the documentation of this file.
22 state.second.invariant_set.make_true();
28 state.second.invariant_set.make_false();
43 typedef std::unordered_map<irep_idt, object_listt> object_cachet;
44 object_cachet object_cache;
51 is.add_objects(globals);
54 for(
const auto &local : locals)
57 object_cachet::const_iterator e_it=object_cache.find(local);
59 if(e_it==object_cache.end())
66 is.add_objects(objects);
71 is.add_objects(e_it->second);
81 std::list<exprt> object_list;
85 for(
const auto &expr : object_list)
91 std::list<exprt> &dest)
95 if(t.
id()==ID_struct ||
108 else if(t.
id()==ID_array)
129 std::set<irep_idt> locals;
135 typedef std::unordered_map<irep_idt, object_listt> object_cachet;
136 object_cachet object_cache;
143 is.add_objects(globals);
146 for(
const auto &local : locals)
149 object_cachet::const_iterator e_it=object_cache.find(local);
151 if(e_it==object_cache.end())
158 is.add_objects(objects);
163 is.add_objects(e_it->second);
176 if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
185 if(type.
id()==ID_pointer)
187 else if(type.
id()==ID_struct ||
190 else if(type.
id()==ID_array)
192 else if(type.
id() == ID_symbol_type)
194 else if(type.
id()==ID_unsignedbv ||
195 type.
id()==ID_signedbv)
197 else if(type.
id()==ID_bool)
242 if(!i_it->is_assert())
246 const auto &d = (*this)[i_it];
252 exprt simplified_guard(i_it->guard);
254 invariant_set.
simplify(simplified_guard);
#define Forall_goto_program_instructions(it, program)
const componentst & components() const
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
tvt implies(const exprt &expr) const
std::list< unsigned > object_listt
The type of an expression, extends irept.
Base class for all expressions.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
void set_namespace(const namespacet &_ns)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
void get_objects(const symbolt &symbol, object_listt &dest)
void set_value_sets(value_setst &_value_sets)
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.
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...
#define Forall_goto_functions(it, functions)
Extract member of struct or union.
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Structure type, corresponds to C style structs.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
inv_object_storet object_store
void simplify(exprt &expr) const
A generic container class for the GOTO intermediate representation of one function.
#define forall_goto_functions(it, functions)
void set_object_store(inv_object_storet &_object_store)
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
The Boolean constant true.
std::set< irep_idt > decl_identifierst
#define forall_goto_program_instructions(it, program)