diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 13:32:14 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 13:32:14 +0000 |
| commit | 582eeac94b777f99b28a2b373c8e1c825763cada (patch) | |
| tree | 40fea1edf1ef7abe7e4001bbf3ab88d96ce822ed /ia32 | |
| parent | 473454765a4009f5a8ee45ccff728b53c33982bc (diff) | |
Update with _a memory accesses
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2542 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/PrintAsm.ml | 4 |
1 files 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 |