File tree Expand file tree Collapse file tree 3 files changed +2
-6
lines changed
Expand file tree Collapse file tree 3 files changed +2
-6
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
Original file line number Diff line number Diff line change @@ -116,7 +116,7 @@ module Make(O:Config)(I:I) : S with module I = I
116116 let tr_global (c :ParsedConstant.v ) =
117117 let open Constant in
118118 match c with
119- | Symbolic sym when not (is_label c) -> Global_litmus. get_base_symbol sym
119+ | Symbolic sym when not (is_label c) -> Global_litmus. tr_symbol sym
120120 | Symbolic _| Tag _| Concrete _| ConcreteVector _| ConcreteRecord _
121121 | PteVal _| AddrReg _| Instruction _
122122 | Frozen _
You can’t perform that action at this time.
0 commit comments