diff options
Diffstat (limited to 'ia32/SelectOp.vp')
| -rw-r--r-- | ia32/SelectOp.vp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 7f79a4f..2d1ab48 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -423,14 +423,14 @@ Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). Definition intuoffloat (e: expr) := Elet e (Elet (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil) - (Econdition (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil) + (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. Definition floatofintu (e: expr) := let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in Elet e - (Econdition (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil) + (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil)) (floatofint (Eletvar O)) (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)). |