mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-27 12:52:52 +03:00
Added single_to_double for floating point operations
This commit is contained in:
parent
e4d3942094
commit
e1963bcbf2
@ -518,6 +518,9 @@ floatingPointTH bvi fnName args =
|
||||
"round_single" -> do
|
||||
fpval <- addEltTH bvi a
|
||||
liftQ [| addExpr (AppExpr (M.FPCvt M.DoubleFloatRepr $(return fpval) M.SingleFloatRepr)) |]
|
||||
"single_to_double" -> do
|
||||
fpval <- addEltTH bvi a
|
||||
liftQ [| addExpr (AppExpr (M.FPCvt M.SingleFloatRepr $(return fpval) M.DoubleFloatRepr)) |]
|
||||
"abs" -> do
|
||||
-- Note that fabs is only defined for doubles; the operation is the
|
||||
-- same for single and double precision on PPC, so there is only a
|
||||
|
Loading…
Reference in New Issue
Block a user