Commit 85715001 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add missing rounding modes to Gappa output.

This fixes the following assertion failure:
anomaly: File "src/printer/gappa.ml", line 182, characters 19-25: Assertion failed
parent a8fe9a2b
......@@ -128,12 +128,20 @@ end
theory floating_point.Single
prelude "@rnd_ieee32_ne=float<ieee_32,ne>;"
prelude "@rnd_ieee32_zr=float<ieee_32,zr>;"
prelude "@rnd_ieee32_up=float<ieee_32,up>;"
prelude "@rnd_ieee32_dn=float<ieee_32,dn>;"
prelude "@rnd_ieee32_na=float<ieee_32,na>;"
end
theory floating_point.Double
prelude "@rnd_ieee64_ne=float<ieee_64,ne>;"
prelude "@rnd_ieee64_zr=float<ieee_64,zr>;"
prelude "@rnd_ieee64_up=float<ieee_64,up>;"
prelude "@rnd_ieee64_dn=float<ieee_64,dn>;"
prelude "@rnd_ieee64_na=float<ieee_64,na>;"
end
......
......@@ -86,6 +86,10 @@ let get_info =
let real_sqrt = find_real_square "sqrt" in
let find_rounding_theory = find_th env "floating_point" "Rounding" in
let round_ne = find_rounding_theory "NearestTiesToEven" in
let round_zr = find_rounding_theory "ToZero" in
let round_up = find_rounding_theory "Up" in
let round_dn = find_rounding_theory "Down" in
let round_na = find_rounding_theory "NearTiesToAway" in
let find_single_theory = find_th env "floating_point" "Single" in
round_single := find_single_theory "round";
let find_double_theory = find_th env "floating_point" "Double" in
......@@ -124,7 +128,11 @@ let get_info =
List.fold_left
(fun acc (ls,s) -> Mls.add ls s acc)
Mls.empty
[ round_ne,"ne" ;
[ round_ne, "ne" ;
round_zr, "zr" ;
round_up, "up" ;
round_dn, "dn" ;
round_na, "na" ;
];
(*
inline :=
......
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