diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-31 09:38:19 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-31 09:38:19 +0000 |
commit | 2079efb2b129e3d00a51b2ed9febef2619742201 (patch) | |
tree | c00f9cd5d36fe00c1f787424c29ab0ee93ec5953 | |
parent | 603e931f49ef04188a58895ce38d892511b75b78 (diff) |
Check fcmpd semantics
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1694 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r-- | arm/Asm.v | 29 |
1 files changed, 19 insertions, 10 deletions
@@ -369,19 +369,28 @@ Definition compare_int (rs: regset) (v1 v2: val) := #CRgt <- (Val.cmp Cgt v1 v2) #CRle <- (Val.cmp Cle v1 v2). +(** Semantics of [fcmpd] instruction: +<< +== EQ=1 NE=0 HS=1 LO=0 MI=0 PL=1 VS=0 VC=1 HI=0 LS=1 GE=1 LT=0 GT=0 LE=1 +< EQ=0 NE=1 HS=0 LO=1 MI=1 PL=0 VS=0 VC=1 HI=0 LS=1 GE=0 LT=1 GT=0 LE=1 +> EQ=0 NE=1 HS=1 LO=0 MI=0 PL=1 VS=0 VC=1 HI=1 LS=0 GE=1 LT=0 GT=1 LE=0 +unord EQ=0 NE=1 HS=1 LO=0 MI=0 PL=1 VS=1 VC=0 HI=1 LS=0 GE=0 LT=1 GT=0 LE=1 +>> +*) + Definition compare_float (rs: regset) (v1 v2: val) := rs#CReq <- (Val.cmpf Ceq v1 v2) #CRne <- (Val.cmpf Cne v1 v2) - #CRhs <- Vundef - #CRlo <- Vundef - #CRmi <- (Val.cmpf Clt v1 v2) (* lt *) - #CRpl <- (Val.notbool (Val.cmpf Clt v1 v2)) (* not lt *) - #CRhi <- (Val.notbool (Val.cmpf Cle v1 v2)) (* not le *) - #CRls <- (Val.cmpf Cle v1 v2) (* le *) - #CRge <- (Val.cmpf Cge v1 v2) (* ge *) - #CRlt <- (Val.notbool (Val.cmpf Cge v1 v2)) (* not ge *) - #CRgt <- (Val.cmpf Cgt v1 v2) (* gt *) - #CRle <- (Val.notbool (Val.cmpf Cgt v1 v2)). (* not gt *) + #CRhs <- (Val.notbool (Val.cmpf Clt v1 v2)) (**r not lt *) + #CRlo <- (Val.cmpf Clt v1 v2) (**r lt *) + #CRmi <- (Val.cmpf Clt v1 v2) (**r lt *) + #CRpl <- (Val.notbool (Val.cmpf Clt v1 v2)) (**r not lt *) + #CRhi <- (Val.notbool (Val.cmpf Cle v1 v2)) (**r not le *) + #CRls <- (Val.cmpf Cle v1 v2) (**r le *) + #CRge <- (Val.cmpf Cge v1 v2) (**r ge *) + #CRlt <- (Val.notbool (Val.cmpf Cge v1 v2)) (**r not ge *) + #CRgt <- (Val.cmpf Cgt v1 v2) (**r gt *) + #CRle <- (Val.notbool (Val.cmpf Cgt v1 v2)). (**r not gt *) (** Execution of a single instruction [i] in initial state [rs] and [m]. Return updated state. For instructions |