52 goto_programt::instructiont &instruction=*i_it;
54 if(instruction.is_assign())
66 goto_programt::instructiont original_instruction;
67 original_instruction.swap(instruction);
68 const locationt &location=original_instruction.location;
70 instruction.make_atomic_begin();
71 instruction.location=location;
76 forall_rw_set_entries(e_it, rw_set)
80 shared_buffers(e_it->second.object);
81 irep_idt choice0=shared_buffers.choice(
"0");
82 irep_idt choice1=shared_buffers.choice(
"1");
99 shared_buffers.assignment(
100 goto_program, i_it, location, choice0, choice0_rhs);
101 shared_buffers.assignment(
102 goto_program, i_it, location, choice1, choice1_rhs);
107 if_exprt(choice0_expr, w_buff0_expr,
108 if_exprt(choice1_expr, w_buff1_expr, lhs));
111 shared_buffers.assignment(
112 goto_program, i_it, location, e_it->second.object, value);
124 shared_buffers.assignment(
125 goto_program, i_it, location, vars.w_used0, w_used0_rhs);
126 shared_buffers.assignment(
127 goto_program, i_it, location, vars.w_used1, w_used1_rhs);
131 forall_rw_set_entries(e_it, rw_set)
135 shared_buffers(e_it->second.object);
138 shared_buffers.assignment(
139 goto_program, i_it, location, vars.w_used1, vars.w_used0);
140 shared_buffers.assignment(
141 goto_program, i_it, location, vars.w_used0,
true_exprt());
144 shared_buffers.assignment(
146 shared_buffers.assignment(
150 original_instruction.code.op1());
154 i_it=goto_program.insert_before(i_it);
155 i_it->make_atomic_end();
156 i_it->location=location;
179 mmio(value_sets, symbol_table,
Goto Programs with Functions.
The trinary if-then-else operator.
void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program)
The boolean constant true.
static irep_idt entry_point()
API to expression classes.
goto_function_templatet< goto_programt > goto_functiont
The boolean constant false.
Interrupt Instrumentation for Goto Programs.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Base class for all expressions.
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
Memory-mapped I/O Instrumentation for Goto Programs.
Field-insensitive, location-sensitive may-alias analysis.
Race Detection for Threaded Goto Programs.