22 state.second.invariant_set.make_true();
28 state.second.invariant_set.make_false();
43 typedef std::unordered_map<irep_idt, object_listt, irep_id_hash>
45 object_cachet object_cache;
52 is.add_objects(globals);
55 for(
const auto &local : locals)
58 object_cachet::const_iterator e_it=object_cache.find(local);
60 if(e_it==object_cache.end())
67 is.add_objects(objects);
72 is.add_objects(e_it->second);
82 std::list<exprt> object_list;
86 for(
const auto &expr : object_list)
92 std::list<exprt> &dest)
96 if(t.
id()==ID_struct ||
103 exprt member_expr(ID_member);
106 for(
const auto &component : c)
108 member_expr.
set(ID_component_name, component.get_name());
109 member_expr.
type()=component.type();
114 else if(t.
id()==ID_array)
135 std::set<irep_idt> locals;
141 typedef std::unordered_map<irep_idt, object_listt, irep_id_hash>
143 object_cachet object_cache;
150 is.add_objects(globals);
153 for(
const auto &local : locals)
156 object_cachet::const_iterator e_it=object_cache.find(local);
158 if(e_it==object_cache.end())
165 is.add_objects(objects);
170 is.add_objects(e_it->second);
182 if(it->second.is_lvalue &&
183 it->second.is_static_lifetime)
189 if(type.
id()==ID_pointer)
191 else if(type.
id()==ID_struct ||
194 else if(type.
id()==ID_array)
196 else if(type.
id()==ID_symbol)
198 else if(type.
id()==ID_unsignedbv ||
199 type.
id()==ID_signedbv)
201 else if(type.
id()==ID_bool)
246 if(!i_it->is_assert())
250 state_mapt::const_iterator s_it=
state_map.find(i_it);
256 exprt simplified_guard(i_it->guard);
258 invariant_set.
simplify(simplified_guard);
The type of an expression.
const typet & follow(const typet &src) const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
std::list< unsigned > object_listt
#define forall_symbols(it, expr)
const symbol_tablet & get_symbol_table() const
instructionst instructions
The list of instructions in the goto program.
void copy_to_operands(const exprt &expr)
void get_local_identifiers(const goto_function_templatet< goto_programt > &goto_function, std::set< irep_idt > &dest)
std::vector< componentt > componentst
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)
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)
API to expression classes.
void get_globals(object_listt &globals)
unsigned add(const exprt &expr)
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
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 &)
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)
void set(const irep_namet &name, const irep_idt &value)
void set_namespace(const namespacet &_ns)