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/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml index e3c5c99c8db5ef823e98341d23bceef3eec40262..c568af840b21486748fa298ed64232f009ecb91c 100644 --- a/src/kernel_services/abstract_interp/offsetmap.ml +++ b/src/kernel_services/abstract_interp/offsetmap.ml @@ -511,8 +511,9 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct 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 *) + match move_right o t z with + | t -> t + | exception End_reached -> abs_max, Empty, z (* End the recursion at next iteration *) in aux_fold no nt nz now 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/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 ;