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 ||
100 for(
const auto &component : struct_type.
components())
103 src, component.get_name(), component.
type());
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)
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);
The type of an expression.
std::list< unsigned > object_listt
const symbol_tablet & get_symbol_table() const
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
void get_objects(const symbolt &symbol, object_listt &dest)
const componentst & components() const
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
Extract member of struct or union.
bool check_type(const typet &type) const
tvt implies(const exprt &expr) const
std::set< irep_idt > decl_identifierst
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
virtual void initialize(const goto_programt &goto_program)
The boolean constant true.
void add_objects(const goto_programt &goto_program)
void set_value_sets(value_setst &_value_sets)
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
void get_globals(object_listt &globals)
unsigned add(const exprt &expr)
const typet & follow(const typet &) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
A generic container class for the GOTO intermediate representation of one function.
void simplify(exprt &expr) const
void set_object_store(inv_object_storet &_object_store)
void simplify(goto_programt &goto_program)
Base class for all expressions.
#define Forall_goto_functions(it, functions)
virtual void initialize(const goto_programt &)
goto_programt & goto_program
inv_object_storet object_store
#define Forall_goto_program_instructions(it, program)
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void set_namespace(const namespacet &_ns)