diff options
Diffstat (limited to 'cfrontend/Cshmgen.v')
| -rw-r--r-- | cfrontend/Cshmgen.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 3ab286e4..c45e0946 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -92,6 +92,8 @@ Definition make_cmp_ne_zero (e: expr) := | Ebinop (Ocmp c) e1 e2 => e | Ebinop (Ocmpu c) e1 e2 => e | Ebinop (Ocmpf c) e1 e2 => e + | Ebinop (Ocmpl c) e1 e2 => e + | Ebinop (Ocmplu c) e1 e2 => e | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero) end. |