summaryrefslogtreecommitdiff
path: root/cfrontend/Cshmgen.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Cshmgen.v')
-rw-r--r--cfrontend/Cshmgen.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index fd34985..f37e8c7 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -329,6 +329,7 @@ Definition transl_unop (op: Cop.unary_operation) (a: expr) (ta: type) : res expr
| Cop.Onotbool => make_notbool a ta
| Cop.Onotint => make_notint a ta
| Cop.Oneg => make_neg a ta
+ | Cop.Oabsfloat => OK (Eunop Oabsf a)
end.
Definition transl_binop (op: Cop.binary_operation)