[Variadic] use Cil_builder for the translation

.Makefile.lint

@@ -338,9 +338,6 @@ ML_LINT_KO+=src/plugins/variadic/format_string.ml
 ML_LINT_KO+=src/plugins/variadic/format_typer.ml
 ML_LINT_KO+=src/plugins/variadic/format_typer.mli
 ML_LINT_KO+=src/plugins/variadic/format_types.mli
-ML_LINT_KO+=src/plugins/variadic/generic.ml
 ML_LINT_KO+=src/plugins/variadic/options.ml
-ML_LINT_KO+=src/plugins/variadic/standard.ml
 ML_LINT_KO+=src/plugins/variadic/translate.ml
-ML_LINT_KO+=src/plugins/variadic/va_build.ml
 ML_LINT_KO+=src/plugins/variadic/va_types.mli

headers/header_spec.txt

@@ -1453,7 +1453,6 @@ src/plugins/variadic/options.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/variadic/register.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/variadic/standard.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/variadic/translate.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/variadic/va_build.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/variadic/va_types.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/wp/.gitignore: .ignore
 src/plugins/wp/.ocp-indent: .ignore

src/plugins/variadic/generic.ml

@@ -24,7 +24,7 @@ open Cil_types
 open Options
 module List = Extends.List
 module Typ = Extends.Typ
-module Build = Va_build
+module Build = Cil_builder.Pure
 
 
 (* Types of variadic parameter and argument *)
@@ -39,7 +39,7 @@ let vpar =
 (* Translation of variadic types (not deeply) *)
 
 let translate_type = function
-| TFun (ret_typ, args, is_variadic, attributes) ->
+  | TFun (ret_typ, args, is_variadic, attributes) ->
     let new_args =
       if is_variadic
       then
@@ -47,11 +47,11 @@ let translate_type = function
         Some (ng_args @ [vpar] @ g_args)
       else args
     in
-    TFun (ret_typ, new_args, false, attributes)      
+    TFun (ret_typ, new_args, false, attributes)
 
-| TBuiltin_va_list attr -> vpar_typ attr
+  | TBuiltin_va_list attr -> vpar_typ attr
 
-| typ -> typ
+  | typ -> typ
 
 
 (* Adding the vpar parameter to variadic functions *)
@@ -60,85 +60,82 @@ let add_vpar vi =
   let formals = Cil.getFormalsDecl vi in
   (* Add the vpar formal once *)
   if not (List.exists (fun vi -> vi.vname = vpar_name) formals) then
-  begin
-    (* Register the new formal *)
-    let new_formal = Cil.makeFormalsVarDecl vpar in
-    let new_formals = formals @ [new_formal] in
-    Cil.unsafeSetFormalsDecl vi new_formals
-  end
+    begin
+      (* Register the new formal *)
+      let new_formal = Cil.makeFormalsVarDecl vpar in
+      let new_formals = formals @ [new_formal] in
+      Cil.unsafeSetFormalsDecl vi new_formals
+    end
 
 
 (* Translation of va_* builtins  *)
 
 let translate_va_builtin caller inst =
   let vi, args, loc = match inst with
-  | Call(_, {enode = Lval(Var vi, _)}, args, loc) ->
+    | Call(_, {enode = Lval(Var vi, _)}, args, loc) ->
       vi, args, loc
-  | _ -> assert false
+    | _ -> assert false
   in
 
   let translate_va_start () =
     let va_list = match args with
-    | [{enode=Lval va_list}] -> va_list
-    | _ -> Self.fatal "Unexpected arguments to va_start"
+      | [{enode=Lval va_list}] -> va_list
+      | _ -> Self.fatal "Unexpected arguments to va_start"
     and varg =
       try Extlib.last (Cil.getFormalsDecl caller.svar)
-      with Invalid_argument _ -> Self.abort
-        "Using va_start macro in a function which is not variadic."
+      with Invalid_argument _ ->
+        Self.abort "Using va_start macro in a function which is not variadic."
     in
     [ Set (va_list, Cil.evar ~loc varg, loc) ]
   in
 
   let translate_va_copy () =
     let dest, src = match args with
-    | [{enode=Lval dest}; src] -> dest, src
-    | _ -> Self.fatal "Unexpected arguments to va_copy"
+      | [{enode=Lval dest}; src] -> dest, src
+      | _ -> Self.fatal "Unexpected arguments to va_copy"
     in
     [ Set (dest, src, loc) ]
   in
 
   let translate_va_arg () =
-    let va_list, typ, lval = match args with
-    | [{enode=Lval va_list};
-       {enode=SizeOf typ};
-       {enode=CastE(_, {enode=AddrOf lval})}] -> va_list, typ, lval
-    | _ -> Self.fatal "Unexpected arguments to va_arg"
+    let va_list, ty, lv = match args with
+      | [{enode=Lval va_list};
+         {enode=SizeOf ty};
+         {enode=CastE(_, {enode=AddrOf lv})}] -> va_list, ty, lv
+      | _ -> Self.fatal "Unexpected arguments to va_arg"
     in
     (* Check validity of type *)
-    if Cil.isIntegralType typ then begin
-      let promoted_type = Cil.integralPromotion typ in
-      if promoted_type <> typ then
+    if Cil.isIntegralType ty then begin
+      let promoted_type = Cil.integralPromotion ty in
+      if promoted_type <> ty then
         Self.warning ~current:true
           "Wrong type argument in va_start: %a is promoted to %a when used \
            in the variadic part of the arguments. (You should pass %a to \
            va_start)"
-          Printer.pp_typ typ
+          Printer.pp_typ ty
           Printer.pp_typ promoted_type
           Printer.pp_typ promoted_type
     end;
     (* Build the replacing instruction *)
-    let mk_lval_exp lval = Cil.new_exp ~loc (Lval lval)  in
-    let mk_mem exp = mk_lval_exp (Cil.mkMem ~addr:exp ~off:NoOffset) in
-    let mk_cast exp typ = Cil.mkCast ~force:false ~e:exp ~newt:typ in 
-    let src = mk_mem (mk_cast (mk_mem (mk_lval_exp va_list)) (TPtr (typ,[])))
-    in
-    [ Set (lval, src, loc);
-      Set (va_list, Cil.increm (mk_lval_exp va_list) 1, loc) ]
+    let va_list, ty, lv = Build.(of_lval va_list, of_ctyp ty, of_lval lv) in
+    List.map (Build.cil_instr ~loc) Build.([
+        lv := mem (cast (ptr ty) (mem va_list));
+        va_list += of_int 1
+      ])
   in
 
   begin match vi.vname with
-  | "__builtin_va_start" -> translate_va_start ()
-  | "__builtin_va_copy" -> translate_va_copy ()
-  | "__builtin_va_arg" -> translate_va_arg ()
-  | "__builtin_va_end" -> [] (* No need to do anything for va_end *)
-  | _ -> assert false
+    | "__builtin_va_start" -> translate_va_start ()
+    | "__builtin_va_copy" -> translate_va_copy ()
+    | "__builtin_va_arg" -> translate_va_arg ()
+    | "__builtin_va_end" -> [] (* No need to do anything for va_end *)
+    | _ -> assert false
   end
 
 
 (* Translation of calls to variadic functions *)
 
 let translate_call ~fundec ~ghost block loc mk_call callee pars =
-
   (* Log translation *)
   Self.result ~current:true ~level:2
     "Generic translation of call to variadic function.";
@@ -150,29 +147,23 @@ let translate_call ~fundec ~ghost block loc mk_call callee pars =
   let variadic_size = (List.length r_exps) - (List.length g_params) in
   let v_exps, g_exps = List.break variadic_size r_exps in
 
+  (* Start build *)
+  let module Build = Cil_builder.Stateful (struct let loc = loc end) in
+  Build.open_block ~into:fundec ~ghost ();
+
   (* Create temporary variables to hold parameters *)
-  let add_var i exp =
-    let typ = Cil.typeOf exp
-    and name = "__va_arg" ^ string_of_int i in
-    let res = Cil.makeLocalVar ~ghost fundec ~scope:block name typ in
-    res.vdefined <- true;
-    res
+  let add_var i e =
+    let name = "__va_arg" ^ string_of_int i in
+    Build.(local' (Cil.typeOf e) name ~init:(of_exp e))
   in
   let vis = List.mapi add_var v_exps in
 
-  (* Assign parameters to these *)
-  let instrs = List.map2 (Build.vi_init ~loc) vis v_exps in
-
   (* Build an array to store addresses *)
-  let addrs = List.map Cil.mkAddrOfVi vis in
-  let vargs, assigns = Build.array_init ~loc fundec ~ghost block
-    "__va_args" Cil.voidPtrType addrs
-  in
-  let instrs = instrs @ [assigns] in
+  let ty = Build.(array (ptr void) ~size:(List.length vis)) in
+  let vargs = Build.(local ty "__va_args" ~init:(List.map addr vis)) in
 
   (* Translate the call *)
-  let exp_vargs = Cil.mkAddrOrStartOf ~loc (Cil.var vargs) in
-  let new_arg = Cil.mkCast ~force:false ~e:exp_vargs ~newt:(vpar_typ []) in
-  let new_args = s_exps @ [new_arg] @ g_exps in
-  let call = mk_call callee new_args in
-  instrs @ [call]
+  let new_arg = Build.(cil_exp ~loc (cast' (vpar_typ []) (addr vargs))) in
+  let new_args = (s_exps @ [new_arg] @ g_exps) in
+  Build.of_instr (mk_call callee new_args);
+  Build.finish_instr_list ~scope:block ()

src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle

@@ -25,7 +25,7 @@ int main(void)
 {
   int __retres;
   {
-    void *__va_args[1] = {(void *)0};
+    void *__va_args[0] = {};
     f(1,2,3,(void * const *)(__va_args)) /*@ ghost (4) */;
   }
   __retres = 0;

src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle

@@ -23,7 +23,7 @@ int main(void)
 {
   int __retres;
   {
-    void *__va_args[1] = {(void *)0};
+    void *__va_args[0] = {};
     f(1,2,3,(void * const *)(__va_args));
   }
   __retres = 0;

src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle

@@ -37,7 +37,7 @@ int main(void)
 {
   int tmp;
   {
-    void *__va_args[1] = {(void *)0};
+    void *__va_args[0] = {};
     tmp = sum(0,(void * const *)(__va_args));
   }
   return tmp;

src/plugins/variadic/tests/defined/oracle/recursive.res.oracle

@@ -28,7 +28,7 @@ int f(int a, void * const *__va_params)
   else {
     int tmp;
     {
-      void *__va_args[1] = {(void *)0};
+      void *__va_args[0] = {};
       tmp = f(a - 1,(void * const *)(__va_args));
     }
     __retres = tmp;
@@ -41,7 +41,7 @@ int main(void)
 {
   int tmp;
   {
-    void *__va_args[1] = {(void *)0};
+    void *__va_args[0] = {};
     tmp = f(7,(void * const *)(__va_args));
   }
   return tmp;

src/plugins/variadic/tests/known/oracle/print_libc.pretty.c

@@ -4,14 +4,14 @@
 #include "stddef.h"
 #include "stdio.h"
 /*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns __fc_stdout->__fc_FILE_data, \result;
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
     assigns \result
       \from (indirect: __fc_stdout->__fc_FILE_id),
             (indirect: __fc_stdout->__fc_FILE_data),
             (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
  */
 int printf_va_1(char const * __restrict format);
 
@@ -30,14 +30,14 @@ int main(void)
 #include "stddef.h"
 #include "stdio.h"
 /*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns __fc_stdout->__fc_FILE_data, \result;
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
     assigns \result
       \from (indirect: __fc_stdout->__fc_FILE_id),
             (indirect: __fc_stdout->__fc_FILE_data),
             (indirect: *(format + (0 ..)));
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
  */
 int printf_va_1(char const * __restrict format);
 

src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle

@@ -53,15 +53,15 @@
 extern int ( /* missing proto */ Frama_C_show_each_nb_printed)();
 
 /*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns __fc_stdout->__fc_FILE_data, \result;
     assigns __fc_stdout->__fc_FILE_data
       \from (indirect: __fc_stdout->__fc_FILE_id),
             __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
             param0;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
  */
 int printf_va_1(char const * __restrict format, int param0);
 

src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle

@@ -46,29 +46,29 @@
 #include "stdlib.h"
 #include "sys/types.h"
 /*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: param0);
+    assigns __fc_stdout->__fc_FILE_data, \result;
     assigns __fc_stdout->__fc_FILE_data
       \from (indirect: __fc_stdout->__fc_FILE_id),
             __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
             param0;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param0);
  */
 int printf_va_1(char const * __restrict format, int param0);
 
 /*@ requires valid_read_string(format);
-    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns __fc_stdout->__fc_FILE_data, \result;
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            param1, param0;
     assigns \result
       \from (indirect: __fc_stdout->__fc_FILE_id),
             (indirect: __fc_stdout->__fc_FILE_data),
             (indirect: *(format + (0 ..))), (indirect: param1),
             (indirect: param0);
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            param1, param0;
  */
 int printf_va_2(char const * __restrict format, int param0, int param1);
 

src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle

@@ -52,82 +52,82 @@
 #include "stdarg.h"
 #include "stddef.h"
 #include "stdio.h"
-/*@ requires valid_read_string(format);
-    requires \valid(param0);
+/*@ requires \valid(param0);
+    requires valid_read_string(format);
     ensures \initialized(param0);
-    assigns \result, __fc_stdout->__fc_FILE_data, *param0;
-    assigns \result
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data, *param0, \result;
     assigns __fc_stdout->__fc_FILE_data
       \from (indirect: __fc_stdout->__fc_FILE_id),
             __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
     assigns *param0
       \from (indirect: __fc_stdout->__fc_FILE_id),
             __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_1(char const * __restrict format, int *param0);
-
-/*@ requires valid_read_string(format);
-    requires \valid(param0);
-    ensures \initialized(param0);
-    assigns \result, __fc_stdout->__fc_FILE_data, *param0;
     assigns \result
       \from (indirect: __fc_stdout->__fc_FILE_id),
             (indirect: __fc_stdout->__fc_FILE_data),
             (indirect: *(format + (0 ..)));
+ */
+int printf_va_1(char const * __restrict format, int *param0);
+
+/*@ requires \valid(param0);
+    requires valid_read_string(format);
+    ensures \initialized(param0);
+    assigns __fc_stdout->__fc_FILE_data, *param0, \result;
     assigns __fc_stdout->__fc_FILE_data
       \from (indirect: __fc_stdout->__fc_FILE_id),
             __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
     assigns *param0
       \from (indirect: __fc_stdout->__fc_FILE_id),
             __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_2(char const * __restrict format, int *param0);
-
-/*@ requires valid_read_string(format);
-    requires \valid(param0);
-    ensures \initialized(param0);
-    assigns \result, __fc_stdout->__fc_FILE_data, *param0;
     assigns \result
       \from (indirect: __fc_stdout->__fc_FILE_id),
             (indirect: __fc_stdout->__fc_FILE_data),
             (indirect: *(format + (0 ..)));
+ */
+int printf_va_2(char const * __restrict format, int *param0);
+
+/*@ requires \valid(param0);
+    requires valid_read_string(format);
+    ensures \initialized(param0);
+    assigns __fc_stdout->__fc_FILE_data, *param0, \result;
     assigns __fc_stdout->__fc_FILE_data
       \from (indirect: __fc_stdout->__fc_FILE_id),
             __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
     assigns *param0
       \from (indirect: __fc_stdout->__fc_FILE_id),
             __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
- */
-int printf_va_3(char const * __restrict format, signed char *param0);
-
-/*@ requires valid_read_string(format);
-    requires valid_read_string(param0);
-    assigns \result, __fc_stdout->__fc_FILE_data;
     assigns \result
       \from (indirect: __fc_stdout->__fc_FILE_id),
             (indirect: __fc_stdout->__fc_FILE_data),
-            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
+            (indirect: *(format + (0 ..)));
+ */
+int printf_va_3(char const * __restrict format, signed char *param0);
+
+/*@ requires valid_read_string(param0);
+    requires valid_read_string(format);
+    assigns __fc_stdout->__fc_FILE_data, \result;
     assigns __fc_stdout->__fc_FILE_data
       \from (indirect: __fc_stdout->__fc_FILE_id),
             __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
             *(param0 + (0 ..));
- */
-int printf_va_4(char const * __restrict format, char *param0);
-
-/*@ requires valid_read_string(format);
-    requires valid_read_wstring(param0);
-    assigns \result, __fc_stdout->__fc_FILE_data;
     assigns \result
       \from (indirect: __fc_stdout->__fc_FILE_id),
             (indirect: __fc_stdout->__fc_FILE_data),
             (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
+ */
+int printf_va_4(char const * __restrict format, char *param0);
+
+/*@ requires valid_read_wstring(param0);
+    requires valid_read_string(format);
+    assigns __fc_stdout->__fc_FILE_data, \result;
     assigns __fc_stdout->__fc_FILE_data
       \from (indirect: __fc_stdout->__fc_FILE_id),
             __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
             *(param0 + (0 ..));
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: *(param0 + (0 ..)));
  */
 int printf_va_5(char const * __restrict format, wchar_t *param0);
 

src/plugins/variadic/tests/known/oracle/scanf.res.oracle

@@ -33,17 +33,13 @@
 #include "stdarg.h"
 #include "stddef.h"
 #include "stdio.h"
-/*@ requires valid_read_string(format);
+/*@ requires \valid(param1);
     requires \valid(param2);
-    requires \valid(param1);
-    ensures \initialized(param2);
+    requires valid_read_string(format);
     ensures \initialized(param1);
-    assigns \result, __fc_stdin->__fc_FILE_data, *param2, *param1,
-            *(param0 + (0 ..));
-    assigns \result
-      \from (indirect: __fc_stdin->__fc_FILE_id),
-            (indirect: __fc_stdin->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
+    ensures \initialized(param2);
+    assigns __fc_stdin->__fc_FILE_data, *param2, *param1, *(param0 + (0 ..)),
+            \result;
     assigns __fc_stdin->__fc_FILE_data
       \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
@@ -56,6 +52,10 @@
     assigns *(param0 + (0 ..))
       \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
+    assigns \result
+      \from (indirect: __fc_stdin->__fc_FILE_id),
+            (indirect: __fc_stdin->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
  */
 int scanf_va_1(char const * __restrict format, char *param0, char *param1,
                int *param2);

src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle

@@ -31,20 +31,20 @@
 #include "stddef.h"
 #include "stdio.h"
 int volatile nondet;
-/*@ requires valid_read_string(format);
-    requires \valid(param0);
+/*@ requires \valid(param0);
+    requires valid_read_string(format);
     ensures \initialized(param0);
-    assigns \result, __fc_stdin->__fc_FILE_data, *param0;
-    assigns \result
-      \from (indirect: __fc_stdin->__fc_FILE_id),
-            (indirect: __fc_stdin->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
+    assigns __fc_stdin->__fc_FILE_data, *param0, \result;
     assigns __fc_stdin->__fc_FILE_data
       \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
     assigns *param0
       \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
+    assigns \result
+      \from (indirect: __fc_stdin->__fc_FILE_id),
+            (indirect: __fc_stdin->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
  */
 int scanf_va_1(char const * __restrict format, int *param0);
 

src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle

@@ -34,17 +34,13 @@
 #include "stdarg.h"
 #include "stddef.h"
 #include "stdio.h"
-/*@ requires valid_read_string(format);
+/*@ requires \valid(param1);
     requires \valid(param2);
-    requires \valid(param1);
-    ensures \initialized(param2);
+    requires valid_read_string(format);
     ensures \initialized(param1);
-    assigns \result, __fc_stdin->__fc_FILE_data, *param2, *param1,
-            *(param0 + (0 ..));
-    assigns \result
-      \from (indirect: __fc_stdin->__fc_FILE_id),
-            (indirect: __fc_stdin->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
+    ensures \initialized(param2);
+    assigns __fc_stdin->__fc_FILE_data, *param2, *param1, *(param0 + (0 ..)),
+            \result;
     assigns __fc_stdin->__fc_FILE_data
       \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
@@ -57,6 +53,10 @@
     assigns *(param0 + (0 ..))
       \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
+    assigns \result
+      \from (indirect: __fc_stdin->__fc_FILE_id),
+            (indirect: __fc_stdin->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
  */
 int scanf_va_1(char const * __restrict format, char *param0, char *param1,
                int *param2);

src/plugins/variadic/tests/known/oracle/snprintf.res.oracle

@@ -49,32 +49,32 @@
 #include "string.h"
 #include "strings.h"
 int volatile nondet;
-/*@ requires
+/*@ requires valid_read_string(param0);
+    requires valid_read_string(format);
+    requires
       \valid(s + (0 .. n - 1)) ∨
       \valid(s + (0 .. format_length(format) - 1));
-    requires valid_read_string(format);
-    requires valid_read_string(param0);
-    assigns \result, *(s + (0 ..));
+    assigns *(s + (0 ..)), \result;
+    assigns *(s + (0 ..))
+      \from (indirect: n), (indirect: *(format + (0 ..))), *(param0 + (0 ..));
     assigns \result
       \from (indirect: n), (indirect: *(format + (0 ..))),
             (indirect: *(param0 + (0 ..)));
-    assigns *(s + (0 ..))
-      \from (indirect: n), (indirect: *(format + (0 ..))), *(param0 + (0 ..));
  */
 int snprintf_va_1(char * __restrict s, size_t n,
                   char const * __restrict format, char *param0);
 
-/*@ requires
+/*@ requires valid_read_string(param0);
+    requires valid_read_string(format);
+    requires
       \valid(s + (0 .. n - 1)) ∨
       \valid(s + (0 .. format_length(format) - 1));
-    requires valid_read_string(format);
-    requires valid_read_string(param0);
-    assigns \result, *(s + (0 ..));
+    assigns *(s + (0 ..)), \result;
+    assigns *(s + (0 ..))
+      \from (indirect: n), (indirect: *(format + (0 ..))), *(param0 + (0 ..));
     assigns \result
       \from (indirect: n), (indirect: *(format + (0 ..))),
             (indirect: *(param0 + (0 ..)));
-    assigns *(s + (0 ..))
-      \from (indirect: n), (indirect: *(format + (0 ..))), *(param0 + (0 ..));
  */
 int snprintf_va_2(char * __restrict s, size_t n,
                   char const * __restrict format, char *param0);

src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle

@@ -67,72 +67,72 @@
 #include "stdarg.h"
 #include "stddef.h"
 #include "stdio.h"
-/*@ requires valid_read_string(format);
-    requires valid_read_string(param1);
-    assigns \result, stream->__fc_FILE_data;
+/*@ requires valid_read_string(param1);
+    requires valid_read_string(format);
+    assigns stream->__fc_FILE_data, \result;
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..))), param2, *(param1 + (0 ..)),
+            param0;
     assigns \result
       \from (indirect: stream->__fc_FILE_id),
             (indirect: stream->__fc_FILE_data),
             (indirect: *(format + (0 ..))), (indirect: param2),
             (indirect: *(param1 + (0 ..))), (indirect: param0);
-    assigns stream->__fc_FILE_data
-      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
-            (indirect: *(format + (0 ..))), param2, *(param1 + (0 ..)),
-            param0;
  */
 int fprintf_va_1(FILE * __restrict stream, char const * __restrict format,
                  int param0, char *param1, int param2);
 
-/*@ requires valid_read_string(format);
-    requires valid_read_string(param1);
-    assigns \result, __fc_stdout->__fc_FILE_data;
+/*@ requires valid_read_string(param1);
+    requires valid_read_string(format);
+    assigns __fc_stdout->__fc_FILE_data, \result;
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            param2, *(param1 + (0 ..)), param0;
     assigns \result
       \from (indirect: __fc_stdout->__fc_FILE_id),
             (indirect: __fc_stdout->__fc_FILE_data),
             (indirect: *(format + (0 ..))), (indirect: param2),
             (indirect: *(param1 + (0 ..))), (indirect: param0);
-    assigns __fc_stdout->__fc_FILE_data
-      \from (indirect: __fc_stdout->__fc_FILE_id),
-            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
-            param2, *(param1 + (0 ..)), param0;
  */
 int printf_va_1(char const * __restrict format, int param0, char *param1,
                 int param2);
 
-/*@ requires
+/*@ requires valid_read_string(param1);
+    requires valid_read_string(format);
+    requires
       \valid(s + (0 .. n - 1)) ∨
       \valid(s + (0 .. format_length(format) - 1));
-    requires valid_read_string(format);
-    requires valid_read_string(param1);
-    assigns \result, *(s + (0 ..));
+    assigns *(s + (0 ..)), \result;
+    assigns *(s + (0 ..))
+      \from (indirect: n), (indirect: *(format + (0 ..))), param2,
+            *(param1 + (0 ..)), param0;
     assigns \result
       \from (indirect: n), (indirect: *(format + (0 ..))),
             (indirect: param2), (indirect: *(param1 + (0 ..))),
             (indirect: param0);
-    assigns *(s + (0 ..))
-      \from (indirect: n), (indirect: *(format + (0 ..))), param2,
-            *(param1 + (0 ..)), param0;
  */
 int snprintf_va_1(char * __restrict s, size_t n,
                   char const * __restrict format, int param0, char *param1,
                   int param2);
 
-/*@ requires valid_read_string(format);
-    requires valid_read_string(param1);
-    assigns \result, *(s + (0 ..));
-    assigns \result
-      \from (indirect: *(format + (0 ..))), (indirect: param2),
-            (indirect: *(param1 + (0 ..))), (indirect: param0);
+/*@ requires valid_read_string(param1);
+    requires valid_read_string(format);
+    assigns *(s + (0 ..)), \result;
     assigns *(s + (0 ..))
       \from (indirect: *(format + (0 ..))), param2, *(param1 + (0 ..)),
             param0;
+    assigns \result
+      \from (indirect: *(format + (0 ..))), (indirect: param2),
+            (indirect: *(param1 + (0 ..))), (indirect: param0);
  */
 int sprintf_va_1(char * __restrict s, char const * __restrict format,
                  int param0, char *param1, int param2);
 
-/*@ requires valid_read_string(format);
+/*@ requires valid_read_string(param1);
     requires valid_read_string(param2);
-    requires valid_read_string(param1);
+    requires valid_read_string(format);
     assigns \result;
     assigns \result
       \from (indirect: fd), (indirect: *(format + (0 ..))),

src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle

@@ -51,17 +51,13 @@
 #include "stdarg.h"
 #include "stddef.h"
 #include "stdio.h"
-/*@ requires valid_read_string(format);
+/*@ requires \valid(param0);
     requires \valid(param2);
-    requires \valid(param0);
-    ensures \initialized(param2);
+    requires valid_read_string(format);
     ensures \initialized(param0);
-    assigns \result, stream->__fc_FILE_data, *param2, *(param1 + (0 ..)),
-            *param0;
-    assigns \result
-      \from (indirect: stream->__fc_FILE_id),
-            (indirect: stream->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
+    ensures \initialized(param2);
+    assigns stream->__fc_FILE_data, *param2, *(param1 + (0 ..)), *param0,
+            \result;
     assigns stream->__fc_FILE_data
       \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
@@ -74,21 +70,21 @@
     assigns *param0
       \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
  */
 int fscanf_va_1(FILE * __restrict stream, char const * __restrict format,
                 int *param0, char *param1, int *param2);
 
-/*@ requires valid_read_string(format);
+/*@ requires \valid(param0);
     requires \valid(param2);
-    requires \valid(param0);
-    ensures \initialized(param2);
+    requires valid_read_string(format);
     ensures \initialized(param0);
-    assigns \result, __fc_stdin->__fc_FILE_data, *param2, *(param1 + (0 ..)),
-            *param0;
-    assigns \result
-      \from (indirect: __fc_stdin->__fc_FILE_id),
-            (indirect: __fc_stdin->__fc_FILE_data),
-            (indirect: *(format + (0 ..)));
+    ensures \initialized(param2);
+    assigns __fc_stdin->__fc_FILE_data, *param2, *(param1 + (0 ..)), *param0,
+            \result;
     assigns __fc_stdin->__fc_FILE_data
       \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
@@ -101,25 +97,29 @@ int fscanf_va_1(FILE * __restrict stream, char const * __restrict format,
     assigns *param0
       \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
+    assigns \result
+      \from (indirect: __fc_stdin->__fc_FILE_id),
+            (indirect: __fc_stdin->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
  */
 int scanf_va_1(char const * __restrict format, int *param0, char *param1,
                int *param2);
 
-/*@ requires valid_read_string(s);
-    requires valid_read_string(format);
+/*@ requires \valid(param0);
     requires \valid(param2);
-    requires \valid(param0);
-    ensures \initialized(param2);
+    requires valid_read_string(format);
+    requires valid_read_string(s);
     ensures \initialized(param0);
-    assigns \result, *param2, *(param1 + (0 ..)), *param0;
-    assigns \result
-      \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
+    ensures \initialized(param2);
+    assigns *param2, *(param1 + (0 ..)), *param0, \result;
     assigns *param2
       \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
     assigns *(param1 + (0 ..))
       \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
     assigns *param0
       \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
+    assigns \result
+      \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
  */
 int sscanf_va_1(char const * __restrict s, char const * __restrict format,
                 int *param0, char *param1, int *param2);