From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 23 Jul 2014 08:54:56 +0000
Subject: Merge of "newspilling" branch: - Support single-precision floats as
 first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64
 to   support saving and restoring registers without knowing   the exact types
 (int/single/float) of their contents, just   their sizes. - Memory model:
 generalize the opaque encoding of pointers to   apply to any value, not just
 pointers, if chunks Many32/Many64   are selected. - More properties of FP
 arithmetic proved.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Cexec.v | 19 +++++--------------
 1 file changed, 5 insertions(+), 14 deletions(-)

(limited to 'cfrontend/Cexec.v')

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index b41902c9..eea1997e 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -104,7 +104,7 @@ Definition eventval_of_val (v: val) (t: typ) : option eventval :=
   match v, t with
   | Vint i, AST.Tint => Some (EVint i)
   | Vfloat f, AST.Tfloat => Some (EVfloat f)
-  | Vfloat f, AST.Tsingle => if Float.is_single_dec f then Some (EVfloatsingle f) else None
+  | Vsingle f, AST.Tsingle => Some (EVsingle f)
   | Vlong n, AST.Tlong => Some (EVlong n)
   | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol ge b; Some (EVptr_global id ofs)
   | _, _ => None
@@ -124,7 +124,7 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
   match ev, t with
   | EVint i, AST.Tint => Some (Vint i)
   | EVfloat f, AST.Tfloat => Some (Vfloat f)
-  | EVfloatsingle f, AST.Tsingle => if Float.is_single_dec f then Some (Vfloat f) else None
+  | EVsingle f, AST.Tsingle => Some (Vsingle f)
   | EVlong n, AST.Tlong => Some (Vlong n)
   | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol ge id; Some (Vptr b ofs)
   | _, _ => None
@@ -133,11 +133,7 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
 Lemma eventval_of_val_sound:
   forall v t ev, eventval_of_val v t = Some ev -> eventval_match ge ev t v.
 Proof.
-  intros. destruct v; destruct t; simpl in H; inv H.
-  constructor.
-  constructor.
-  constructor.
-  destruct (Float.is_single_dec f); inv H1. constructor; auto.
+  intros. destruct v; destruct t; simpl in H; inv H; try constructor.
   destruct (Genv.invert_symbol ge b) as [id|] eqn:?; inv H1. 
   constructor. apply Genv.invert_find_symbol; auto.
 Qed.
@@ -146,7 +142,6 @@ Lemma eventval_of_val_complete:
   forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev.
 Proof.
   induction 1; simpl; auto.
-  rewrite pred_dec_true; auto.
   rewrite (Genv.find_invert_symbol _ _ H). auto. 
 Qed.
 
@@ -170,11 +165,7 @@ Qed.
 Lemma val_of_eventval_sound:
   forall ev t v, val_of_eventval ev t = Some v -> eventval_match ge ev t v.
 Proof.
-  intros. destruct ev; destruct t; simpl in H; inv H.
-  constructor.
-  constructor.
-  constructor.
-  destruct (Float.is_single_dec f); inv H1. constructor; auto.
+  intros. destruct ev; destruct t; simpl in H; inv H; try constructor.
   destruct (Genv.find_symbol ge i) as [b|] eqn:?; inv H1.
   constructor. auto.
 Qed.
@@ -182,7 +173,7 @@ Qed.
 Lemma val_of_eventval_complete:
   forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v.
 Proof.
-  induction 1; simpl; auto. rewrite pred_dec_true; auto. rewrite H; auto.
+  induction 1; simpl; auto. rewrite H; auto.
 Qed.
 
 (** Volatile memory accesses. *)
-- 
cgit