diff options
Diffstat (limited to 'x86/Asm.v')
| -rw-r--r-- | x86/Asm.v | 12 |
1 files changed, 6 insertions, 6 deletions
@@ -442,8 +442,8 @@ Definition compare_longs (x y: val) (rs: regset) (m: mem): regset := #PF <- Vundef. (** Floating-point comparison between x and y: -- ZF = 1 if x=y or unordered, 0 if x<>y -- CF = 1 if x<y or unordered, 0 if x>=y +- ZF = 1 if x=y or unordered, 0 if x<>y and ordered +- CF = 1 if x<y or unordered, 0 if x>=y. - PF = 1 if unordered, 0 if ordered. - SF and 0F are undefined *) @@ -451,9 +451,9 @@ Definition compare_longs (x y: val) (rs: regset) (m: mem): regset := Definition compare_floats (vx vy: val) (rs: regset) : regset := match vx, vy with | Vfloat x, Vfloat y => - rs #ZF <- (Val.of_bool (negb (Float.cmp Cne x y))) + rs #ZF <- (Val.of_bool (Float.cmp Ceq x y || negb (Float.ordered x y))) #CF <- (Val.of_bool (negb (Float.cmp Cge x y))) - #PF <- (Val.of_bool (negb (Float.cmp Ceq x y || Float.cmp Clt x y || Float.cmp Cgt x y))) + #PF <- (Val.of_bool (negb (Float.ordered x y))) #SF <- Vundef #OF <- Vundef | _, _ => @@ -463,9 +463,9 @@ Definition compare_floats (vx vy: val) (rs: regset) : regset := Definition compare_floats32 (vx vy: val) (rs: regset) : regset := match vx, vy with | Vsingle x, Vsingle y => - rs #ZF <- (Val.of_bool (negb (Float32.cmp Cne x y))) + rs #ZF <- (Val.of_bool (Float32.cmp Ceq x y || negb (Float32.ordered x y))) #CF <- (Val.of_bool (negb (Float32.cmp Cge x y))) - #PF <- (Val.of_bool (negb (Float32.cmp Ceq x y || Float32.cmp Clt x y || Float32.cmp Cgt x y))) + #PF <- (Val.of_bool (negb (Float32.ordered x y))) #SF <- Vundef #OF <- Vundef | _, _ => |