Commit 8a64fbf4 authored by Heiko Becker's avatar Heiko Becker

WIP:Fix broken FP range calculation

parent 6bc1a0dd
......@@ -354,7 +354,7 @@ Fixed-Points:
**)
Definition maxValue (m:mType) :=
match m with
|F w f => ((Z.pow_pos 2 (w -1))-1) * (Z.pow_pos 2 (maxExponent m)) # 1
|F w f => (((Z.pow_pos 2 (w -1))-1)#1) * Qinv ((Z.pow_pos 2 (maxExponent m))#1)
|_ => (Z.pow_pos 2 (maxExponent m)) # 1
end.
......
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