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(
89 shared_buffers.assignment(
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(
132 shared_buffers.assignment(
134 shared_buffers.assignment(
138 original_instruction.
code.
op1());
143 i_it->make_atomic_end();
144 i_it->location=location;
targett insert_before(const_targett target)
Insertion before the given target.
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
::goto_functiont goto_functiont
The boolean constant false.
A generic container class for the GOTO intermediate representation of one function.
static irep_idt entry_point()
#define Forall_goto_functions(it, functions)
void swap(instructiont &instruction)
Swap two instructions.
goto_programt & goto_program
#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.