Commit 2149fe69 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix specification for FP neg and sqrt.

parent 22408364
......@@ -490,7 +490,7 @@ theory GenFloatSpecFull
(is_NaN x -> is_NaN r)
/\ (is_infinite x -> is_infinite r)
/\ (is_finite x -> is_finite r /\ value r = - value x)
/\ diff_sign r x
/\ (not is_NaN x -> diff_sign r x)
/\ exact r = - exact x
/\ model r = - model x
......@@ -549,7 +549,7 @@ theory GenFloatSpecFull
predicate sqrt_post (m:mode) (x:t) (r:t) =
(is_NaN x -> is_NaN r)
/\ (is_plus_infinity x -> is_plus_infinity x)
/\ (is_plus_infinity x -> is_plus_infinity r)
/\ (is_minus_infinity x -> is_NaN r)
/\ (is_finite x /\ value x < 0.0 -> is_NaN r)
/\ (is_finite x /\ value x = 0.0
......
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