diff --git a/Changelog b/Changelog
index 096941c7805da0740a436e1c3b510d473e4f539b..b93770e049663127c886df176930eb8f5e1b16b5 100644
--- a/Changelog
+++ b/Changelog
@@ -46,6 +46,7 @@ Open Source Release <next-release>
option) on loops with several exit conditions, conditions using
equality operators, temporary variables introduced by the Frama-C
normalization or goto statements.
+-! Kernel [2020-07-21] OCaml version greater than or equal to 4.08.1 required.
- Eva [2020-05-29] New builtins for trigonometric functions acos, asin
and atan (and their single-precision version acosf, asinf, atanf).
- Kernel [2020-05-28] Support for C11's _Thread_local storage specifier
diff --git a/INSTALL.md b/INSTALL.md
index 14134ca017f529a047acd96fa1ca579431489928..0ef93eeabc28e91fd91eff3b62ce79e9d0b0a66f 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -180,7 +180,7 @@ sudo apt install make m4 gcc opam
Then opam can be set up using these commands:
```
-opam init --disable-sandboxing -c 4.05.0 --shell-setup
+opam init --disable-sandboxing --shell-setup
eval $(opam env)
opam install -y depext
```
diff --git a/bin/frama-c.debug b/bin/frama-c.debug
index 39667bbb3b51dce581215eab1876f0450075fe6c..2e110a0af4c4b7271aedf426e33d55f6bbc1652e 100755
--- a/bin/frama-c.debug
+++ b/bin/frama-c.debug
@@ -33,7 +33,6 @@ fi
OCAML_VERSION=$(ocamlc -version)
case $OCAML_VERSION in
-4.05*|4.06*|4.07*) DYNLINK='load_printer "dynlink.cma"';;
4.08*)
echo "impossible to load dynlink in ocamldebug for version $OCAML_VERSION";
echo "pretty-printers will not be loaded";
diff --git a/opam/opam b/opam/opam
index 3dd15df5e212f1161e02cb8e900bdd8fa4d91fc5..d183cd513d31a989cc7a04f3df78bb13edf28501 100644
--- a/opam/opam
+++ b/opam/opam
@@ -102,13 +102,13 @@ run-test: [
]
depends: [
- "ocaml" { >= "4.05.0" & ( < "4.08.0~" | >= "4.08.1" ) }
+ "ocaml" { >= "4.08.1" }
"ocamlgraph" { >= "1.8.8" & < "1.9~" }
"ocamlfind" # needed beyond build stage, used by -load-module
"zarith"
"conf-autoconf" { build }
- ( ( "lablgtk" { >= "2.18.2" } & "conf-gnomecanvas" & "conf-gtksourceview" )
- | ( "lablgtk3" { >= "3.0.beta4" & os!="macos" }
+ ( ( "lablgtk" { >= "2.18.8" } & "conf-gnomecanvas" & "conf-gtksourceview" )
+ | ( "lablgtk3" { >= "3.1.0" & os!="macos" }
& "lablgtk3-sourceview3" & "conf-gtksourceview3" ) )
( "alt-ergo-free" | "alt-ergo" )
"conf-graphviz" { post }
@@ -128,18 +128,9 @@ depopts: [
"ppx_deriving_yojson"
]
-conflicts: [
- "lablgtk" { < "2.18.2" } #for ocaml >= 4.02.1
- "frama-c-e-acsl" #avoid mixing old releases of E-ACSL, it is already
- #distributed with this version of Frama-C
- "frama-c-base" #avoid mixing old releases of Frama-C, now that only the
- #'frama-c' package exists
-]
-
messages: [
"The Frama-C/Wp now uses Why-3 for all provers (Cf. deprecated -wp-prover native:alt-ergo)"
{alt-ergo:installed}
"The Frama-C/Wp native support for Coq is now deprecated (use TIP or Why-3 instead)."
{coq:installed}
- "WARNING: There is a known issue with OCaml 4.05.0 and ocamlfind 1.8.1 (https://github.com/ocaml/opam-repository/issues/10925) when upgrading from a previous ocamlfind. If the compilation of Frama-C fails, try downgrading ocamlfind to 1.8.0 or upgrading OCaml to > 4.05.0." { ocaml:version = "4.05.0" & ocamlfind:version = "1.8.1" }
]
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 603bab87c565977c17eece7e50293bb4e86baaff..71d54b7ee3449b04cebdab892e97bdc67ada3112 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -233,12 +233,12 @@ let init_lexicon _ =
let filename =
Filepath.Normalized.to_pretty_string (fst loc).pos_path
in
- (* TODO: when 4.07 becomes minimal OCaml version,
- use String.to_seq and Seq.fold_left. *)
- let l = ref [] in
- let convert_char c = l:=Int64.of_int (Char.code c) :: !l in
- String.iter convert_char filename;
- CST_STRING (List.rev !l,loc)))
+ let seq = String.to_seq filename in
+ let convert_char c = Int64.of_int (Char.code c) in
+ let l =
+ Seq.fold_left (fun acc c -> convert_char c :: acc) [] seq
+ in
+ CST_STRING (List.rev l,loc)))
]
diff --git a/src/kernel_services/abstract_interp/fc_float.ml b/src/kernel_services/abstract_interp/fc_float.ml
index 3fd653052056c4e4aede01aaa7a01b37fc20652c..748e227d2dd83dd709a9d36b08724a06029ebbd5 100644
--- a/src/kernel_services/abstract_interp/fc_float.ml
+++ b/src/kernel_services/abstract_interp/fc_float.ml
@@ -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
diff --git a/src/kernel_services/abstract_interp/fval.ml b/src/kernel_services/abstract_interp/fval.ml
index 8bd884baf257cd2d9b9d7af27fd10e6b8337a536..a3771a9b86e7d65a30c5a5fdd7c2dcab18d3c45a 100644
--- a/src/kernel_services/abstract_interp/fval.ml
+++ b/src/kernel_services/abstract_interp/fval.ml
@@ -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
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index e3c5c99c8db5ef823e98341d23bceef3eec40262..624255d6fe3c6a3389ab128ccd16a2357a62c77c 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -510,13 +510,9 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
| Node (max, _, _, _, _, r, m, v, _) ->
let abs_max = max +~ o in
let now = f (o, abs_max) (v, m, r) pre in
- let no, nt, nz =
- try move_right o t z
- with End_reached -> (* Use match ... with exception in 4.02 *)
- abs_max, Empty, z (* End the recursion at next iteration *)
- in
- aux_fold no nt nz now
-
+ match move_right o t z with
+ | no, nt, nz -> aux_fold no nt nz now
+ | exception End_reached -> now
in
aux_fold o n z acc
;;
@@ -531,16 +527,11 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
match t with
| Empty -> ()
| Node (max, _, _, _, _, r, m, v, _) ->
- begin
- let abs_max = max +~ o in
- f (o, abs_max) (v, m, r);
- let no, nt, nz =
- try move_right o t z
- with End_reached ->
- abs_max, Empty, z (* End the recursion at next iteration *)
- in
- aux_iter no nt nz
- end
+ let abs_max = max +~ o in
+ f (o, abs_max) (v, m, r);
+ match move_right o t z with
+ | no, nt, nz -> aux_iter no nt nz
+ | exception End_reached -> ()
in
aux_iter o n z
;;
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 04d1facd71e8c7df8b9a21aef7b9b054ff26f70b..1877cb944df416118f4d499324ec6dfaa41a3b25 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -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} *)
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 7a1204e843cf57bea0b27b12844c5a73774360b1..391de576362035a40b73ea78cfb7f9acabaef5fb 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -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} *)
diff --git a/src/libraries/utils/floating_point.ml b/src/libraries/utils/floating_point.ml
index 63c67cd7a57612bf07140f07269a0442f07bf13f..e86a8df5f1b6cb8e8f746abd8f2ea87dcffac109 100644
--- a/src/libraries/utils/floating_point.ml
+++ b/src/libraries/utils/floating_point.ml
@@ -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 =
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index 932ff7ea662055bb9bc6a51c4aff786fa7fce132..6b6aa63f210194985e9d5c417a9d7b6f21e54c93 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -28,8 +28,7 @@ module P = Plugin.Register
let help = "Executable ANSI/ISO C Specification Language --- runtime \
assertion checker generator"
end)
-module PP = P (* [PP] required to avoid an ocamldoc error in OCaml 4.02 *)
-include PP
+include P
module Run =
False
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index 2c342d7285f90966395484b127e28bdba7f74925..d751577ab1e2d2fd6e3d761ca26ce6a3b1a5cfd7 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -94,7 +94,6 @@ let section_stubs env =
in
let stubbed_kf = List.filter Kernel_function.is_definition stubbed_kf in
let opt = Dynamic.Parameter.String.get "-eva-use-spec" () in
- (* NB: requires OCaml >= 4.04 *)
let l = String.split_on_char ',' opt in
let use_spec =
Extlib.filter_map
diff --git a/src/plugins/scope/zones.ml b/src/plugins/scope/zones.ml
index fad94b2d116a38c41b4c04cfa56acf2c4690467f..bb4292562c0cb6b5afabf476bfc9acae85ec9f47 100644
--- a/src/plugins/scope/zones.ml
+++ b/src/plugins/scope/zones.ml
@@ -329,10 +329,7 @@ let get stmt_zones stmt =
let pretty fmt stmt_zones =
let pp s d = Format.fprintf fmt "Stmt:%d -> %a@." s.sid Data.pretty d in
- (* Sort output so that it does not depend on the OCaml hash function.
- Can be removed when OCaml 4.01 is mandatory *)
- let sorted = Stmt.Hashtbl.fold Stmt.Map.add stmt_zones Stmt.Map.empty in
- Stmt.Map.iter pp sorted
+ Stmt.Hashtbl.iter_sorted pp stmt_zones
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 4d817854fc534d2de8746f3568c46352a94f8707..6647c539acf0696c7c8f7f84eda30496e9ffe98f 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -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
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index dac25e8ec8d00a02707cc800cc423161833a4bbc..0a837cbf7378b488a8eb1bea384c7b4b93c72326 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1320,8 +1320,7 @@ struct
(* --- WPO Grouper --- *)
(* -------------------------------------------------------------------------- *)
- (* NOTE: bug in ocamldoc in OCaml 4.02 prevents usage of 'P' here *)
- module PMAP = Map.Make(WpPropId.PropId)
+ module PMAP = Map.Make(P)
type group = {
mutable verifs : VC_Annot.t Bag.t ;