85 shared_varst::const_iterator v_it =
shared_vars.find(s.get_identifier());
96 replace_symbol.
insert(s, new_expr);
104 for(goto_programt::instructionst::iterator
113 else if(it->is_assume() || it->is_assert() || it->is_goto())
117 else if(it->is_function_call())
145 thread_local_var.
type = symbol.
type;
164 if(is_threaded(i_it))
182 collect(gf_entry.second.body, is_threaded);
codet representation of a function call statement.
optionalt< symbol_exprt > array_symbol
optionalt< symbol_exprt > w_index_symbol
optionalt< symbol_exprt > array_symbol
void collect(const goto_programt &goto_program, const is_threadedt &is_threaded)
void operator()(goto_functionst &goto_functions)
concurrency_instrumentationt(value_setst &_value_sets, symbol_tablet &_symbol_table)
std::map< irep_idt, thread_local_vart > thread_local_varst
thread_local_varst thread_local_vars
void instrument(goto_functionst &goto_functions)
symbol_tablet & symbol_table
std::map< irep_idt, shared_vart > shared_varst
Base class for all expressions.
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
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().
Replace expression or type symbols by an expression or type, respectively.
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...
Expression to hold a symbol (variable)
typet type
Type of symbol.
The type of an expression, extends irept.
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Encoding for Threaded Goto Programs.
void find_symbols(const exprt &src, find_symbols_sett &dest, bool current, bool next)
Add to the set dest the sub-expressions of src with id ID_symbol if current is true,...
std::unordered_set< irep_idt > find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol.
const code_function_callt & to_code_function_call(const codet &code)
#define forall_goto_program_instructions(it, program)
Over-approximate Concurrency for Threaded Goto Programs.
nonstd::optional< T > optionalt
API to expression classes.