Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
36ae057b
Commit
36ae057b
authored
1 year ago
by
Loïc Correnson
Committed by
Maxime Jacquemin
1 year ago
Browse files
Options
Downloads
Patches
Plain Diff
[lib] further cleaning the source
parent
a85a6e7b
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/libraries/utils/floating_point.ml
+41
-26
41 additions, 26 deletions
src/libraries/utils/floating_point.ml
with
41 additions
and
26 deletions
src/libraries/utils/floating_point.ml
+
41
−
26
View file @
36ae057b
...
...
@@ -20,7 +20,9 @@
(* *)
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
(* --- Rounding Modes --- *)
(* -------------------------------------------------------------------------- *)
type
c_rounding_mode
=
FE_ToNearest
|
FE_Upward
|
FE_Downward
|
FE_TowardZero
...
...
@@ -31,9 +33,6 @@ let string_of_c_rounding_mode = function
|
FE_Downward
->
"FE_DOWNWARD"
|
FE_TowardZero
->
"FE_TOWARDZERO"
external
set_round_downward
:
unit
->
unit
=
"set_round_downward"
[
@@
noalloc
]
external
set_round_upward
:
unit
->
unit
=
"set_round_upward"
[
@@
noalloc
]
external
set_round_nearest_even
:
unit
->
unit
=
"set_round_nearest_even"
[
@@
noalloc
]
...
...
@@ -45,11 +44,13 @@ external sys_single_precision_of_string: string -> float = "single_precision_of_
(* TODO two functions above: declare "float",
must have separate version for bytecode, see OCaml manual *)
(* -------------------------------------------------------------------------- *)
(* --- Constructors --- *)
(* -------------------------------------------------------------------------- *)
let
max_single_precision_float
=
Int32
.
float_of_bits
0x7f7fffff
l
let
most_negative_single_precision_float
=
-.
max_single_precision_float
type
parsed_float
=
{
f_nearest
:
float
;
f_lower
:
float
;
f_upper
:
float
}
let
zero
=
{
f_lower
=
0
.
0
;
f_nearest
=
0
.
0
;
f_upper
=
0
.
0
}
...
...
@@ -99,7 +100,9 @@ let make_float ~num ~den ~exp ~man_size ~min_exp ~max_exp =
else
inf
~
man_size
~
max_exp
else
zero
(* -------------------------------------------------------------------------- *)
(* --- Parser Engine --- *)
(* -------------------------------------------------------------------------- *)
let
reg_exp
=
"[eE][+]?
\\
(-?[0-9]+
\\
)"
let
reg_dot
=
"[.]"
...
...
@@ -110,8 +113,6 @@ let num_dot_frac = Str.regexp (reg_numopt ^ reg_dot ^ reg_numopt)
let
num_dot_frac_exp
=
Str
.
regexp
(
reg_numopt
^
reg_dot
^
reg_numopt
^
reg_exp
)
let
num_exp
=
Str
.
regexp
(
reg_num
^
reg_exp
)
let
float_of_string_opt
s
=
try
Some
(
float_of_string
s
)
with
Failure
_
->
None
...
...
@@ -123,8 +124,6 @@ let sys_single_precision_of_string_opt s =
let
is_hexadecimal
s
=
String
.
length
s
>=
2
&&
s
.
[
0
]
=
'
0
'
&&
(
Char
.
uppercase_ascii
s
.
[
1
]
=
'
X'
)
exception
Shortcut
of
parsed_float
let
match_exp
~
man_size
~
min_exp
~
max_exp
group
s
=
...
...
@@ -178,7 +177,9 @@ let parse_positive_float ~man_size ~min_exp ~max_exp s =
try
parse_positive_float_with_shortcut
~
man_size
~
min_exp
~
max_exp
s
with
Shortcut
r
->
Some
r
(* -------------------------------------------------------------------------- *)
(* --- Float & Double Parsers --- *)
(* -------------------------------------------------------------------------- *)
let
rec
single_precision_of_string
s
=
let
open
Option
.
Operators
in
...
...
@@ -202,12 +203,14 @@ let rec double_precision_of_string s =
{
f_lower
=
f
;
f_nearest
=
f
;
f_upper
=
f
}
else
parse_positive_float
~
man_size
:
52
~
min_exp
:
(
-
1022
)
~
max_exp
:
1023
s
(* -------------------------------------------------------------------------- *)
(* --- Qualified C-float literals --- *)
(* -------------------------------------------------------------------------- *)
let
parse_fkind
string
=
function
|
Cil_types
.
FFloat
->
single_precision_of_string
string
|
Cil_types
.(
FDouble
|
FLongDouble
)
->
double_precision_of_string
string
let
fkind_of_char
=
function
|
'
F'
->
Cil_types
.
FFloat
,
true
|
'
D'
->
Cil_types
.
FDouble
,
true
...
...
@@ -224,8 +227,6 @@ let pretty_fkind fmt = function
|
Cil_types
.
FDouble
->
Format
.
fprintf
fmt
"double precision"
|
Cil_types
.
FLongDouble
->
Format
.
fprintf
fmt
"long double precision"
let
cannot_be_parsed
string
fkind
=
Kernel
.
abort
~
current
:
true
"The string %s cannot be parsed as a %a floating-point constant"
...
...
@@ -235,6 +236,10 @@ let empty_string () =
Kernel
.
abort
~
current
:
true
"Parsing an empty string as a floating-point constant."
(* -------------------------------------------------------------------------- *)
(* --- Full Parser --- *)
(* -------------------------------------------------------------------------- *)
let
parse
string
=
let
l
=
String
.
length
string
-
1
in
if
l
>=
0
then
...
...
@@ -246,13 +251,15 @@ let parse string =
|
None
->
cannot_be_parsed
string
fkind
else
empty_string
()
let
has_suffix
fk
lit
=
let
ln
=
String
.
length
lit
in
let
suffix
=
suffix_of_fkind
fk
in
ln
>
0
&&
Char
.
uppercase_ascii
lit
.
[
ln
-
1
]
=
suffix
(* -------------------------------------------------------------------------- *)
(* --- Classification --- *)
(* -------------------------------------------------------------------------- *)
let
is_not_finite
f
=
match
classify_float
f
with
|
FP_normal
|
FP_subnormal
|
FP_zero
->
false
...
...
@@ -261,6 +268,10 @@ let is_not_finite f =
let
is_not_integer
s
=
String
.(
contains
s
'.'
||
contains
s
'
e'
||
contains
s
'
E'
)
(* -------------------------------------------------------------------------- *)
(* --- Pretty Printing --- *)
(* -------------------------------------------------------------------------- *)
let
pretty_normal
~
use_hex
fmt
f
=
let
double_norm
=
Int64
.
shift_left
1
L
52
in
let
double_mask
=
Int64
.
pred
double_norm
in
...
...
@@ -309,7 +320,9 @@ let pretty fmt f =
Format
.
fprintf
fmt
"%s%s"
r
dot
else
pretty_normal
~
use_hex
fmt
f
(* -------------------------------------------------------------------------- *)
(* --- Conversions --- *)
(* -------------------------------------------------------------------------- *)
type
sign
=
Neg
|
Pos
...
...
@@ -341,13 +354,14 @@ let bits_of_most_negative_float =
let
v
=
Int64
.
of_int32
0xFF7FFFFF
l
in
Integer
.
of_int64
v
external
fround
:
float
->
float
=
"c_round"
external
trunc
:
float
->
float
=
"c_trunc"
(** Single-precision (32-bit) functions. We round the result computed
as a double, since float32 functions are rarely precise. *)
(* -------------------------------------------------------------------------- *)
(* --- Single Precision Operations --- *)
(* -------------------------------------------------------------------------- *)
(* We round the result float64 operators since float32 ones are less precise. *)
external
expf
:
float
->
float
=
"c_expf"
external
logf
:
float
->
float
=
"c_logf"
...
...
@@ -362,9 +376,9 @@ external asinf: float -> float = "c_asinf"
external
atanf
:
float
->
float
=
"c_atanf"
external
atan2f
:
float
->
float
->
float
=
"c_atan2f"
(*
* C math-like functions
*)
(* -------------------------------------------------------------------------- *)
(* --- C-Math like functions --- *)
(*
--------------------------------------------------------------------------
*)
let
isnan
f
=
match
classify_float
f
with
...
...
@@ -416,6 +430,7 @@ let nextafter x y =
let
nextafterf
x
y
=
nextafter_aux
~
is_f32
:
true
incr_f32
decr_f32
x
y
(* -------------------------------------------------------------------------- *)
(*
Local Variables:
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment