diff --git a/src/plugins/instantiate/Instantiate.mli b/src/plugins/instantiate/Instantiate.mli
index 4444dd5d95bae406b65c2def46efcd16145479da..ee3914d0e8094b3def9a1126d5167089cf6d996b 100644
--- a/src/plugins/instantiate/Instantiate.mli
+++ b/src/plugins/instantiate/Instantiate.mli
@@ -84,12 +84,12 @@ module Instantiator_builder: sig
     *)
     val generate_prototype: override_key -> (string * typ)
 
-    (** [generate_spec key fundec loc] must generate the specification of the
+    (** [generate_spec key loc fundec] must generate the specification of the
         [fundec] generated from [key]. The location is the one generated by the
         [Transform] visitor. Note that it must return a [funspec] but should
         {b not} register it in [Annotations] tables.
     *)
-    val generate_spec: override_key -> fundec -> location -> funspec
+    val generate_spec: override_key -> location -> fundec -> funspec
   end
 end
 
diff --git a/src/plugins/instantiate/instantiator_builder.ml b/src/plugins/instantiate/instantiator_builder.ml
index e700239c933ccda3c281059325354f4fd794ebed..05c65a157f7b5071bb44c16f8f93b04660606043 100644
--- a/src/plugins/instantiate/instantiator_builder.ml
+++ b/src/plugins/instantiate/instantiator_builder.ml
@@ -33,7 +33,7 @@ module type Generator_sig = sig
   val retype_args: override_key -> exp list -> exp list
   val args_for_original: override_key -> exp list -> exp list
   val generate_prototype: override_key -> (string * typ)
-  val generate_spec: override_key -> fundec -> location -> funspec
+  val generate_spec: override_key -> location -> fundec -> funspec
 end
 
 module type Instantiator = sig
@@ -90,7 +90,7 @@ module Make_instantiator (G: Generator_sig) = struct
     let spec = Cil.empty_funspec () in
     Globals.Functions.replace_by_definition spec fd loc ;
     let kf = Globals.Functions.get fd.svar in
-    let spec = generate_spec key fd loc in
+    let spec = generate_spec key loc fd in
     Annotations.add_behaviors Options.emitter kf spec.spec_behavior ;
     List.iter
       (Annotations.add_complete Options.emitter kf)
diff --git a/src/plugins/instantiate/instantiator_builder.mli b/src/plugins/instantiate/instantiator_builder.mli
index b0eb2f79fcf975b1957079beed9ac29d32c14e6d..b731e6b55764f9ed6eeb2f8f889ad9a712d4fe03 100644
--- a/src/plugins/instantiate/instantiator_builder.mli
+++ b/src/plugins/instantiate/instantiator_builder.mli
@@ -83,12 +83,12 @@ module type Generator_sig = sig
   *)
   val generate_prototype: override_key -> (string * typ)
 
-  (** [generate_spec key fundec loc] must generate the specification of the
+  (** [generate_spec key loc fundec] must generate the specification of the
       [fundec] generated from [key]. The location is the one generated by the
       [Transform] visitor. Note that it must return a [funspec] but should
       {b not} register it in [Annotations] tables.
   *)
-  val generate_spec: override_key -> fundec -> location -> funspec
+  val generate_spec: override_key -> location -> fundec -> funspec
 end
 
 (** Signature of a instantiator.
diff --git a/src/plugins/instantiate/stdlib/calloc.ml b/src/plugins/instantiate/stdlib/calloc.ml
index 443804eb044e4421e57b327092a23c65cf12c176..2176585ddaf7807c112b09ca3b16e61e1d6b0249 100644
--- a/src/plugins/instantiate/stdlib/calloc.ml
+++ b/src/plugins/instantiate/stdlib/calloc.ml
@@ -107,7 +107,7 @@ let make_behavior_no_allocation loc alloc_type num size =
   let alloc = allocates_nothing () in
   make_behavior ~name:"no_allocation" ~assumes ~assigns ~ensures ~alloc ()
 
-let generate_spec alloc_type { svar = vi } loc =
+let generate_spec alloc_type loc { svar = vi } =
   let (cnum, csize) = match Cil.getFormalsDecl vi with
     | [ cnum ; csize ] -> cnum, csize
     | _ -> unexpected "ill-formed fundec in specification generation"
diff --git a/src/plugins/instantiate/stdlib/free.ml b/src/plugins/instantiate/stdlib/free.ml
index b1adaae34a331f69f8b9f4110511a726cda44cb9..1542cc7a5ab15fd97efe798442ff485b8a1e1cd9 100644
--- a/src/plugins/instantiate/stdlib/free.ml
+++ b/src/plugins/instantiate/stdlib/free.ml
@@ -62,7 +62,7 @@ let make_behavior_no_deallocation loc ptr =
   let alloc = allocates_nothing () in
   make_behavior ~name:"no_allocation" ~assumes ~assigns ~ensures ~alloc ()
 
-let generate_spec _typ { svar = vi } loc =
+let generate_spec _typ loc { svar = vi } =
   let ptr = match Cil.getFormalsDecl vi with
     | [ ptr ] -> cvar_to_tvar ptr
     | _ -> unexpected "ill-formed fundec in specification generation"
diff --git a/src/plugins/instantiate/stdlib/malloc.ml b/src/plugins/instantiate/stdlib/malloc.ml
index f7b3e9f3b0d3485f7cf7ace2a47d12712b19f0bd..f471209a1036b97e080ee7e9a64fadf92bf708db 100644
--- a/src/plugins/instantiate/stdlib/malloc.ml
+++ b/src/plugins/instantiate/stdlib/malloc.ml
@@ -48,7 +48,7 @@ let make_behavior_no_allocation loc ptr_type size =
   let alloc = allocates_nothing () in
   make_behavior ~name:"no_allocation" ~assumes ~assigns ~ensures ~alloc ()
 
-let generate_spec alloc_typ { svar = vi } loc =
+let generate_spec alloc_typ loc { svar = vi } =
   let (csize) = match Cil.getFormalsDecl vi with
     | [ size ] -> size
     | _ -> unexpected "ill-formed fundec in specification generation"
diff --git a/src/plugins/instantiate/string/mem_utils.ml b/src/plugins/instantiate/string/mem_utils.ml
index 200e3f1e37eb746fb20475ec3a73c83087a810de..c1df382fa532adfe35057d5e8c8fb851c51af2c8 100644
--- a/src/plugins/instantiate/string/mem_utils.ml
+++ b/src/plugins/instantiate/string/mem_utils.ml
@@ -58,7 +58,7 @@ let mem2s_typing _ = function
     (Cil.isCompleteType dest)
   | _ -> false
 
-let mem2s_spec ~requires ~assigns ~ensures _t { svar = vi } loc =
+let mem2s_spec ~requires ~assigns ~ensures _t loc { svar = vi } =
   let (cdest, csrc, clen) = match Cil.getFormalsDecl vi with
     | [ dest ; src ; len ] -> dest, src, len
     | _ -> unexpected "ill-formed fundec in specification generation"
diff --git a/src/plugins/instantiate/string/mem_utils.mli b/src/plugins/instantiate/string/mem_utils.mli
index 2a580c48732ada81908001ff088e88858048da53..d81d16f04fea281bfbb861c09515a80a14cff234 100644
--- a/src/plugins/instantiate/string/mem_utils.mli
+++ b/src/plugins/instantiate/string/mem_utils.mli
@@ -56,7 +56,7 @@ val mem2s_spec:
   requires: (identified_predicate list) spec_gen ->
   assigns: assigns spec_gen ->
   ensures: (termination_kind * identified_predicate) list spec_gen ->
-  typ -> fundec -> location -> funspec
+  typ -> location -> fundec -> funspec
 
 val mem2s_typing: typ option -> typ list -> bool
 
diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml
index bb3ce6ca4d87e11a6f6db75609d4ea3ed7aec3b9..f71c0b994c88476f0c387153039b76e60028e403 100644
--- a/src/plugins/instantiate/string/memset.ml
+++ b/src/plugins/instantiate/string/memset.ml
@@ -162,7 +162,7 @@ let generate_ensures e loc t ptr value len =
       { (presult_ptr ~loc t ptr) with pred_name = [ "result"] }
     ])
 
-let generate_spec (_t, e) { svar = vi } loc =
+let generate_spec (_t, e) loc { svar = vi } =
   let (cptr, cvalue, clen) = match Cil.getFormalsDecl vi with
     | [ ptr ; value ; len ] -> ptr, (Some value), len
     | [ ptr ; len ] -> ptr, None, len