diff options
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. |