Commit 0e2c6aef authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix specification of the sign of FP result in presence of NaNs.

parent c51200a4
...@@ -481,7 +481,7 @@ theory GenFloatSpecFull ...@@ -481,7 +481,7 @@ theory GenFloatSpecFull
-> is_finite r /\ value r = round m (value x * value y)) -> is_finite r /\ value r = round m (value x * value y))
/\ (is_finite x /\ is_finite y /\ not no_overflow m (value x * value y) /\ (is_finite x /\ is_finite y /\ not no_overflow m (value x * value y)
-> overflow_value m r) -> overflow_value m r)
/\ product_sign r x y /\ (not is_NaN r -> product_sign r x y)
/\ exact r = exact x * exact y /\ exact r = exact x * exact y
/\ model r = model x * model y /\ model r = model x * model y
...@@ -489,7 +489,7 @@ theory GenFloatSpecFull ...@@ -489,7 +489,7 @@ theory GenFloatSpecFull
(is_NaN x -> is_NaN r) (is_NaN x -> is_NaN r)
/\ (is_infinite x -> is_infinite r) /\ (is_infinite x -> is_infinite r)
/\ (is_finite x -> is_finite r /\ value r = - value x) /\ (is_finite x -> is_finite r /\ value r = - value x)
/\ diff_sign r x /\ (not is_NaN r -> diff_sign r x)
/\ exact r = - exact x /\ exact r = - exact x
/\ model r = - model x /\ model r = - model x
...@@ -508,7 +508,7 @@ theory GenFloatSpecFull ...@@ -508,7 +508,7 @@ theory GenFloatSpecFull
/\ (is_finite x /\ is_gen_zero y /\ value x <> 0.0 /\ (is_finite x /\ is_gen_zero y /\ value x <> 0.0
-> is_infinite r) -> is_infinite r)
/\(is_gen_zero x /\ is_gen_zero y -> is_NaN r) /\(is_gen_zero x /\ is_gen_zero y -> is_NaN r)
/\ product_sign r x y /\ (not is_NaN r -> product_sign r x y)
/\ exact r = exact x / exact y /\ exact r = exact x / exact y
/\ model r = model x / model y /\ model r = model x / model y
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment