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;