diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 4330418f551dae8d41c1d5e7b89fff6f114bb770..29f82f78abe10376c31592c416d9b74e4fb20414 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/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
 
diff --git a/src/kernel_services/analysis/interpreted_automata.mli b/src/kernel_services/analysis/interpreted_automata.mli
index 9f7eb9bd8126197890c610050b6b332b10a986c6..e751f86f751f2c454f3d5653066ea470e3efae61 100644
--- a/src/kernel_services/analysis/interpreted_automata.mli
+++ b/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 *)
diff --git a/tests/misc/interpreted_automata_dataflow_backward.ml b/tests/misc/interpreted_automata_dataflow_backward.ml
index dce5e8cfc2b03a89b957de3e4c16fe25a09e3071..444b362690d450331706660c8c312762d14c310d 100644
--- a/tests/misc/interpreted_automata_dataflow_backward.ml
+++ b/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 ->
diff --git a/tests/misc/interpreted_automata_dataflow_forward.ml b/tests/misc/interpreted_automata_dataflow_forward.ml
index 97678ef9abb1e9e2e6c4d626c5600abf3ac13d53..017d2f638d0b723b8731704db434122718c5fb6b 100644
--- a/tests/misc/interpreted_automata_dataflow_forward.ml
+++ 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)