Go to the documentation of this file.
80 std::set<exprt> symbols;
86 for(std::set<exprt>::const_iterator
91 if(s_it->id()==ID_symbol)
106 replace_symbol.
insert(s, new_expr);
115 for(goto_programt::instructionst::iterator
125 else if(it->is_assume() || it->is_assert() || it->is_goto())
127 else if(it->is_function_call())
141 std::set<exprt> symbols;
145 for(std::set<exprt>::const_iterator
146 s_it=symbols.begin();
150 if(s_it->id()==ID_symbol)
187 if(is_threaded(i_it))
189 if(i_it->is_assign())
191 else if(i_it->is_assume() || i_it->is_assert() || i_it->is_goto())
193 else if(i_it->is_function_call())
212 collect(f_it->second.body, is_threaded);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
thread_local_varst thread_local_vars
std::map< irep_idt, shared_vart > shared_varst
symbol_exprt w_index_symbol
The type of an expression, extends irept.
typet type
Type of symbol.
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Base class for all expressions.
void collect(const goto_programt &goto_program, const is_threadedt &is_threaded)
Expression to hold a symbol (variable)
void operator()(goto_functionst &goto_functions)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
void find_symbols(const exprt &src, find_symbols_sett &dest)
void instrument(goto_functionst &goto_functions)
symbol_tablet & symbol_table
const irep_idt & get_identifier() const
concurrency_instrumentationt(value_setst &_value_sets, symbol_tablet &_symbol_table)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
symbol_exprt array_symbol
const code_function_callt & to_code_function_call(const codet &code)
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
#define Forall_goto_functions(it, functions)
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
const code_assignt & to_code_assign(const codet &code)
symbol_exprt array_symbol
std::map< irep_idt, thread_local_vart > thread_local_varst
A generic container class for the GOTO intermediate representation of one function.
#define forall_goto_functions(it, functions)
A codet representing an assignment in the program.
symbol_tablet symbol_table
Symbol table.
#define forall_goto_program_instructions(it, program)
Replace expression or type symbols by an expression or type, respectively.