Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
71e0ab5d
Commit
71e0ab5d
authored
Oct 15, 2020
by
Andre Maroneze
💬
Browse files
[Kernel] update noalloc annotations to modern OCaml
parent
bbbd3fc5
Changes
6
Hide whitespace changes
Inline
Side-by-side
src/kernel_services/abstract_interp/fc_float.ml
View file @
71e0ab5d
...
...
@@ -58,11 +58,8 @@ let cmp_ieee = (compare: float -> float -> int)
are also considered, e.g. "if x < 0.0" is equivalent to "if x < -0.0",
which is also equivalent to "F.compare x (-0.0) < 0".
This 'compare' operator distinguishes -0. and 0. *)
(* replace "noalloc" with [@@noalloc] for OCaml version >= 4.03.0 *)
[
@@@
warning
"-3"
]
external
compare
:
float
->
float
->
int
=
"float_compare_total"
"noalloc"
external
compare
:
float
->
float
->
int
=
"float_compare_total"
[
@@
noalloc
]
let
total_compare
=
compare
[
@@@
warning
"+3"
]
let
of_float
round
prec
f
=
round
>>%
fun
()
->
round_to_precision
prec
f
...
...
@@ -74,10 +71,7 @@ let is_finite f = match classify_float f with
|
FP_nan
|
FP_infinite
->
false
|
FP_normal
|
FP_subnormal
|
FP_zero
->
true
(* replace "noalloc" with [@@noalloc] for OCaml version >= 4.03.0 *)
[
@@@
warning
"-3"
]
external
is_negative
:
float
->
bool
=
"float_is_negative"
"noalloc"
[
@@@
warning
"+3"
]
external
is_negative
:
float
->
bool
=
"float_is_negative"
[
@@
noalloc
]
let
round_to_precision
round
prec
t
=
if
is_single
prec
...
...
src/kernel_services/abstract_interp/fval.ml
View file @
71e0ab5d
...
...
@@ -59,10 +59,7 @@ module F = struct
are also considered, e.g. "if x < 0.0" is equivalent to "if x < -0.0",
which is also equivalent to "F.compare x (-0.0) < 0".
This 'compare' operator distinguishes -0. and 0. *)
(* replace "noalloc" with [@@noalloc] for OCaml version >= 4.03.0 *)
[
@@@
warning
"-3"
]
external
compare
:
float
->
float
->
int
=
"float_compare_total"
"noalloc"
[
@@@
warning
"+3"
]
external
compare
:
float
->
float
->
int
=
"float_compare_total"
[
@@
noalloc
]
let
equal
f1
f2
=
compare
f1
f2
=
0
(* The Caml version of compare below is fine but the C version above is
...
...
src/libraries/stdlib/extlib.ml
View file @
71e0ab5d
...
...
@@ -330,10 +330,7 @@ let xor x y = if x then not y else y
(** {2 Performance} *)
(* ************************************************************************* *)
(* replace "noalloc" with [@@noalloc] for OCaml version >= 4.03.0 *)
[
@@@
warning
"-3"
]
external
address_of_value
:
'
a
->
int
=
"address_of_value"
"noalloc"
[
@@@
warning
"+3"
]
external
address_of_value
:
'
a
->
int
=
"address_of_value"
[
@@
noalloc
]
(* ************************************************************************* *)
(** {2 Exception catcher} *)
...
...
src/libraries/stdlib/extlib.mli
View file @
71e0ab5d
...
...
@@ -331,10 +331,7 @@ val format_string_of_stag: Format.stag -> string
(** {2 Performance} *)
(* ************************************************************************* *)
(* replace "noalloc" with [@@noalloc] for OCaml version >= 4.03.0 *)
[
@@@
warning
"-3"
]
external
address_of_value
:
'
a
->
int
=
"address_of_value"
"noalloc"
[
@@@
warning
"+3"
]
external
address_of_value
:
'
a
->
int
=
"address_of_value"
[
@@
noalloc
]
(* ************************************************************************* *)
(** {2 Exception catcher} *)
...
...
src/libraries/utils/floating_point.ml
View file @
71e0ab5d
...
...
@@ -29,17 +29,12 @@ let string_of_c_rounding_mode = function
|
FE_Downward
->
"FE_DOWNWARD"
|
FE_TowardZero
->
"FE_TOWARDZERO"
(* replace "noalloc" with [@@noalloc] for OCaml version >= 4.03.0 *)
[
@@@
warning
"-3"
]
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"
external
set_round_toward_zero
:
unit
->
unit
=
"set_round_toward_zero"
"noalloc"
external
get_rounding_mode
:
unit
->
c_rounding_mode
=
"get_rounding_mode"
"noalloc"
external
set_rounding_mode
:
c_rounding_mode
->
unit
=
"set_rounding_mode"
"noalloc"
[
@@@
warning
"+3"
]
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
]
external
set_round_toward_zero
:
unit
->
unit
=
"set_round_toward_zero"
[
@@
noalloc
]
external
get_rounding_mode
:
unit
->
c_rounding_mode
=
"get_rounding_mode"
[
@@
noalloc
]
external
set_rounding_mode
:
c_rounding_mode
->
unit
=
"set_rounding_mode"
[
@@
noalloc
]
external
round_to_single_precision_float
:
float
->
float
=
"round_to_float"
external
sys_single_precision_of_string
:
string
->
float
=
...
...
src/plugins/value_types/cvalue.ml
View file @
71e0ab5d
...
...
@@ -714,10 +714,7 @@ module V_Or_Uninitialized = struct
let
mask_init
=
2
let
mask_noesc
=
1
(* replace "noalloc" with [@@noalloc] for OCaml version >= 4.03.0 *)
[
@@@
warning
"-3"
]
external
get_flags
:
t
->
int
=
"caml_obj_tag"
"noalloc"
[
@@@
warning
"+3"
]
external
get_flags
:
t
->
int
=
"caml_obj_tag"
[
@@
noalloc
]
let
is_initialized
v
=
(
get_flags
v
land
mask_init
)
<>
0
let
is_noesc
v
=
(
get_flags
v
land
mask_noesc
)
<>
0
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment