diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-08-02 08:05:18 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-08-02 08:05:18 +0000 |
commit | 4ee0544a157090ddd087b36109d292cd174bae7c (patch) | |
tree | 3282bd6a14816239268e14bb40f2f09217c45456 /powerpc/Nan.v | |
parent | b5da812fdc8db859d816cb2fc85e367569a38bed (diff) | |
download | compcert-4ee0544a157090ddd087b36109d292cd174bae7c.tar.gz compcert-4ee0544a157090ddd087b36109d292cd174bae7c.zip |
Merge of Flocq version 2.2.0.
More precise modeling of NaNs.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/Nan.v')
-rw-r--r-- | powerpc/Nan.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/powerpc/Nan.v b/powerpc/Nan.v new file mode 100644 index 00000000..77a752e9 --- /dev/null +++ b/powerpc/Nan.v @@ -0,0 +1,28 @@ +Require Import Fappli_IEEE. +Require Import Fappli_IEEE_bits. +Require Import Floats. +Require Import ZArith. +Require Import Integers. + +(* Needed to break a circular reference after extraction *) +Definition transform_quiet_pl := + Eval unfold Float.transform_quiet_pl in Float.transform_quiet_pl. + +Program Definition default_pl : bool * nan_pl 53 := (false, nat_iter 51 xO xH). + +Definition binop_pl (pl1 pl2:binary64) : bool*nan_pl 53 := + match pl1, pl2 with + | B754_nan s1 pl1, _ => (s1, transform_quiet_pl pl1) + | _, B754_nan s2 pl2 => (s2, transform_quiet_pl pl2) + | _, _ => default_pl + end. + +Theorem binop_propagate1: Float.binop_propagate1_prop binop_pl. +Proof. + repeat intro. destruct f1, f2; try discriminate; reflexivity. +Qed. + +Theorem binop_propagate2: Float.binop_propagate2_prop binop_pl. +Proof. + repeat intro. destruct f1, f2, f3; try discriminate; simpl; reflexivity. +Qed. |