From 582eeac94b777f99b28a2b373c8e1c825763cada Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 13:32:14 +0000 Subject: Update with _a memory accesses git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2542 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/PrintAsm.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 67fb80c..d30c856 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -571,9 +571,9 @@ let print_instruction oc = function let lbl = new_label() in fprintf oc " movsd %a, %a %s %.18g\n" label lbl freg rd comment (camlfloat_of_coqfloat n); float64_literals := (lbl, b) :: !float64_literals - | Pmovsd_fm(rd, a) -> + | Pmovsd_fm(rd, a) | Pmovsd_fm_a(rd, a) -> fprintf oc " movsd %a, %a\n" addressing a freg rd - | Pmovsd_mf(a, r1) -> + | Pmovsd_mf(a, r1) | Pmovsd_mf_a(a, r1) -> fprintf oc " movsd %a, %a\n" freg r1 addressing a | Pmovss_fi(rd, n) -> let b = camlint_of_coqint (Floats.Float32.to_bits n) in -- cgit v1.2.3