Merge branch 'feature/cleanup/state_selection_static_gone' into 'master'

[project] get rid of since-10-years-deprecated State_selection.Static

Closes #1103

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

Changelog

@@ -21,6 +21,8 @@ Open Source Release <next-release>
 o   Kernel    [2022-02-23] New visitor functions visitFramacFileFunctions
               and visitCilFileFunctions to visit only function definitions,
               for better performance.
+o! [kernel]   [2022-02-23] Remove State_selection.Static (deprecated since
+              10 years, use directly State_selection instead)
 -*  Kernel    [2022-02-22] Fix list of potential types for decimal
               integer literal constants
 *   Kernel    [2022-02-17] Reject programs using unsupported
@@ -28,6 +30,9 @@ o   Kernel    [2022-02-23] New visitor functions visitFramacFileFunctions
 *   Kernel    [2022-02-08] Reject array whose size is too big with a proper
               error message instead of a crash (fixes ##2590)
 o!  Kernel    [2022-01-19] Removed obsolete AST nodes IndexPI and Info
+o!  Kernel    [2022-02-19] Removed obsolete AST nodes IndexPI and Info
+*   Kernel    [2022-02-08] Reject array whose size is too big with a proper
+              error message instead of a crash (fixes ##2590)
 o!  Kernel    [2021-12-03] Remove unused AST node Dcustom_annot and field
               fpadding_in_bits. Do not cache size of types in the AST but in
               a dedicated table.

bin/migration_scripts/chromium2manganese.sh

@@ -89,6 +89,7 @@ process_file ()
    -e 's/(Integer\.pretty ~hexa:true)/Integer.pretty_hex/g' \
    -e 's/Integer\.pretty ~hexa:false/Integer.pretty/g' \
    -e 's/Integer\.pretty ~hexa:true/Integer.pretty_hex/g' \
+   -e 's/State_selection\.Static/State_selection/g'
    # this line left empty on purpose
 }
 

src/kernel_services/ast_data/ast.ml

@@ -208,7 +208,7 @@ let is_def_or_last_decl g =
   | _ -> false
 
 let clear_last_decl () =
-  let selection = State_selection.Static.with_dependencies LastDecl.self in
+  let selection = State_selection.with_dependencies LastDecl.self in
   Project.clear ~selection ()
 
 let add_hook_on_update f =

src/kernel_services/plugin_entry_points/emitter.ml

@@ -387,7 +387,7 @@ let register_tuning_parameter name p =
 let () =
   Cmdline.run_after_extended_stage
     (fun () ->
-       State_selection.Static.iter
+       State_selection.iter
          (fun s ->
             let tbl = Datatype.String.Hashtbl.create 7 in
             let p = Typed_parameter.get (State.get_name s) in

src/libraries/project/state_selection.ml

@@ -106,158 +106,132 @@ include Datatype.Make
             Type.par p_caller Type.Call fmt pp
     end)
 
-module type S = sig
-  val with_dependencies: State.t -> t
-  val only_dependencies: State.t -> t
-  val with_codependencies: State.t -> t
-  val only_codependencies: State.t -> t
-  val union: t -> t -> t
-  val list_union: t list -> t
-  val diff: t -> t -> t
-  val cardinal: t -> int
-  val to_list: t -> State.t list
-  val pretty: Format.formatter -> t -> unit
-  val pretty_witness: Format.formatter -> t -> unit
-  val iter_succ: (State.t -> unit) -> t -> State.t -> unit
-  val fold_succ: (State.t -> 'a -> 'a) -> t -> State.t -> 'a -> 'a
-  val iter: (State.t -> unit) -> t -> unit
-  val fold: (State.t -> 'a -> 'a) -> t -> 'a -> 'a
-  val iter_in_order: (State.t -> unit) -> t -> unit
-  val fold_in_order: (State.t -> 'a -> 'a) -> t -> 'a -> 'a
-end
-
-module Static = struct
-
-  let transitive_closure next_vertices s =
-    let rec visit acc v =
-      next_vertices
-        (fun v' acc ->
-           let e = v, v' in
-           if Selection.mem_edge_e acc e then acc
-           else visit (Selection.add_edge_e acc e) v')
-        State_dependency_graph.graph v acc
-    in
-    (* add [s] in the selection even if it has no ingoing/outgoing edges *)
-    visit (Selection.add_vertex Selection.empty s) s
-
-  let with_dependencies s =
-    Subset (transitive_closure State_dependency_graph.G.fold_succ s),
-    WDependencies s
-
-  let with_codependencies s =
-    Subset (transitive_closure State_dependency_graph.G.fold_pred s),
-    WCoDependencies s
-
-  let only_dependencies s =
-    let g = transitive_closure State_dependency_graph.G.fold_succ s in
-    Subset (Selection.remove_vertex g s), WStrictDependencies s
-
-  let only_codependencies s =
-    let g = transitive_closure State_dependency_graph.G.fold_pred s in
-    Subset (Selection.remove_vertex g s), WStrictCoDependencies s
-
-  let diff (sel1, w1) (sel2, w2 as selw2) =
-    let sel = match sel1, sel2 with
-      | _, Full -> Subset Selection.empty
-      | Full, _sel2 when is_empty selw2 -> Full
-      | Full, Subset sel2 ->
-        let selection =
-          State_dependency_graph.G.fold_vertex
-            (fun v acc ->
-               if Selection.mem_vertex sel2 v then acc
-               else Selection.add_vertex acc v)
-            State_dependency_graph.graph
-            Selection.empty
-        in
-        let sel =
-          State_dependency_graph.G.fold_edges
-            (fun v1 v2 acc ->
-               if Selection.mem_vertex sel2 v1 || Selection.mem_vertex sel2 v2
-               then acc
-               else Selection.add_edge acc v1 v2)
-            State_dependency_graph.graph
-            selection
-        in
-        Subset sel
-      | Subset sel1, Subset sel2 ->
-        Subset
-          (Selection.fold_vertex
-             (fun v acc -> Selection.remove_vertex acc v) sel2 sel1)
-    in
-    sel, WDiff (w1, w2)
-
-  module Operations = Graph.Oper.P(Selection)
-
-  let union (sel1, w1) (sel2, w2) =
-    let sel = match sel1, sel2 with
-      | Full, _ | _, Full -> Full
-      | Subset sel1, Subset sel2 -> Subset (Operations.union sel1 sel2)
-    in
-    sel, WUnion (w1, w2)
-
-  let list_union l =
-    let sel, _ = List.fold_left union empty l in
-    let w = WOfList (List.map snd l) in
-    sel, w
-
-  let cardinal (sel, _) = match sel with
-    | Full -> State_dependency_graph.G.nb_vertex State_dependency_graph.graph
-    | Subset sel -> Selection.nb_vertex sel
-
-  let iter_succ f (sel, _) v = match sel with
-    | Full ->
-      State_dependency_graph.G.iter_succ f State_dependency_graph.graph v
-    | Subset sel -> Selection.iter_succ f sel v
-
-  let fold_succ f (sel, _) v acc = match sel with
-    | Full ->
-      State_dependency_graph.G.fold_succ f State_dependency_graph.graph v acc
-    | Subset sel -> Selection.fold_succ f sel v acc
-
-  let iter f (sel, _) = match sel with
-    | Full ->
-      State_dependency_graph.G.iter_vertex f State_dependency_graph.graph
-    | Subset sel -> Selection.iter_vertex f sel
-
-  let fold f (sel, _) acc = match sel with
-    | Full ->
-      State_dependency_graph.G.fold_vertex f State_dependency_graph.graph acc
-    | Subset sel -> Selection.fold_vertex f sel acc
-
-  let to_list s = fold (fun s acc -> s :: acc) s []
-
-  module TG = State_topological.Make(State_dependency_graph.G)
-  module TS = State_topological.Make(Selection)
-
-  let iter_in_order f (sel, _) = match sel with
-    | Full -> TG.iter f State_dependency_graph.graph
-    | Subset sel -> TS.iter f sel
-
-  let fold_in_order f (sel, _) acc = match sel with
-    | Full -> TG.fold f State_dependency_graph.graph acc
-    | Subset sel -> TS.fold f sel acc
-
-  let pretty fmt sel =
-    Format.fprintf fmt "contents of the selection:@\n";
-    let mem s =
-      State_dependency_graph.G.mem_vertex
-        State_dependency_graph.graph
-        s
-    in
-    iter_in_order
-      (fun s ->
-         Format.fprintf fmt "\t state %S%s@\n"
-           (State.get_unique_name s)
-           (if mem s then "" else "(\"" ^ State.get_name s ^ "\")"))
-      sel;
-    Format.pp_print_flush fmt ()
-
-  let pretty_witness fmt (_, w) =
-    pretty_witness fmt w
-
-end
-
-include Static
+let transitive_closure next_vertices s =
+  let rec visit acc v =
+    next_vertices
+      (fun v' acc ->
+         let e = v, v' in
+         if Selection.mem_edge_e acc e then acc
+         else visit (Selection.add_edge_e acc e) v')
+      State_dependency_graph.graph v acc
+  in
+  (* add [s] in the selection even if it has no ingoing/outgoing edges *)
+  visit (Selection.add_vertex Selection.empty s) s
+
+let with_dependencies s =
+  Subset (transitive_closure State_dependency_graph.G.fold_succ s),
+  WDependencies s
+
+let with_codependencies s =
+  Subset (transitive_closure State_dependency_graph.G.fold_pred s),
+  WCoDependencies s
+
+let only_dependencies s =
+  let g = transitive_closure State_dependency_graph.G.fold_succ s in
+  Subset (Selection.remove_vertex g s), WStrictDependencies s
+
+let only_codependencies s =
+  let g = transitive_closure State_dependency_graph.G.fold_pred s in
+  Subset (Selection.remove_vertex g s), WStrictCoDependencies s
+
+let diff (sel1, w1) (sel2, w2 as selw2) =
+  let sel = match sel1, sel2 with
+    | _, Full -> Subset Selection.empty
+    | Full, _sel2 when is_empty selw2 -> Full
+    | Full, Subset sel2 ->
+      let selection =
+        State_dependency_graph.G.fold_vertex
+          (fun v acc ->
+             if Selection.mem_vertex sel2 v then acc
+             else Selection.add_vertex acc v)
+          State_dependency_graph.graph
+          Selection.empty
+      in
+      let sel =
+        State_dependency_graph.G.fold_edges
+          (fun v1 v2 acc ->
+             if Selection.mem_vertex sel2 v1 || Selection.mem_vertex sel2 v2
+             then acc
+             else Selection.add_edge acc v1 v2)
+          State_dependency_graph.graph
+          selection
+      in
+      Subset sel
+    | Subset sel1, Subset sel2 ->
+      Subset
+        (Selection.fold_vertex
+           (fun v acc -> Selection.remove_vertex acc v) sel2 sel1)
+  in
+  sel, WDiff (w1, w2)
+
+module Operations = Graph.Oper.P(Selection)
+
+let union (sel1, w1) (sel2, w2) =
+  let sel = match sel1, sel2 with
+    | Full, _ | _, Full -> Full
+    | Subset sel1, Subset sel2 -> Subset (Operations.union sel1 sel2)
+  in
+  sel, WUnion (w1, w2)
+
+let list_union l =
+  let sel, _ = List.fold_left union empty l in
+  let w = WOfList (List.map snd l) in
+  sel, w
+
+let cardinal (sel, _) = match sel with
+  | Full -> State_dependency_graph.G.nb_vertex State_dependency_graph.graph
+  | Subset sel -> Selection.nb_vertex sel
+
+let iter_succ f (sel, _) v = match sel with
+  | Full ->
+    State_dependency_graph.G.iter_succ f State_dependency_graph.graph v
+  | Subset sel -> Selection.iter_succ f sel v
+
+let fold_succ f (sel, _) v acc = match sel with
+  | Full ->
+    State_dependency_graph.G.fold_succ f State_dependency_graph.graph v acc
+  | Subset sel -> Selection.fold_succ f sel v acc
+
+let iter f (sel, _) = match sel with
+  | Full ->
+    State_dependency_graph.G.iter_vertex f State_dependency_graph.graph
+  | Subset sel -> Selection.iter_vertex f sel
+
+let fold f (sel, _) acc = match sel with
+  | Full ->
+    State_dependency_graph.G.fold_vertex f State_dependency_graph.graph acc
+  | Subset sel -> Selection.fold_vertex f sel acc
+
+let to_list s = fold (fun s acc -> s :: acc) s []
+
+module TG = State_topological.Make(State_dependency_graph.G)
+module TS = State_topological.Make(Selection)
+
+let iter_in_order f (sel, _) = match sel with
+  | Full -> TG.iter f State_dependency_graph.graph
+  | Subset sel -> TS.iter f sel
+
+let fold_in_order f (sel, _) acc = match sel with
+  | Full -> TG.fold f State_dependency_graph.graph acc
+  | Subset sel -> TS.fold f sel acc
+
+let pretty fmt sel =
+  Format.fprintf fmt "contents of the selection:@\n";
+  let mem s =
+    State_dependency_graph.G.mem_vertex
+      State_dependency_graph.graph
+      s
+  in
+  iter_in_order
+    (fun s ->
+       Format.fprintf fmt "\t state %S%s@\n"
+         (State.get_unique_name s)
+         (if mem s then "" else "(\"" ^ State.get_name s ^ "\")"))
+    sel;
+  Format.pp_print_flush fmt ()
+
+let pretty_witness fmt (_, w) =
+  pretty_witness fmt w
 
 (*
 Local Variables:

src/libraries/project/state_selection.mli

@@ -77,113 +77,99 @@ val mem: t -> State.t -> bool
 (** {2 Specific selections} *)
 (* ************************************************************************** *)
 
-(** Operations over selections which depend on a State Dependency Graph
-    implementation.
-    @since Carbon-20101201 *)
-module type S = sig
-
-  (* ************************************************************************ *)
-  (** {2 Builders from dependencies} *)
-  (* ************************************************************************ *)
-
-  val with_dependencies: State.t -> t
-  (** The selection containing the given state and all its dependencies.
-      @since Carbon-20101201
-      @plugin development guide *)
 
-  val only_dependencies: State.t -> t
-  (** The selection containing all the dependencies of the given state (but not
-      this state itself).
-      @since Carbon-20101201
-      @plugin development guide *)
+(* ************************************************************************ *)
+(** {3 Builders from dependencies} *)
+(* ************************************************************************ *)
 
-  val with_codependencies: State.t -> t
-  (** The selection containing the given state and all its co-dependencies.
-      @since Carbon-20101201 *)
+val with_dependencies: State.t -> t
+(** The selection containing the given state and all its dependencies.
+    @since Carbon-20101201
+    @plugin development guide *)
 
-  val only_codependencies: State.t -> t
-  (** The selection containing all the co-dependencies of the given state (but
-      not this state itself).
-      @since Carbon-20101201 *)
+val only_dependencies: State.t -> t
+(** The selection containing all the dependencies of the given state (but not
+    this state itself).
+    @since Carbon-20101201
+    @plugin development guide *)
 
-  (* ************************************************************************ *)
-  (** {2 Builders by operations over sets} *)
-  (* ************************************************************************ *)
+val with_codependencies: State.t -> t
+(** The selection containing the given state and all its co-dependencies.
+    @since Carbon-20101201 *)
 
-  val union: t -> t -> t
-  (** Union of two selections.
-      @since Carbon-20101201 *)
+val only_codependencies: State.t -> t
+(** The selection containing all the co-dependencies of the given state (but
+    not this state itself).
+    @since Carbon-20101201 *)
 
-  val list_union: t list -> t
-  (** Union of an arbitrary number of selection (0 gives an empty selection)
-      @since Oxygen-20120901
-  *)
+(* ************************************************************************ *)
+(** {3 Builders by operations over sets} *)
+(* ************************************************************************ *)
 
-  val diff: t -> t -> t
-  (** Difference between two selections.
-      @since Carbon-20101201 *)
+val union: t -> t -> t
+(** Union of two selections.
+    @since Carbon-20101201 *)
 
-  (* ************************************************************************ *)
-  (** {2 Specific Getters} *)
-  (* ************************************************************************ *)
+val list_union: t list -> t
+(** Union of an arbitrary number of selection (0 gives an empty selection)
+    @since Oxygen-20120901
+*)
 
-  val cardinal: t -> int
-  (** Size of a selection.
-      @since Carbon-20101201 *)
+val diff: t -> t -> t
+(** Difference between two selections.
+    @since Carbon-20101201 *)
 
-  val to_list: t -> State.t list
-  (** Convert a selection into a list of states.
-      @since Fluorine-20130401 *)
+(* ************************************************************************ *)
+(** {3 Specific Getters} *)
+(* ************************************************************************ *)
 
-  val pretty: Format.formatter -> t -> unit
-  (** Display a selection.
-      @since Carbon-20101201 *)
+val cardinal: t -> int
+(** Size of a selection.
+    @since Carbon-20101201 *)
 
-  val pretty_witness: Format.formatter -> t -> unit
-  (** Display a selection in a more concise form. (Using the atomic operations
-      that were used to create it.)
-      @since Aluminium-20160501 *)
+val to_list: t -> State.t list
+(** Convert a selection into a list of states.
+    @since Fluorine-20130401 *)
 
+val pretty: Format.formatter -> t -> unit
+(** Display a selection.
+    @since Carbon-20101201 *)
 
-  (** {3 Iterators} *)
+val pretty_witness: Format.formatter -> t -> unit
+(** Display a selection in a more concise form. (Using the atomic operations
+    that were used to create it.)
+    @since Aluminium-20160501 *)
 
-  val iter_succ: (State.t -> unit) -> t -> State.t -> unit
-  (** Iterate over the successor of a state in a selection.
-      The order is unspecified.
-      @since Carbon-20101201 *)
 
-  val fold_succ: (State.t -> 'a -> 'a) -> t -> State.t -> 'a -> 'a
-  (** Iterate over the successor of a state in a selection.
-      The order is unspecified.
-      @since Carbon-20101201 *)
+(** {3 Iterators} *)
 
-  val iter: (State.t -> unit) -> t -> unit
-  (** Iterate over a selection. The order is unspecified.
-      @since Carbon-20101201 *)
+val iter_succ: (State.t -> unit) -> t -> State.t -> unit
+(** Iterate over the successor of a state in a selection.
+    The order is unspecified.
+    @since Carbon-20101201 *)
 
-  val fold: (State.t -> 'a -> 'a) -> t -> 'a -> 'a
-  (** Fold over a selection. The order is unspecified.
-      @since Carbon-20101201 *)
+val fold_succ: (State.t -> 'a -> 'a) -> t -> State.t -> 'a -> 'a
+(** Iterate over the successor of a state in a selection.
+    The order is unspecified.
+    @since Carbon-20101201 *)
 
-  val iter_in_order: (State.t -> unit) -> t -> unit
-  (** Iterate over a selection in a topological ordering compliant with the
-      State Dependency Graph. Less efficient that {!iter}.
-      @since Carbon-20101201 *)
+val iter: (State.t -> unit) -> t -> unit
+(** Iterate over a selection. The order is unspecified.
+    @since Carbon-20101201 *)
 
-  val fold_in_order: (State.t -> 'a -> 'a) -> t -> 'a -> 'a
-  (** Fold over a selection in a topological ordering compliant with the
-      State Dependency Graph. Less efficient that {!iter}.
-      @since Carbon-20101201 *)
+val fold: (State.t -> 'a -> 'a) -> t -> 'a -> 'a
+(** Fold over a selection. The order is unspecified.
+    @since Carbon-20101201 *)
 
-end
+val iter_in_order: (State.t -> unit) -> t -> unit
+(** Iterate over a selection in a topological ordering compliant with the
+    State Dependency Graph. Less efficient that {!iter}.
+    @since Carbon-20101201 *)
 
-(** Operations over selections which depend on
-    {!State_dependency_graph.graph}.
-    @since Carbon-20101201
-    @deprecated Oxygen-20120901 directly use equivalent top-level function
-    instead. *)
-module Static: S
-include S
+val fold_in_order: (State.t -> 'a -> 'a) -> t -> 'a -> 'a
+(** Fold over a selection in a topological ordering compliant with the
+    State Dependency Graph. Less efficient that {!iter}.
+    @since Carbon-20101201 *)
 
 (*
 Local Variables:

src/plugins/obfuscator/obfuscator_register.ml

@@ -23,14 +23,14 @@
 let disable_other_analyzers () =
   if Options.Run.get () then
     let selection =
-      State_selection.Static.diff
+      State_selection.diff
         (Parameter_state.get_selection ())
-        (State_selection.Static.union
+        (State_selection.union
            (State_selection.of_list
               (Kernel.CodeOutput.self :: Options.states))
            (* The command-line options that govern the creation of the AST
               must be preserved *)
-           (State_selection.Static.with_codependencies Ast.self))
+           (State_selection.with_codependencies Ast.self))
     in
     Project.clear ~selection ()
 

src/plugins/report/tests/report/multi_emitters.ml

-let emitter1 = 
+let emitter1 =
   Emitter.create "Test1" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
 
-let emitter2 = 
+let emitter2 =
   Emitter.create "Test2" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
 
 let set_status e s =
-  Kernel.feedback "%a SET STATUS TO %a" 
+  Kernel.feedback "%a SET STATUS TO %a"
     Emitter.pretty e Property_status.Emitted_status.pretty s;
   Annotations.iter_all_code_annot
     (fun stmt _ ca ->
-      let kf = Kernel_function.find_englobing_kf stmt in
-      let ps = Property.ip_of_code_annot kf stmt ca in
-      List.iter (fun p -> Property_status.emit e p ~hyps:[] s) ps)
+       let kf = Kernel_function.find_englobing_kf stmt in
+       let ps = Property.ip_of_code_annot kf stmt ca in
+       List.iter (fun p -> Property_status.emit e p ~hyps:[] s) ps)
 
 let print_status =
   Dynamic.get
     ~plugin:"Report"
-    "print" 
+    "print"
     (Datatype.func Datatype.unit Datatype.unit)
 
 let clear () =
   Kernel.feedback "CLEARING";
   Project.clear
-    ~selection:(State_selection.Static.with_dependencies Property_status.self)
+    ~selection:(State_selection.with_dependencies Property_status.self)
     ()
 
 let main () =
@@ -31,7 +31,7 @@ let main () =
   set_status emitter1 Property_status.Dont_know;
   set_status emitter2 Property_status.Dont_know;
   (* unknown /\ unknown *)
-  print_status (); 
+  print_status ();
   (* unknown /\ true *)
   set_status emitter1 Property_status.True;
   print_status ();

src/plugins/report/tests/report/no_hyp.ml

@@ -4,9 +4,9 @@ let emitter =
 let set_status s =
   Annotations.iter_all_code_annot
     (fun stmt _ ca ->
-      let kf = Kernel_function.find_englobing_kf stmt in
-      let ps = Property.ip_of_code_annot kf stmt ca in
-      List.iter (fun p -> Property_status.emit emitter p ~hyps:[] s) ps)
+       let kf = Kernel_function.find_englobing_kf stmt in
+       let ps = Property.ip_of_code_annot kf stmt ca in
+       List.iter (fun p -> Property_status.emit emitter p ~hyps:[] s) ps)
 
 let print_status =
   Dynamic.get
@@ -16,7 +16,7 @@ let print_status =
 
 let clear () =
   Project.clear
-    ~selection:(State_selection.Static.with_dependencies Property_status.self)
+    ~selection:(State_selection.with_dependencies Property_status.self)
     ()
 
 let main () =

src/plugins/report/tests/report/several_hyps.ml

 open Cil_types
 
-let emitter = 
+let emitter =
   Emitter.create "Test" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
 
-let emitter2 = 
+let emitter2 =
   Emitter.create "Test2" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
 
 let set_status ?(emitter=emitter) p hyps s =
-  Kernel.feedback "SETTING STATUS OF %a TO %a" 
+  Kernel.feedback "SETTING STATUS OF %a TO %a"
     Property.pretty p
     Property_status.Emitted_status.pretty s;
   Property_status.emit emitter p ~hyps s
@@ -15,13 +15,13 @@ let set_status ?(emitter=emitter) p hyps s =
 let print_status =
   Dynamic.get
     ~plugin:"Report"
-    "print" 
+    "print"
     (Datatype.func Datatype.unit Datatype.unit)
 
 let clear () =
   Kernel.feedback "CLEARING";
   Project.clear
-    ~selection:(State_selection.Static.with_dependencies Property_status.self)
+    ~selection:(State_selection.with_dependencies Property_status.self)
     ()
 
 let main () =
@@ -30,13 +30,13 @@ let main () =
   let main, j, i, h, g =
     let l =
       Annotations.fold_all_code_annot
-	(fun stmt _ ca acc ->
-	  let kf = Kernel_function.find_englobing_kf stmt in
-	  let ps = Property.ip_of_code_annot kf stmt ca in
-	  match ps with
-	  | [ p ] -> p :: acc
-	  | _ -> assert false)
-	[]
+        (fun stmt _ ca acc ->
+           let kf = Kernel_function.find_englobing_kf stmt in
+           let ps = Property.ip_of_code_annot kf stmt ca in
+           match ps with
+           | [ p ] -> p :: acc
+           | _ -> assert false)
+        []
     in
     match l with
     | [ p1; p2; p3; p4; p5 ] -> p1, p2, p3, p4, p5
@@ -57,7 +57,7 @@ let main () =
     clear ();
     f ()
   in
-  let test msg ?(hyps=hyps) set_status_hyps = 
+  let test msg ?(hyps=hyps) set_status_hyps =
     Kernel.feedback msg;
     reset set_status_hyps;
     (* unknown *)
@@ -72,33 +72,33 @@ let main () =
     print_status ()
   in
   let nothing () = () in
-  let valid ?(g=g) ?(i=i) () = 
-    let _i = i in set_status g [] Property_status.True 
+  let valid ?(g=g) ?(i=i) () =
+    let _i = i in set_status g [] Property_status.True
   in
-  let valid_under_hyp ?(g=g) ?(i=i) () = 
+  let valid_under_hyp ?(g=g) ?(i=i) () =
     set_status g [ i ] Property_status.True in
-  let unknown ?(g=g) ?(i=i) () = 
-    let _i = i in set_status g [] Property_status.Dont_know 
+  let unknown ?(g=g) ?(i=i) () =
+    let _i = i in set_status g [] Property_status.Dont_know
   in
-  let invalid ?(g=g) ?(i=i) () = 
-    let _i = i in set_status g [] Property_status.False_and_reachable 
+  let invalid ?(g=g) ?(i=i) () =
+    let _i = i in set_status g [] Property_status.False_and_reachable
   in
-  let invalid_under_hyp ?(g=g) ?i:_ () = 
-    set_status g [ ] Property_status.False_and_reachable 
+  let invalid_under_hyp ?(g=g) ?i:_ () =
+    set_status g [ ] Property_status.False_and_reachable
   in
   let invalid_but_dead ?(g=g) ?(i=i) () =
     set_status i [] Property_status.False_and_reachable;
-    set_status g [ ] Property_status.False_and_reachable 
+    set_status g [ ] Property_status.False_and_reachable
   in
-  let valid_but_dead ?(g=g) ?(i=i) () = 
+  let valid_but_dead ?(g=g) ?(i=i) () =
     set_status i [] Property_status.False_and_reachable;
-    set_status g [ ] Property_status.True 
+    set_status g [ ] Property_status.True
   in
-  let unknown_but_dead ?(g=g) ?(i=i) () = 
+  let unknown_but_dead ?(g=g) ?(i=i) () =
     set_status i [] Property_status.False_and_reachable;
-    set_status g [ i ] Property_status.Dont_know 
+    set_status g [ i ] Property_status.Dont_know
   in
-  let inconsistent ?(g=g) ?(i=i) () = 
+  let inconsistent ?(g=g) ?(i=i) () =
     let _i = i in
     set_status g [ ] Property_status.True;
     set_status ~emitter:emitter2 g [] Property_status.False_and_reachable
@@ -129,9 +129,9 @@ let main () =
   test "CONSIDERED_VALID + INCONSISTENT" ~hyps inconsistent;
   (***************************************************************************)
   let set status_g status_h () =
-(*      (status_h: ?g:Property.t -> ?i:Property.t -> unit -> unit) () =*)
+    (*      (status_h: ?g:Property.t -> ?i:Property.t -> unit -> unit) () =*)
     status_g ();
-(*    status_h ~g:h ~i:j ()*)
+    (*    status_h ~g:h ~i:j ()*)
     status_h ?g:(Some h) ?i:(Some j) ()
   in
   test "VALID + VALID" (set valid valid);
@@ -144,16 +144,16 @@ let main () =
   test "VALID + UNKNOWN_BUT_DEAD" (set valid unknown_but_dead);
   test "VALID + INCONSISTENT" (set valid inconsistent);
   (***************************************************************************)
-  test "VALID_UNDER_HYP + VALID_UNDER_HYP" 
+  test "VALID_UNDER_HYP + VALID_UNDER_HYP"
     (set valid_under_hyp valid_under_hyp);
   test "VALID_UNDER_HYP + UNKNOWN" (set valid_under_hyp unknown);
   test "VALID_UNDER_HYP + INVALID"  (set valid_under_hyp invalid);
-  test "VALID_UNDER_HYP + INVALID_UNDER_HYP" 
+  test "VALID_UNDER_HYP + INVALID_UNDER_HYP"
     (set valid_under_hyp invalid_under_hyp);
-  test "VALID_UNDER_HYP + INVALID_BUT_DEAD" 
+  test "VALID_UNDER_HYP + INVALID_BUT_DEAD"
     (set valid_under_hyp invalid_but_dead);
   test "VALID_UNDER_HYP + VALID_BUT_DEAD" (set valid_under_hyp valid_but_dead);
-  test "VALID_UNDER_HYP + UNKNOWN_BUT_DEAD" 
+  test "VALID_UNDER_HYP + UNKNOWN_BUT_DEAD"
     (set valid_under_hyp unknown_but_dead);
   test "VALID_UNDER_HYP + INCONSISTENT" (set valid_under_hyp inconsistent);
   (***************************************************************************)
@@ -172,24 +172,24 @@ let main () =
   test "INVALID + UNKNOWN_BUT_DEAD" (set invalid unknown_but_dead);
   test "INVALID + INCONSISTENT" (set invalid inconsistent);
   (***************************************************************************)
-  test "INVALID_UNDER_HYP + INVALID_UNDER_HYP" 
+  test "INVALID_UNDER_HYP + INVALID_UNDER_HYP"
     (set invalid_under_hyp invalid_under_hyp);
-  test "INVALID_UNDER_HYP + INVALID_BUT_DEAD" 
+  test "INVALID_UNDER_HYP + INVALID_BUT_DEAD"
     (set invalid_under_hyp invalid_but_dead);
-  test "INVALID_UNDER_HYP + VALID_BUT_DEAD" 
+  test "INVALID_UNDER_HYP + VALID_BUT_DEAD"
     (set invalid_under_hyp valid_but_dead);
   test "INVALID_UNDER_HYP + UNKNOWN_BUT_DEAD"
     (set invalid_under_hyp unknown_but_dead);
-  test "INVALID_UNDER_HYP + INCONSISTENT" 
+  test "INVALID_UNDER_HYP + INCONSISTENT"
     (set invalid_under_hyp inconsistent);
   (***************************************************************************)
-  test "INVALID_BUT_DEAD + INVALID_BUT_DEAD" 
+  test "INVALID_BUT_DEAD + INVALID_BUT_DEAD"
     (set invalid_but_dead invalid_but_dead);
-  test "INVALID_BUT_DEAD + VALID_BUT_DEAD" 
+  test "INVALID_BUT_DEAD + VALID_BUT_DEAD"
     (set invalid_but_dead valid_but_dead);
   test "INVALID_BUT_DEAD + UNKNOWN_BUT_DEAD"
     (set invalid_but_dead unknown_but_dead);
-  test "INVALID_BUT_DEAD + INCONSISTENT" 
+  test "INVALID_BUT_DEAD + INCONSISTENT"
     (set invalid_but_dead inconsistent);
   (***************************************************************************)
   test "VALID_BUT_DEAD + VALID_BUT_DEAD" (set valid_but_dead valid_but_dead);
@@ -204,4 +204,3 @@ let main () =
   test "INCONSISTENT + INCONSISTENT" (set inconsistent inconsistent)
 
 let () = Db.Main.extend main
-

tests/misc/my_visitor.ml

@@ -76,7 +76,7 @@ let main () =
     print ();
     Kernel.SafeArrays.set false;
     Project.clear
-      ~selection:(State_selection.Static.with_dependencies S.self) ();
+      ~selection:(State_selection.with_dependencies S.self) ();
     (* The AST with 1/2 asserts *)
     print ()
   end