Commit 53ed013b authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'feature/andre/opam-bump-versions' into 'master'

several updates related to minimum OCaml version

See merge request frama-c/frama-c!2898
parents 44302ad3 c789aed5
......@@ -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
......
......@@ -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
```
......
......@@ -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";
......
......@@ -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" }
]
......@@ -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)))
]
......
......@@ -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
......
......@@ -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
......
......@@ -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
;;
......
......@@ -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} *)
......
......@@ -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} *)
......
......@@ -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 =
......
......@@ -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
......
......@@ -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
......
......@@ -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
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
......
......@@ -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
......
......@@ -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 ;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment