diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index 9a8415af15..545d389459 100644 --- a/herd/AArch64Sem.ml +++ b/herd/AArch64Sem.ml @@ -2701,19 +2701,15 @@ module Make * overwrite another. By convention, those are * instructions pointed to by "exported" labels. *) - let get_overwriting_instrs lbls test = + let get_overwriting_instrs test = let init_instrs = AArch64.state_fold (fun _ v k -> match v with | V.Val (Constant.Instruction i) -> i::k | _ -> k) - test.Test_herd.init_state [] - and code_instrs = - List.map - (fun (_,i) -> i) - (AArch64.from_labels lbls test.Test_herd.nice_prog) in - init_instrs@code_instrs + test.Test_herd.init_state [] in + init_instrs (* Test all possible instructions, when appropriate *) @@ -2734,15 +2730,9 @@ module Make | Some hd -> let insts = InstrSet.of_list - (get_overwriting_instrs lbls test) in + (get_overwriting_instrs test) in let insts = InstrSet.add inst (InstrSet.filter AArch64.can_overwrite insts) in - if false then - Printf.eprintf "%s: {%s}\n%!" - (Label.pp hd) - (String.concat "," - (List.map AArch64.V.Cst.Instr.pp - (InstrSet.elements insts))) ; (* Shadow default control sequencing operator *) let(>>*=) = M.bind_control_set_data_input_first in let a_v = make_label_value ii.A.fetch_proc hd in