IA32 port: more faithful treatment of pseudoregister ST0.

Related general change: support for destroyed_at_moves.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1700 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 2 insertions, 2 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 1870d69..2eb6a8d 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -437,7 +437,7 @@ Definition exec_load (chunk: memory_chunk) (m: mem)
 Definition exec_store (chunk: memory_chunk) (m: mem)
                       (a: addrmode) (rs: regset) (r1: preg) :=
   match Mem.storev chunk m (eval_addrmode a rs) (rs r1) with
-  | Some m' => Next (nextinstr_nf rs) m'
+  | Some m' => Next (nextinstr_nf (if preg_eq r1 ST0 then rs#ST0 <- Vundef else rs)) m'
   | None => Stuck
   end.
 
@@ -488,7 +488,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Pfld_m a =>
       exec_load Mfloat64 m a rs ST0
   | Pfstp_f rd =>
-      Next (nextinstr (rs#rd <- (rs ST0))) m
+      Next (nextinstr (rs#rd <- (rs ST0) #ST0 <- Vundef)) m
   | Pfstp_m a =>
       exec_store Mfloat64 m a rs ST0
   (** Moves with conversion *)