From 7998ccfd709b97f1a2306df4570365d58a5bb4b5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 12 Jan 2014 10:48:56 +0000 Subject: - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4. - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asm.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/Asm.v') diff --git a/arm/Asm.v b/arm/Asm.v index 76e81962..69f6319e 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -615,11 +615,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfcvtsd r1 r2 => Next (nextinstr (rs#r1 <- (Val.singleoffloat rs#r2))) m | Pfldd r1 r2 n => - exec_load Mfloat64al32 (Val.add rs#r2 (Vint n)) r1 rs m + exec_load Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m | Pflds r1 r2 n => exec_load Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m | Pfstd r1 r2 n => - exec_store Mfloat64al32 (Val.add rs#r2 (Vint n)) r1 rs m + exec_store Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m | Pfsts r1 r2 n => match exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m with | Next rs' m' => Next (rs'#FR6 <- Vundef) m' -- cgit