diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-19 15:13:42 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-19 15:13:42 +0000 |
| commit | eb7c8587f462adca878088ef5f610c81734efc70 (patch) | |
| tree | 6771c5be9d0d6048357be99c663ec64981ad63dd /cfrontend/Cshmgen.v | |
| parent | 165407527b1be7df6a376791719321c788e55149 (diff) | |
| download | compcert-kvx-eb7c8587f462adca878088ef5f610c81734efc70.tar.gz compcert-kvx-eb7c8587f462adca878088ef5f610c81734efc70.zip | |
Meilleure compilation de la negation booleenne
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@112 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cshmgen.v')
| -rw-r--r-- | cfrontend/Cshmgen.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index aaec07d8..664c6fc4 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -96,7 +96,10 @@ Definition make_neg (e: expr) (ty: type) := end. Definition make_notbool (e: expr) (ty: type) := - make_binop (Ocmp Ceq) (make_boolean e ty) (make_intconst Int.zero). + match ty with + | Tfloat _ => make_binop (Ocmpf Ceq) e (make_floatconst Float.zero) + | _ => make_unop Onotbool e + end. Definition make_notint (e: expr) (ty: type) := make_unop Onotint e. |