[kernel] Pass vertex and edge instead of edge_transition in transfer function

src/kernel_services/analysis/interpreted_automata.ml

@@ -1206,7 +1206,7 @@ sig
 
   val join : t -> t -> t
   val widen : t -> t -> t option (* returns None when inclusion *)
-  val transfer : vertex transition ->  t -> t option
+  val transfer : vertex -> vertex edge ->  t -> t option
 end
 
 module type DataflowAnalysis =
@@ -1254,7 +1254,7 @@ struct
     let process_edge v e acc =
       (* Retrieve origin value *)
       let value = States.find_opt results v in
-      let result = Option.bind value (D.transfer e.edge_transition) in
+      let result = Option.bind value (D.transfer v e) in
       Option.to_list result @ acc
     in
 

src/kernel_services/analysis/interpreted_automata.mli

@@ -52,9 +52,9 @@ type 'a control =
       the given cases and default vertices. *)
 
 (** Vertices are control points. When a vertice is the *start* of a statement,
-    this statement is kept in vertex_stmt. Currently, this statement is kept for
-    two reasons: to know when callbacks should be called and when annotations
-    should be read. *)
+    this statement is kept in [vertex_start_of]. Currently, this statement is
+    kept for two reasons: to know when callbacks should be called and when
+    annotations should be read. *)
 
 type vertex = private {
   vertex_kf : Cil_types.kernel_function;
@@ -325,10 +325,10 @@ sig
       Called on loop heads to ensure the analysis termination. *)
   val widen : t -> t -> t option
 
-  (** Transfer function for transitions: computes the state after the transition
+  (** Transfer function for edges: computes the state after the transition
       from the state before. Returns None if the end of the transition is not
       reachable from the given state. *)
-  val transfer : vertex transition ->  t -> t option
+  val transfer : vertex -> vertex edge ->  t -> t option
 end
 
 (** Simple dataflow analysis *)

tests/misc/interpreted_automata_dataflow_backward.ml

@@ -34,9 +34,9 @@ struct
     | Lval (Var vi, _) -> Set.singleton vi
     | Lval (Mem e, _) -> vars e
 
-  let transfer t v =
+  let transfer _ e v =
     let open Interpreted_automata in
-    let r = match t with
+    let r = match e.edge_transition with
       | Skip | Prop _ | Leave _ | Return (None,_) ->
         v (* Nothing to do *)
       | Enter b ->

tests/misc/interpreted_automata_dataflow_forward.ml

@@ -83,9 +83,9 @@ struct
     with Not_constant ->
       Map.remove vi v
 
-  let transfer t v =
+  let transfer _ e v =
     let open Interpreted_automata in
-    match t with
+    match e.edge_transition with
     | Skip | Return _ | Prop _ | Enter _ | Leave _ -> Some v
     | Guard (exp, kind, _) -> assume v exp kind
     | Instr (Set ((Var vi, NoOffset), exp, _), _) -> Some (assign v vi exp)