Merge branch 'feature/dive_simplify_range_type' into 'master'

The range type is used only with the application int option

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

src/plugins/dive/build.mli

@@ -38,4 +38,4 @@ val explore_backward : depth:int -> t -> node -> unit
 val show : t -> node -> unit
 val hide : t -> node -> unit
 
-val reduce_to_horizon : t -> int option range -> node -> unit
+val reduce_to_horizon : t -> range -> node -> unit

src/plugins/dive/dive_types.ml

@@ -76,12 +76,12 @@ type graph_diff = {
   removed_nodes: node list;
 }
 
-type 'a range = {
-  backward: 'a;
-  forward: 'a;
+type range = {
+  backward: int option;
+  forward: int option;
 }
 
 type window = {
-  perception: int option range; (* depth of exploration *)
-  horizon: int option range; (* hide beyond horizon ; None for infinite *)
+  perception: range; (* depth of exploration *)
+  horizon: range; (* hide beyond horizon ; None for infinite *)
 }

src/plugins/dive/server_interface.ml

@@ -69,7 +69,7 @@ let origin_to_locations = function
       callsites
 
 
-module Range : Data.S with type t = int option range =
+module Range : Data.S with type t = range =
 struct
   include Record ()
 
@@ -80,7 +80,7 @@ struct
 
   let descr = "Parametrization of the exploration range."
   include (val publish "range" ~descr)
-  type t = int option range
+  type t = range
 
   let to_json r=
     default |>