diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 09:51:23 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 09:51:23 +0000 |
| commit | e4585d1b9523c174c75518546513e8184587639d (patch) | |
| tree | 5d420b18233d4a327f482f670519631a04e2f2c4 /cfrontend/Csem.v | |
| parent | d71a5cfd10378301b71d32659d5936e01d72ae50 (diff) | |
| download | compcert-kvx-e4585d1b9523c174c75518546513e8184587639d.tar.gz compcert-kvx-e4585d1b9523c174c75518546513e8184587639d.zip | |
Suppressed axioms Float.eq_zero_{true,false}, since the latter is
wrong because of +0.0 / -0.0.
Adapted Clight semantics accordingly. (Truth value of a float is
defined by comparison Float.cmp Ceq with 0.0, no longer by structural
equality.)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Csem.v')
| -rw-r--r-- | cfrontend/Csem.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 6e35c2f0..5f8bbf14 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -40,8 +40,9 @@ Inductive is_false: val -> type -> Prop := is_false (Vint Int.zero) (Tint sz sg) | is_false_pointer: forall t, is_false (Vint Int.zero) (Tpointer t) - | is_false_float: forall sz, - is_false (Vfloat Float.zero) (Tfloat sz). + | is_false_float: forall sz f, + Float.cmp Ceq f Float.zero = true -> + is_false (Vfloat f) (Tfloat sz). Inductive is_true: val -> type -> Prop := | is_true_int_int: forall n sz sg, @@ -55,7 +56,7 @@ Inductive is_true: val -> type -> Prop := | is_true_pointer_pointer: forall b ofs t, is_true (Vptr b ofs) (Tpointer t) | is_true_float: forall f sz, - f <> Float.zero -> + Float.cmp Ceq f Float.zero = false -> is_true (Vfloat f) (Tfloat sz). Inductive bool_of_val : val -> type -> val -> Prop := |