diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8296d6b0e03a40f5e07236dbec0040b6febdb937..e9056c12c0ed2c02c6dba57829a149b92534a576 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -22,7 +22,7 @@ default: variables: DEFAULT: "master" - OCAML: "4.11" + OCAML: "4.13" PUBLISH: "no" RELEASE: "no" WEEKLY: "no" @@ -349,11 +349,12 @@ internal_nightly: matrix: - OCAML: ["4.14"] -.build_template: &ocaml_manual_additional_versions_template - parallel: - matrix: - - OCAML: ["4.12", "4.13"] - when: manual +# Uncomment this block when there are intermediate versions to check manully +#.build_template: &ocaml_manual_additional_versions_template +# parallel: +# matrix: +# - OCAML: ["4.14"] +# when: manual .build_template: &ocaml_versions_template stage: compatibility @@ -369,7 +370,8 @@ ocaml-versions: ocaml-versions-more: <<: *ocaml_versions_template - <<: *ocaml_manual_additional_versions_template +# Uncomment below when there are intermediate versions to check manully +# <<: *ocaml_manual_additional_versions_template ocaml-versions-nightly: <<: *ocaml_versions_template diff --git a/opam b/opam index d08f2ed480e158c3c4d8311b019f5b3d6783a673..8ccaa3669bc50deb9d57482d14938f8583ffb088 100644 --- a/opam +++ b/opam @@ -126,10 +126,10 @@ depends: [ "conf-graphviz" { post } "conf-time" { with-test } "menhir" { >= "20181006" & build } - "ocaml" { >= "4.11.1" } - "ocamlfind" # needed beyond build stage, used by -load-module + "ocaml" { >= "4.13.1" } "ocamlgraph" { >= "1.8.8" } "odoc" { with-doc } + "unionFind" { >= "20220107" } "why3" { >= "1.6.0" } "yaml" { >= "3.0.0" } "yojson" {>= "1.6.0" & (>= "2.0.1" | !with-test)} diff --git a/src/libraries/stdlib/transitioning.ml b/src/libraries/stdlib/transitioning.ml index 747e2811e0bb8fd639f4ab40a1ba9de3d105df22..38937e6f5cbdd8f968d744b6d7dfb2542a655480 100644 --- a/src/libraries/stdlib/transitioning.ml +++ b/src/libraries/stdlib/transitioning.ml @@ -22,31 +22,6 @@ (* Generated file. The file to update is [transitioning.ml.in] *) -module List = struct - - let concat_map f l = - let rec aux f acc = function - | [] -> List.rev acc - | x :: l -> - let xs = f x in - aux f (List.rev_append xs acc) l - in aux f [] l - - let equal f l1 l2 = - l1 == l2 || try List.for_all2 f l1 l2 with Invalid_argument _ -> false - - let rec compare f l1 l2 = - if l1 == l2 then 0 - else match l1, l2 with - | [], [] -> assert false - | [], _ :: _ -> -1 - | _ :: _, [] -> 1 - | x1 :: q1, x2 :: q2 -> - let n = f x1 x2 in - if n = 0 then compare f q1 q2 else n -end - - module Seq = struct open Stdlib.Seq @@ -57,11 +32,6 @@ module Seq = struct let unzip seq = map fst seq, map snd seq - let rec append xs ys () = - match xs () with - | Nil -> ys () - | Cons (x, xt) -> Cons (x, append xt ys) - let is_empty xs = match xs () with | Nil -> true diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli index 3be73b061e217174606f3e5d4d2f29ac56d55f0f..1954b47f420ad0981b2c2dc7f5c78d8fee853f75 100644 --- a/src/libraries/stdlib/transitioning.mli +++ b/src/libraries/stdlib/transitioning.mli @@ -32,17 +32,6 @@ (** {1 OCaml} *) -module List: sig - (** since 4.10.0 *) - val concat_map: ('a -> 'b list) -> 'a list -> 'b list - - (** since 4.12.0 *) - val equal: ('a -> 'a -> bool) -> 'a list -> 'a list -> bool - - (** since 4.12.0 *) - val compare: ('a -> 'a -> int) -> 'a list -> 'a list -> int -end - module Seq: sig open Stdlib.Seq @@ -55,9 +44,6 @@ module Seq: sig (** since 4.14.0 *) val unzip : ('a * 'b) t -> 'a t * 'b t - (** since 4.11.0 *) - val append : 'a t -> 'a t -> 'a t - (** since 4.14.0 *) val drop : int -> 'a t -> 'a t end diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml index b1fff81fcd0702622895d473cd5717a959edf906..04d64f4fbae2c351ec37449dbb1179535c1b3dba 100644 --- a/src/libraries/utils/hptmap.ml +++ b/src/libraries/utils/hptmap.ml @@ -343,7 +343,7 @@ module Shape(Key: Id_Datatype) = struct | Empty -> Seq.Nil | Leaf (key, data, _) -> Seq.Cons ((key, data), Seq.empty) | Branch (_, _, tree0, tree1, _) -> - Transitioning.Seq.append (to_seq tree0) (to_seq tree1) () + Seq.append (to_seq tree0) (to_seq tree1) () (* This reference will contain a list of functions that will clear all the transient caches used in this module *) diff --git a/src/plugins/eva/domains/multidim/segmentation.ml b/src/plugins/eva/domains/multidim/segmentation.ml index 06ffc859de30512647526c323c0476eb2eef6157..475933251eaa60f4d2ca7ea589200eeeb63ce19b 100644 --- a/src/plugins/eva/domains/multidim/segmentation.ml +++ b/src/plugins/eva/domains/multidim/segmentation.ml @@ -471,7 +471,7 @@ struct M.compare v1 v2 <?> lazy (B.compare u1 u2) in B.compare m1.start m2.start <?> - lazy (Transitioning.List.compare compare_segments m1.segments m2.segments) <?> + lazy (List.compare compare_segments m1.segments m2.segments) <?> lazy (Bit.compare m1.padding m2.padding) let equal (m1 : t) (m2 : t) : bool = @@ -479,7 +479,7 @@ struct M.equal v1 v2 && B.equal u1 u2 in B.equal m1.start m2.start && - Transitioning.List.equal equal_segments m1.segments m2.segments && + List.equal equal_segments m1.segments m2.segments && Bit.equal m1.padding m2.padding let raw (m : t) : bit = diff --git a/src/plugins/eva/partitioning/partition.ml b/src/plugins/eva/partitioning/partition.ml index a994030d11119fdf8254e9cde51a4d6962fca531..13ae29b16c5695f7f8418e115b48e0249b67ce18 100644 --- a/src/plugins/eva/partitioning/partition.ml +++ b/src/plugins/eva/partitioning/partition.ml @@ -536,19 +536,19 @@ struct let key = { key with dynamic_splits } in split_state ~monitor term (key, state) in - Transitioning.List.concat_map add_split p + List.concat_map add_split p let update_dynamic_splits p = (* Update one state *) let update_state (key, state) = (* Split the states in the list l for the given exp *) let update_exp term monitor l = - Transitioning.List.concat_map (split_state ~monitor term) l + List.concat_map (split_state ~monitor term) l in (* Foreach exp in original state: split *) SplitMap.fold update_exp key.dynamic_splits [(key,state)] in - Transitioning.List.concat_map update_state p + List.concat_map update_state p let map_keys (f : key -> state -> key) (p : t) : t = List.map (fun (k,x) -> f k x, x) p diff --git a/src/plugins/studia/writes.ml b/src/plugins/studia/writes.ml index 5958368970b0acd176334fff1d5163aecef5a54e..d5a2f6b0584af1ebbf9e74565b1580c54437dfe6 100644 --- a/src/plugins/studia/writes.ml +++ b/src/plugins/studia/writes.ml @@ -42,7 +42,6 @@ let (<?>) c lcmp = let compare w1 w2 = let open Cil_datatype in - let module List = Transitioning.List in match w1, w2 with | Assign s1, Assign s2 | CallDirect s1, CallDirect s2 diff --git a/tools/hdrck/hdrck.ml b/tools/hdrck/hdrck.ml index 036d3b9bb700ea7be4f066bb0cd2e701aea42f33..3a093fa251800ff103c60ae1cdebfc0558890815 100644 --- a/tools/hdrck/hdrck.ml +++ b/tools/hdrck/hdrck.ml @@ -142,11 +142,7 @@ let error ~exit_value = in the header_spec.txt files. *) let path_concat p1 p2 = - (* Note: use String.ends_with when minimum OCaml version is 4.13 *) - if String.length p1 > 0 && String.get p1 (String.length p1 - 1) = '/' then - p1 ^ p2 - else - p1 ^ "/" ^ p2 + if String.ends_with ~suffix:"/" p1 then p1 ^ p2 else p1 ^ "/" ^ p2 (* Temporary directory management (cont.) *) let get_tmp_dirname () = match !tmp_dirname with