diff --git a/src/plugins/wp/MemEmpty.ml b/src/plugins/wp/MemEmpty.ml
index a9999cc1990b2e2b24909ac5926e788623bbc9e2..cf7d3dc174069393407c5a60dcbca667178d9fb0 100644
--- a/src/plugins/wp/MemEmpty.ml
+++ b/src/plugins/wp/MemEmpty.ml
@@ -35,6 +35,8 @@ let configure () =
     Context.set Lang.pointer (fun _typ -> Logic.Int) ;
     Context.set Cvalues.null (p_equal e_zero) ;
   end
+let no_binder = { bind = fun _ f v -> f v }
+let configure_ia _ = no_binder
 
 let hypotheses () = []
 
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 4fbf8ef305ef565611689406e43c078cd379856a..1f21bfb47d4dc75d8042d76d43afebd7fb03eeee 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -391,6 +391,8 @@ let configure () =
     Context.set Lang.pointer (fun _ -> t_addr) ;
     Context.set Cvalues.null (p_equal a_null) ;
   end
+let no_binder = { bind = fun _ f v -> f v }
+let configure_ia _ = no_binder
 
 type pointer = NoCast | Fits | Unsafe
 let pointer = Context.create "MemTyped.pointer"
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index cd5dcfd28d4f04fee81807c9d5604dea8bb52d43..b4d8a304b5e39ebcfb26c760a27b16bc269f24c9 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -49,6 +49,8 @@ struct
 
   let datatype = "MemVar." ^ V.datatype ^ M.datatype
   let configure = M.configure
+  let no_binder = { bind = fun _ f v -> f v }
+  let configure_ia _ = no_binder
 
   let hypotheses () = V.hypotheses () @ M.hypotheses ()
 
diff --git a/src/plugins/wp/MemZeroAlias.ml b/src/plugins/wp/MemZeroAlias.ml
index 1983f2361f498823fd38afb9fccaa19e372d77e6..c88f4531a438160afc5b4b7377c13978f189b43e 100644
--- a/src/plugins/wp/MemZeroAlias.ml
+++ b/src/plugins/wp/MemZeroAlias.ml
@@ -39,6 +39,8 @@ let configure () =
     Context.set Lang.pointer (fun _typ -> Logic.Int) ;
     Context.set Cvalues.null F.(p_equal e_zero) ;
   end
+let no_binder = { bind = fun _ f v -> f v }
+let configure_ia _ = no_binder
 
 (* TODO: compute actual separation hypotheses *)
 let hypotheses () = []
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index aa49e4f9d21b6052dbb868d93dfa3573905c5624..d451e04f15fcb2003abd1d85c6769e6a4afc1da0 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -27,6 +27,7 @@
 open Cil_types
 open Ctypes
 open Lang.F
+open Interpreted_automata
 
 (* -------------------------------------------------------------------------- *)
 (** {1 General Definitions} *)
@@ -34,6 +35,8 @@ open Lang.F
 
 type 'a sequence = { pre : 'a ; post : 'a }
 
+type 'a binder = { bind: 'b 'c. 'a -> ('b -> 'c) -> 'b -> 'c }
+
 (** Oriented equality or arbitrary relation *)
 type equation =
   | Set of term * term (** [Set(a,b)] is [a := b]. *)
@@ -267,6 +270,11 @@ sig
   (** Initializers to be run before using the model.
       Typically sets {!Context} values. *)
 
+  val configure_ia: automaton -> vertex binder
+  (** Given an automaton, return a vertex's binder.
+      Currently used by the automata compiler to bind current vertex.
+      See {!StmtSemantics}. *)
+
   val datatype : string
   (** For projectification. Must be unique among models. *)