Merge branch 'update/blanchard/ocaml/4.14' into 'master'

Minimal OCaml is now 4.14

See merge request frama-c/frama-c!4716

.gitattributes

@@ -394,4 +394,3 @@ README* header_spec=.ignore
 /share/_frama-c header_spec=CEA_LGPL
 
 /src/kernel_internals/runtime/system_config.ml.in header_spec=CEA_LGPL
-/src/libraries/stdlib/transitioning.ml.in header_spec=CEA_LGPL

.gitlab-ci.yml

@@ -22,7 +22,7 @@ default:
 
 variables:
   DEFAULT: "master"
-  OCAML: "4.13"
+  OCAML: "4.14"
   NODE: "22"
   PUBLISH: "no"
   RELEASE: "no"
@@ -465,13 +465,13 @@ additional-arch-release:
 .build_template: &ocaml_always_additional_versions_template
   parallel:
     matrix:
-      - OCAML: ["5.1"]
+      - OCAML: ["5.2"]
 
 # Uncomment this block when there are intermediate versions to check manully
 .build_template: &ocaml_manual_additional_versions_template
   parallel:
     matrix:
-      - OCAML: ["4.14"]
+      - OCAML: ["5.1"]
   when: manual
 
 .build_template: &ocaml_versions_template

INSTALL.md

@@ -375,7 +375,7 @@ To install the required dependencies, you can use opam v2.1
 or higher to do the following (assuming you are in frama-c
 root source folder):
 
-1. `opam switch create frama-c ocaml-base-compiler.4.13.1`
+1. `opam switch create frama-c ocaml-base-compiler.4.14.2`
    to create a compatible opam switch
 2. `opam pin . -n` to pin to the latest development version
 3. `opam install --deps-only .` will fetch and build all

bin/frama-c.debug

@@ -49,7 +49,6 @@ $DYNLINK
 load_printer "extlib.cmo"
 load_printer "filepath.cmo"
 load_printer "integer.cmo"
-load_printer "transitioning.cmo"
 load_printer "pretty_utils.cmo"
 load_printer "cil_types_debug.cmo"
 load_printer "cabs_debug.cmo"

nix/ocaml-versions.txt

-4.13.1
-4.14.1
+4.14.2
 5.1.1
+5.2.0

opam

@@ -129,7 +129,7 @@ depends: [
   "conf-graphviz" { post }
   "conf-time" { with-test }
   "menhir" { >= "20181006" & build }
-  "ocaml" { >= "4.13.1" }
+  "ocaml" { >= "4.14.0" }
   "ocamlgraph" { >= "2.0.0" }
   "ocamlgraph" { with-test & >= "2.1.0" }
   "odoc" { with-doc }

reference-configuration.md

 The following set of packages is known to be a working configuration for
 compiling Frama-C 29.0.
 
-- OCaml 4.13.1
+- OCaml 4.14.2
 - alt-ergo.2.5.3 (for wp, optional)
 - dune.3.13.1
 - dune-configurator.3.13.1

src/libraries/stdlib/transitioning.ml

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2024                                               *)
-(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
-(*         alternatives)                                                  *)
-(*                                                                        *)
-(*  you can redistribute it and/or modify it under the terms of the GNU   *)
-(*  Lesser General Public License as published by the Free Software       *)
-(*  Foundation, version 2.1.                                              *)
-(*                                                                        *)
-(*  It is distributed in the hope that it will be useful,                 *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
-(*  GNU Lesser General Public License for more details.                   *)
-(*                                                                        *)
-(*  See the GNU Lesser General Public License version 2.1                 *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* Generated file. The file to update is [transitioning.ml.in] *)
-
-module Seq = struct
-  open Stdlib.Seq
-
-  let mapi f seq =
-    let i = ref 0 in
-    map (fun x -> let y = f !i x in incr i; y) seq
-
-  let unzip seq =
-    map fst seq, map snd seq
-
-  let is_empty xs =
-    match xs () with
-    | Nil -> true
-    | Cons _ -> false
-
-  let drop n xs =
-    if n < 0
-    then invalid_arg "Seq.drop"
-    else if n = 0
-    then xs
-    else
-      let rec aux n xs =
-        match xs () with
-        | Nil -> Nil
-        | Cons (_, xs) ->
-          let n = n - 1 in
-          if n = 0
-          then xs ()
-          else aux n xs
-      in
-      fun () -> aux n xs
-end

src/libraries/stdlib/transitioning.mli

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2024                                               *)
-(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
-(*         alternatives)                                                  *)
-(*                                                                        *)
-(*  you can redistribute it and/or modify it under the terms of the GNU   *)
-(*  Lesser General Public License as published by the Free Software       *)
-(*  Foundation, version 2.1.                                              *)
-(*                                                                        *)
-(*  It is distributed in the hope that it will be useful,                 *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
-(*  GNU Lesser General Public License for more details.                   *)
-(*                                                                        *)
-(*  See the GNU Lesser General Public License version 2.1                 *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-(** This file contains functions available in recent OCaml releases but
-    unavailable in the oldest OCaml version officially supported by Frama-C. Be
-    sure to update it when support for a given version is dropped.
-
-    Functions are grouped according to the module of the stdlib they
-    emulate. The mentioned OCaml version indicate when the function was
-    introduced in the stdlib (i.e. when Frama-C requires a version higher
-    than that, it can safely be removed from Transitioning).
-*)
-
-(** {1 OCaml} *)
-
-module Seq: sig
-  open Stdlib.Seq
-
-  (** since 4.14.0 *)
-  val is_empty: 'a t -> bool
-
-  (** since 4.14.0 *)
-  val mapi: (int -> 'a -> 'b) -> 'a t -> 'b t
-
-  (** since 4.14.0 *)
-  val unzip : ('a * 'b) t -> 'a t * 'b t
-
-  (** since 4.14.0 *)
-  val drop : int -> 'a t -> 'a t
-end

src/plugins/dive/build.ml

@@ -24,11 +24,6 @@ open Cil_types
 open Dive_types
 
 module Graph = Dive_graph
-module Seq =
-struct
-  include Stdlib.Seq
-  include Transitioning.Seq
-end
 
 let dkey = Self.register_category "build"
 

src/plugins/markdown-report/sarif_gen.ml

@@ -179,7 +179,7 @@ let gen_results remarks =
   in
   let rules, content =
     Alarms.to_seq () |> Seq.filter keep_alarm |>
-    Transitioning.Seq.mapi treat_alarm |> Transitioning.Seq.unzip
+    Seq.mapi treat_alarm |> Seq.unzip
   in
   Datatype.String.Map.of_seq rules, List.of_seq content