55 original_instruction.
swap(instruction);
56 const locationt &location=original_instruction.location;
59 instruction.location=location;
64 forall_rw_set_entries(e_it, rw_set)
68 shared_buffers(e_it->second.object);
69 irep_idt choice0=shared_buffers.choice(
"0");
70 irep_idt choice1=shared_buffers.choice(
"1");
81 const side_effect_nondet_exprt nondet_bool_expr(
bool_typet());
83 const and_exprt choice0_rhs(nondet_bool_expr, w_used0_expr);
84 const and_exprt choice1_rhs(nondet_bool_expr, w_used1_expr);
87 shared_buffers.assignment(
88 goto_program, i_it, location, choice0, choice0_rhs);
89 shared_buffers.assignment(
90 goto_program, i_it, location, choice1, choice1_rhs);
97 if_exprt(choice1_expr, w_buff1_expr, lhs));
100 shared_buffers.assignment(
101 goto_program, i_it, location, e_it->second.object, value);
112 shared_buffers.assignment(
113 goto_program, i_it, location, vars.w_used0, w_used0_rhs);
114 shared_buffers.assignment(
115 goto_program, i_it, location, vars.w_used1, w_used1_rhs);
119 forall_rw_set_entries(e_it, rw_set)
123 shared_buffers(e_it->second.object);
126 shared_buffers.assignment(
127 goto_program, i_it, location, vars.w_used1, vars.w_used0);
128 shared_buffers.assignment(
129 goto_program, i_it, location, vars.w_used0,
true_exprt());
132 shared_buffers.assignment(
134 shared_buffers.assignment(
138 original_instruction.
code.
op1());
142 i_it=goto_program.insert_before(i_it);
143 i_it->make_atomic_end();
144 i_it->location=location;
The trinary if-then-else operator.
void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program)
symbol_tablet symbol_table
Symbol table.
This class represents an instruction in the GOTO intermediate representation.
The Boolean constant true.
#define INITIALIZE_FUNCTION
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
The Boolean constant false.
A generic container class for the GOTO intermediate representation of one function.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
#define Forall_goto_functions(it, functions)
void swap(instructiont &instruction)
Swap two instructions.
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
Memory-mapped I/O Instrumentation for Goto Programs.
goto_functionst goto_functions
GOTO functions.
Field-insensitive, location-sensitive may-alias analysis.
Race Detection for Threaded Goto Programs.