File tree Expand file tree Collapse file tree 2 files changed +1
-5
lines changed
Expand file tree Collapse file tree 2 files changed +1
-5
lines changed Original file line number Diff line number Diff line change @@ -1374,9 +1374,6 @@ module Make
13741374 fun (r,_) -> M.unitT r
13751375 else m
13761376
1377- let set_elr_el1 v ii =
1378- write_reg AArch64Base.elr_el1 v ii
1379-
13801377 let lift_kvm dir updatedb mop ma an ii mphy =
13811378 let lbl_v = get_instr_label ii in
13821379 let mfault ma a ft =
@@ -3615,7 +3612,6 @@ Arguments:
36153612 >>= do_indirect_jump test [] i ii
36163613
36173614 | I_ERET ->
3618- let open Constant in
36193615 let eret_to_addr v =
36203616 match v2tgt v with
36213617 | Some tgt -> B.faultRetT tgt
Original file line number Diff line number Diff line change @@ -263,7 +263,7 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S =
263263 locs
264264 else
265265 let sym = Constant. mk_sym_virtual s in
266- A. Location_global (A.V. Val sym)::locs
266+ A. Location_global (A.V. Val sym)::locs
267267 | None -> locs
268268 with V. Undetermined -> locs)
269269 init [] in
You can’t perform that action at this time.
0 commit comments