Merge branch 'fix/andre/warning-68' into 'master'

[Instantiate] avoid warning 68 with OCaml 4.12

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

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
 

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)

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.

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"

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"

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"

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"

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
 

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