diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index c77af9cb63bd8e5d454b7e2e5e588af8f820ec46..e3f5fce6cc868ee3e5e9dc619d71c46652e8101f 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3216,7 +3216,11 @@ let setupBuiltin ?(force_keep=false) name ?spec (resTyp, args_or_argtypes, isva)
| Args args ->
Some (List.map (fun vi -> (vi.vname, vi.vtype, vi.vattr)) args), args
| ArgTypes argTypes ->
- let funargs = List.map (fun at -> ("", at, [])) argTypes in
+ let funargs =
+ List.mapi
+ (fun i at ->
+ ("__x" ^ string_of_int i, at, [Cil.anonymous_attribute])) argTypes
+ in
Some funargs, List.map makeFormalsVarDecl funargs
in
let typ = TFun(resTyp, funargs, isva, []) in
@@ -9230,11 +9234,17 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
(* Create the formals and add them to the environment. *)
(* sfg: extract tsets for the formals from dt *)
+ let cnt = ref 0 in
let doFormal (loc : location) ((fn, ft, fa) as fd) =
let ghost = ghost || isGhostFormalVarDecl fd in
let f = makeVarinfo ~ghost ~temp:false ~loc false true fn ft in
- (f.vattr <- fa;
- alphaConvertVarAndAddToEnv true f)
+ f.vattr <- fa;
+ if f.vname = "" then begin
+ f.vname <- "__x" ^ (string_of_int !cnt);
+ incr cnt;
+ f.vattr <- addAttribute anonymous_attribute f.vattr;
+ end;
+ alphaConvertVarAndAddToEnv true f
in
let rec doFormals fl' ll' =
begin
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 0da9d5eabce3540239f66bfa18bb7c2b22953684..0d20565d540de63b748142d6194a57dd69d4920e 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -2614,15 +2614,6 @@ let equalInitOpts (x: init option) (y: init option) : bool =
| _,_ -> false
end
-let merge_arg_names merged_args curr_args =
- let do_one_arg merged_arg curr_arg =
- (* if curr_arg is also anonymous, this doesn't do much,
- but at least doesn't worsen things. *)
- if merged_arg.vname = "" then merged_arg.vname <- curr_arg.vname
- in
- (* if both list have different lengths, merge should have failed earlier. *)
- List.iter2 do_one_arg merged_args curr_args
-
let update_formals_names merged_vi curr_vi =
(* if the reference varinfo already has formals, everything
is renamed accordingly. However, if the old prototype contains
@@ -2631,7 +2622,7 @@ let update_formals_names merged_vi curr_vi =
match Cil.getFormalsDecl curr_vi with
| curr_args ->
(match Cil.getFormalsDecl merged_vi with
- | merged_args -> merge_arg_names merged_args curr_args
+ | _ -> ()
| exception Not_found ->
(*existing prototype does not have formals list. Just use current one*)
Cil.unsafeSetFormalsDecl merged_vi curr_args)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index a71f6f3f5a9e64ed407958e9d70d2f5227de2a86..60d0eeb0404ae44a52f0021239714bfc4ad6ff5a 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -120,6 +120,7 @@ let () = register_shallow_attribute Cil.frama_c_ghost_formal
let () = register_shallow_attribute Cil.frama_c_mutable
let () = register_shallow_attribute Cil.frama_c_init_obj
let () = register_shallow_attribute Cil.frama_c_inlined
+let () = register_shallow_attribute Cil.anonymous_attribute_name
let keep_attr = function
| Attr _ as a -> not (List.mem (Cil.attributeName a) !reserved_attributes)
@@ -729,14 +730,20 @@ class cil_printer () = object (self)
end
else v
in
+ let name =
+ if Cil.hasAttribute Cil.anonymous_attribute_name v.vattr
+ && not v.vreferenced && not state.print_cil_as_is
+ then
+ None
+ else Some (fun fmt -> self#varinfo fmt v)
+ in
(* First the storage modifiers *)
fprintf fmt "%s%a%a%s%a%a"
(if v.vinline then "__inline " else "")
self#storage v.vstorage
self#attributes stom
(if stom = [] then "" else " ")
- (self#typ ?fundecl
- (if v.vname = "" then None else Some (fun fmt -> self#varinfo fmt v)))
+ (self#typ ?fundecl name)
v.vtype
self#attributes rest
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index a1f3467b9489bfa294a67c5a0fa9dd8f7ffa53b9..695600d6793e3315cf8301ee56e07dade97e4744 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -300,6 +300,9 @@ let stmt_of_instr_list ?(loc=Location.unknown) = function
let bitfield_attribute_name = "FRAMA_C_BITFIELD_SIZE"
+let anonymous_attribute_name = "__fc_anonymous"
+let anonymous_attribute = Attr(anonymous_attribute_name, [])
+
(** Construct sorted lists of attributes ***)
let attributeName =
function Attr(a, _) | AttrAnnot a -> Extlib.strip_underscore a
@@ -725,8 +728,16 @@ let setFormalsDecl vi typ =
match unrollType typ with
| TFun(_, Some args, _, _) ->
let is_ghost d = vi.vghost || isGhostFormalVarDecl d in
- let makeFormalsVarDecl x = makeFormalsVarDecl ~ghost:(is_ghost x) x in
- FormalsDecl.replace vi (List.map makeFormalsVarDecl args)
+ let makeFormalsVarDecl i (n,t,a as x) =
+ let x = if n = "" then begin
+ let a = addAttribute anonymous_attribute a in
+ "__x" ^ string_of_int i,t,a
+ end
+ else x
+ in
+ makeFormalsVarDecl ~ghost:(is_ghost x) x
+ in
+ FormalsDecl.replace vi (List.mapi makeFormalsVarDecl args)
| TFun(_,None,_,_) -> ()
| _ ->
Kernel.error ~current:true
@@ -6234,7 +6245,9 @@ let uniqueVarNames (f: file) : unit =
let processLocal (v: varinfo) =
(* start from original name to avoid putting another _0 in case
of conflicts. *)
- let lookupname = v.vorig_name in
+ let lookupname =
+ if v.vorig_name = "" then v.vname else v.vorig_name
+ in
let data = CurrentLoc.get () in
let newname, oldloc =
Alpha.newAlphaName
@@ -6745,6 +6758,12 @@ let create_alpha_renaming old_args new_args =
List.iter2
(fun old_vi new_vi ->
Hashtbl.add conversion old_vi.vid new_vi;
+ if hasAttribute anonymous_attribute_name new_vi.vattr &&
+ not (hasAttribute anonymous_attribute_name old_vi.vattr)
+ then begin
+ new_vi.vname <- old_vi.vname;
+ new_vi.vattr <- dropAttribute anonymous_attribute_name new_vi.vattr;
+ end;
match old_vi.vlogic_var_assoc, new_vi.vlogic_var_assoc with
| None, _ -> () (* nothing to convert in logic spec. *)
| Some old_lv, Some new_lv ->
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 2f3a0822bef32574efd959a4257dded2b0d81159..8f83ecbc8bee2cb5310a838a341e18069184317a 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1424,6 +1424,17 @@ val bitfield_attribute_name: string
(** Name of the attribute that is automatically inserted (with an [AINT size]
argument when querying the type of a field that is a bitfield *)
+val anonymous_attribute_name: string
+(** Name of the attribute that is inserted when generating a name for a varinfo
+ representing an anonymous function parameter.
+ @since Frama-C+dev
+*)
+
+val anonymous_attribute: attribute
+(** attribute identifying anonymous function parameters
+ @since Frama-C+dev
+*)
+
(** Convert an expression into an attrparam, if possible. Otherwise raise
NotAnAttrParam with the offending subexpression *)
val expToAttrParam: exp -> attrparam
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index b8e8cae1f28b5a1714c302d37e24b493903d9d5e..2aaec4541364d087d3d0b4ba1a493704d68f6686 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -125,6 +125,9 @@ module Base_checker = struct
method! vvdec v =
Kernel.debug
~dkey:Kernel.dkey_check "Declaration of %s(%d)" v.vname v.vid;
+ if v.vname = "" then
+ check_abort "variable of id %d and type %a has an empty name"
+ v.vid Cil_datatype.Typ.pretty v.vtype;
if Varinfo.Hashtbl.mem known_vars v then
(let v' = Varinfo.Hashtbl.find known_vars v in
if v != v' then (* we can see the declaration twice
@@ -193,6 +196,8 @@ module Base_checker = struct
Cil.DoChildren
method! vlogic_var_decl lv =
+ if lv.lv_name = "" then
+ check_abort "logic variable of id %d has an empty name" lv.lv_id;
Logic_var.Hashtbl.add known_logic_vars lv lv;
match lv.lv_origin with
(* lvkind for purely logical variables is checked at the parent level. *)
diff --git a/src/kernel_services/ast_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index 43304358b4c7d8754eeae30674ae4909ba0d4e3b..84a83e8b7e20f75d55ee044d5e7195410e184318 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -831,6 +831,11 @@ end = struct
Cil.update_var_type new_var mytype;
List.iter2
(fun x y ->
+ if y.vname = "" then begin
+ y.vname <- x.vname;
+ if hasAttribute anonymous_attribute_name x.vattr then
+ y.vattr <- addAttribute anonymous_attribute y.vattr;
+ end;
Visitor_behavior.Set.varinfo self#behavior x y;
Visitor_behavior.Set_orig.varinfo self#behavior y x;
match x.vlogic_var_assoc with
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index 14cc5ce21320519c1aa8484d60fd8430cc589777..4cd812ec3d82c2e17440adb142995f8d54b9c13e 100644
--- a/src/plugins/variadic/standard.ml
+++ b/src/plugins/variadic/standard.ml
@@ -462,18 +462,27 @@ let build_specialized_fun env vf format_fun tvparams =
Build.add_stdlib_generated ();
(* Add parameters *)
+ let fresh_param_name =
+ let counter = ref 0 in
+ fun () ->
+ let p = "param" ^ string_of_int !counter in
+ incr counter;
+ p
+ in
let add_static_param (name,typ,attributes) =
+ (* create a new name for parameters which does not have one *)
+ let name = if name = "" then fresh_param_name () else name in
Build.parameter ~attributes typ name
- and add_variadic_param i (typ,_dir) =
+ and add_variadic_param (typ,_dir) =
let typ = if Cil.isIntegralType typ then
Cil.integralPromotion typ
else
typ
in
- Build.parameter typ ("param" ^ string_of_int i)
+ Build.parameter typ (fresh_param_name ())
in
let sformals = List.map add_static_param (Option.get params)
- and vformals = List.mapi add_variadic_param tvparams
+ and vformals = List.map add_variadic_param tvparams
in
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
index 77d342b3dd8113ce3c181cca5993138243e6bbe4..179380e42d59c545cf1035fe08e04769d45155c8 100644
--- a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
@@ -18,7 +18,7 @@
behavior bhv:
requires c > 0;
requires a ≤ 42; */
-void f(int const a, int, int c, void * const *__va_params)
+void f(int const a, int __x1, int c, void * const *__va_params)
/*@ ghost (int x) */;
int main(void)
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
index c028e9e151d91ac8f3d848668a9ead0863bef9f1..c747e92c44eae658143432e49fcd1574c0fb8988 100644
--- a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
@@ -17,7 +17,7 @@
behavior bhv:
requires c > 0;
requires a ≤ 42; */
-void f(int const a, int, int c, void * const *__va_params);
+void f(int const a, int __x1, int c, void * const *__va_params);
int main(void)
{
diff --git a/src/plugins/variadic/tests/declared/oracle/label.res.oracle b/src/plugins/variadic/tests/declared/oracle/label.res.oracle
index 427868a9c76ae47b935ff087454c0ef2b589dc3d..2de09b271e78448da9d97031e7d05fce8608b3f8 100644
--- a/src/plugins/variadic/tests/declared/oracle/label.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/label.res.oracle
@@ -13,7 +13,7 @@
__retres ∈ {0}
/* Generated by Frama-C */
/*@ assigns \result;
- assigns \result \from \nothing; */
+ assigns \result \from __x0; */
int f(int, void * const *__va_params);
int main(void)
diff --git a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
index adcbb2b04d43ce39487600c92e43c8f4c6d65a55..0cf3b24972f4204f3431dceb595d5c56b4b040a7 100644
--- a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
@@ -23,14 +23,14 @@
/* Generated by Frama-C */
/*@ assigns \result;
- assigns \result \from a, c;
+ assigns \result \from a, __x1, c;
behavior bhv1:
requires c > 0;
requires a ≤ 42;
ensures \result > 0;
*/
-int f(int const a, int, int c, void * const *__va_params);
+int f(int const a, int __x1, int c, void * const *__va_params);
int call1(void)
{
diff --git a/src/plugins/variadic/tests/declared/oracle/redefine_anonymous_parameters.res.oracle b/src/plugins/variadic/tests/declared/oracle/redefine_anonymous_parameters.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ae66c74da91293f7c7a4f6e550d3b3de3764f02b
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/oracle/redefine_anonymous_parameters.res.oracle
@@ -0,0 +1,26 @@
+[variadic] tests/declared/redefine_anonymous_parameters.i:1:
+ Declaration of variadic function printf.
+[variadic] Warning: Unable to locate ACSL predicate valid_read_string which should be in the Frama-C LibC. Correct specifications can't be generated.
+[variadic] Warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.
+[variadic] tests/declared/redefine_anonymous_parameters.i:4:
+ Translating call to printf to a call to the specialized version printf_va_1.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva] using specification for function printf_va_1
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+
+/* Generated by Frama-C */
+/*@ assigns \result;
+ assigns \result \from (indirect: *(param0 + (0 ..))); */
+int printf_va_1(char *param0);
+
+void main(void)
+{
+ printf((char *)""); /* printf_va_1 */
+ return;
+}
+
+
diff --git a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
index fa2e63b8a114173eac0d131f2fe7c203d8ef6592..afe3fe0a174a0b03f4b921571d02f921451a87cd 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
@@ -14,14 +14,14 @@
/* Generated by Frama-C */
/*@ assigns \result;
- assigns \result \from a, c;
+ assigns \result \from a, __x1, c;
behavior bhv:
requires c > 0;
requires a ≤ 42;
ensures \result > 0;
*/
-int f(int const a, int, int c, void * const *__va_params)
+int f(int const a, int __x1, int c, void * const *__va_params)
/*@ ghost (int x) */;
int main(void)
diff --git a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
index 9112e9470077a769eaa504faed32bb9cf3caf757..d1ed1eec99ada14fcdb114282bc3b17bf4a17dd1 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
@@ -13,14 +13,14 @@
/* Generated by Frama-C */
/*@ assigns \result;
- assigns \result \from a, c;
+ assigns \result \from a, __x1, c;
behavior bhv:
requires c > 0;
requires a ≤ 42;
ensures \result > 0;
*/
-int f(int const a, int, int c, void * const *__va_params);
+int f(int const a, int __x1, int c, void * const *__va_params);
int main(void)
{
diff --git a/src/plugins/variadic/tests/declared/redefine_anonymous_parameters.i b/src/plugins/variadic/tests/declared/redefine_anonymous_parameters.i
new file mode 100644
index 0000000000000000000000000000000000000000..c9f4440de15d5bcaa007f661d1a449771a86c1a2
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/redefine_anonymous_parameters.i
@@ -0,0 +1,5 @@
+int printf (char*, ...);
+
+void main(void) {
+ printf("");
+}
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index b647d40caefdab3371fc969f9c085857e3964a42..033244bd8fd3ea79f4f2712c84d403e0f8ceb97a 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1565,7 +1565,7 @@ extern int execvp(char const *path, char * const *argv);
/*@ ensures never_terminates: \false;
assigns \nothing; */
-extern __attribute__((__noreturn__)) void _exit(int);
+extern __attribute__((__noreturn__)) void _exit(int __x0);
/*@ ensures
result_ok_child_or_error:
@@ -1635,7 +1635,7 @@ extern pid_t getppid(void);
/*@ assigns \result;
assigns \result \from \nothing; */
-extern pid_t getsid(pid_t);
+extern pid_t getsid(pid_t __x0);
/*@ assigns \result;
assigns \result \from \nothing; */
@@ -7988,7 +7988,7 @@ extern size_t iconv(iconv_t cd, char ** restrict inbuf,
/*@ ensures result_zero_or_neg: \result ≡ 0 ∨ \result ≡ -1;
assigns __fc_errno;
*/
-extern int iconv_close(iconv_t);
+extern int iconv_close(iconv_t __x0);
/*@ assigns \result, __fc_errno;
assigns \result \from *(tocode + (..)), *(fromcode + (..));
@@ -8293,16 +8293,16 @@ CODE prioritynames[13] =
extern void closelog(void);
/*@ assigns \nothing; */
-extern void openlog(char const *, int, int);
+extern void openlog(char const *__x0, int __x1, int __x2);
/*@ assigns \nothing; */
-extern int setlogmask(int);
+extern int setlogmask(int __x0);
/*@ assigns \nothing; */
-extern void syslog(int, char const *, void * const *__va_params);
+extern void syslog(int __x0, char const *__x1, void * const *__va_params);
/*@ assigns \nothing; */
-extern void vsyslog(int, char const *, va_list);
+extern void vsyslog(int __x0, char const *__x1, va_list __x2);
/*@ assigns \result;
assigns \result \from which, who; */
diff --git a/tests/slicing/oracle/unravel-point.0.res.oracle b/tests/slicing/oracle/unravel-point.0.res.oracle
index 892a13dfd9ace31ff1d20e9ea6bf2f8dbf31a767..3fda244140018eb16df637b2ed60a6af651656af 100644
--- a/tests/slicing/oracle/unravel-point.0.res.oracle
+++ b/tests/slicing/oracle/unravel-point.0.res.oracle
@@ -81,13 +81,13 @@
[eva] done for function main
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to printf at tests/slicing/unravel-point.i:36 (by send1):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:40 (by send2):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:44 (by send3):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:48 (by send4):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to scanf at tests/slicing/unravel-point.i:59 (by main):
input1 FROM \nothing
\result FROM ANYTHING(origin:Unknown)
diff --git a/tests/slicing/oracle/unravel-point.1.res.oracle b/tests/slicing/oracle/unravel-point.1.res.oracle
index 1d4a3d5acbd379698c91599a347b835e0201ffb1..a890fa20e816504cc01ced6ece96931c5f5e85e7 100644
--- a/tests/slicing/oracle/unravel-point.1.res.oracle
+++ b/tests/slicing/oracle/unravel-point.1.res.oracle
@@ -81,13 +81,13 @@
[eva] done for function main
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to printf at tests/slicing/unravel-point.i:36 (by send1):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:40 (by send2):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:44 (by send3):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:48 (by send4):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to scanf at tests/slicing/unravel-point.i:59 (by main):
input1 FROM \nothing
\result FROM ANYTHING(origin:Unknown)
diff --git a/tests/slicing/oracle/unravel-point.2.res.oracle b/tests/slicing/oracle/unravel-point.2.res.oracle
index 695f510a073771b8f3c202fd21a709f25b5ce3c3..b9b817c3f6cb242ba295dced6a0482662923ee03 100644
--- a/tests/slicing/oracle/unravel-point.2.res.oracle
+++ b/tests/slicing/oracle/unravel-point.2.res.oracle
@@ -81,13 +81,13 @@
[eva] done for function main
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to printf at tests/slicing/unravel-point.i:36 (by send1):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:40 (by send2):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:44 (by send3):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:48 (by send4):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to scanf at tests/slicing/unravel-point.i:59 (by main):
input1 FROM \nothing
\result FROM ANYTHING(origin:Unknown)
diff --git a/tests/slicing/oracle/unravel-point.3.res.oracle b/tests/slicing/oracle/unravel-point.3.res.oracle
index 4f09e01392e10705ddaa3beab3de59944e7d8ea4..97ac7856428adf3214cbe7b0dbc37de08d8b6c8f 100644
--- a/tests/slicing/oracle/unravel-point.3.res.oracle
+++ b/tests/slicing/oracle/unravel-point.3.res.oracle
@@ -81,13 +81,13 @@
[eva] done for function main
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to printf at tests/slicing/unravel-point.i:36 (by send1):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:40 (by send2):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:44 (by send3):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:48 (by send4):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to scanf at tests/slicing/unravel-point.i:59 (by main):
input1 FROM \nothing
\result FROM ANYTHING(origin:Unknown)
diff --git a/tests/slicing/oracle/unravel-point.4.res.oracle b/tests/slicing/oracle/unravel-point.4.res.oracle
index 1f8cdc7191b0682e09fcee2d185d1b79f63d7be6..111fe11a744d9eafc4cf108de952f63668306c03 100644
--- a/tests/slicing/oracle/unravel-point.4.res.oracle
+++ b/tests/slicing/oracle/unravel-point.4.res.oracle
@@ -81,13 +81,13 @@
[eva] done for function main
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to printf at tests/slicing/unravel-point.i:36 (by send1):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:40 (by send2):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:44 (by send3):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to printf at tests/slicing/unravel-point.i:48 (by send4):
- \result FROM \nothing
+ \result FROM __x1; "%d\n"
[from] call to scanf at tests/slicing/unravel-point.i:59 (by main):
input1 FROM \nothing
\result FROM ANYTHING(origin:Unknown)
@@ -189,20 +189,20 @@
[eva] done for function main
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to scanf at tests/slicing/unravel-point.i:59 (by main):
- input1 FROM input1 (and SELF)
- \result FROM input1
+ input1 FROM input1; "%d"[bits 0 to 23] (and SELF)
+ \result FROM input1; "%d"[bits 0 to 23]
[from] call to scanf at tests/slicing/unravel-point.i:61 (by main):
- input2 FROM input2 (and SELF)
- \result FROM input2
+ input2 FROM input2; "%d"[bits 0 to 23] (and SELF)
+ \result FROM input2; "%d"[bits 0 to 23]
[from] call to scanf at tests/slicing/unravel-point.i:63 (by main):
- input3 FROM input3 (and SELF)
- \result FROM input3
+ input3 FROM input3; "%d"[bits 0 to 23] (and SELF)
+ \result FROM input3; "%d"[bits 0 to 23]
[from] call to scanf at tests/slicing/unravel-point.i:65 (by main):
- cond1 FROM cond1 (and SELF)
- \result FROM cond1
+ cond1 FROM cond1; "%d"[bits 0 to 23] (and SELF)
+ \result FROM cond1; "%d"[bits 0 to 23]
[from] call to scanf at tests/slicing/unravel-point.i:66 (by main):
- cond2 FROM cond2 (and SELF)
- \result FROM cond2
+ cond2 FROM cond2; "%d"[bits 0 to 23] (and SELF)
+ \result FROM cond2; "%d"[bits 0 to 23]
[from] call to send1_slice_1 at tests/slicing/unravel-point.i:75 (by main):
\result FROM x
[from] call to send4_slice_1 at tests/slicing/unravel-point.i:78 (by main):
@@ -229,8 +229,9 @@
[sparecode] removed unused global declarations in new project 'Slicing export'
/* Generated by Frama-C */
/*@ assigns \result, *p;
- assigns \result \from *p;
- assigns *p \from *p; */
+ assigns \result \from *(__x0 + (0 ..)), *p;
+ assigns *p \from *(__x0 + (0 ..)), *p;
+ */
int scanf(char const *, int *p);
int send1_slice_1(int x)
diff --git a/tests/spec/oracle/unused.res.oracle b/tests/spec/oracle/unused.res.oracle
index c28824052ed4446fdf10c762e1d7ff2a44fe9876..1853a1ef2a9e02473873c63fbc13014c2c364c61 100644
--- a/tests/spec/oracle/unused.res.oracle
+++ b/tests/spec/oracle/unused.res.oracle
@@ -15,6 +15,6 @@ static int i;
extern int c;
/*@ requires c ≡ 0; */
- __attribute__((__FC_BUILTIN__)) void foo(int *);
+ __attribute__((__FC_BUILTIN__)) void foo(int *__x0);
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index 510a8f2b3ab41a3c39cd5c26cc41c8703528b9e1..e3f67044af38fd7e0b6bc3940c501fb55455fc03 100644
--- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle
+++ b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
@@ -2,232 +2,239 @@
[kernel:file:print-one]
result of parsing tests/syntax/check_builtin_bts1440.i:
/* Generated by Frama-C */
- void __builtin__Exit(int);
+ void __builtin__Exit(int __x0);
- int __builtin___fprintf_chk(void *, int, char const * , ...);
+ int __builtin___fprintf_chk(void *__x0, int __x1, char const *__x2 , ...);
- void *__builtin___memcpy_chk(void *, void const *, unsigned int, unsigned int);
+ void *__builtin___memcpy_chk(void *__x0, void const *__x1, unsigned int __x2,
+ unsigned int __x3);
- void *__builtin___memmove_chk(void *, void const *, unsigned int,
- unsigned int);
+ void *__builtin___memmove_chk(void *__x0, void const *__x1,
+ unsigned int __x2, unsigned int __x3);
- void *__builtin___mempcpy_chk(void *, void const *, unsigned int,
- unsigned int);
+ void *__builtin___mempcpy_chk(void *__x0, void const *__x1,
+ unsigned int __x2, unsigned int __x3);
- void *__builtin___memset_chk(void *, int, unsigned int, unsigned int);
+ void *__builtin___memset_chk(void *__x0, int __x1, unsigned int __x2,
+ unsigned int __x3);
- int __builtin___printf_chk(int, char const * , ...);
+ int __builtin___printf_chk(int __x0, char const *__x1 , ...);
- int __builtin___snprintf_chk(char *, unsigned int, int, unsigned int,
- char const * , ...);
+ int __builtin___snprintf_chk(char *__x0, unsigned int __x1, int __x2,
+ unsigned int __x3, char const *__x4 , ...);
- int __builtin___sprintf_chk(char *, int, unsigned int, char const * , ...);
+ int __builtin___sprintf_chk(char *__x0, int __x1, unsigned int __x2,
+ char const *__x3 , ...);
- char *__builtin___stpcpy_chk(char *, char const *, unsigned int);
+ char *__builtin___stpcpy_chk(char *__x0, char const *__x1, unsigned int __x2);
- char *__builtin___strcat_chk(char *, char const *, unsigned int);
+ char *__builtin___strcat_chk(char *__x0, char const *__x1, unsigned int __x2);
- char *__builtin___strcpy_chk(char *, char const *, unsigned int);
+ char *__builtin___strcpy_chk(char *__x0, char const *__x1, unsigned int __x2);
- char *__builtin___strncat_chk(char *, char const *, unsigned int,
- unsigned int);
+ char *__builtin___strncat_chk(char *__x0, char const *__x1,
+ unsigned int __x2, unsigned int __x3);
- char *__builtin___strncpy_chk(char *, char const *, unsigned int,
- unsigned int);
+ char *__builtin___strncpy_chk(char *__x0, char const *__x1,
+ unsigned int __x2, unsigned int __x3);
- int __builtin___vfprintf_chk(void *, int, char const *, __builtin_va_list);
+ int __builtin___vfprintf_chk(void *__x0, int __x1, char const *__x2,
+ __builtin_va_list __x3);
- int __builtin___vprintf_chk(int, char const *, __builtin_va_list);
+ int __builtin___vprintf_chk(int __x0, char const *__x1,
+ __builtin_va_list __x2);
- int __builtin___vsnprintf_chk(char *, unsigned int, int, unsigned int,
- char const *, __builtin_va_list);
+ int __builtin___vsnprintf_chk(char *__x0, unsigned int __x1, int __x2,
+ unsigned int __x3, char const *__x4,
+ __builtin_va_list __x5);
- int __builtin___vsprintf_chk(char *, int, unsigned int, char const *,
- __builtin_va_list);
+ int __builtin___vsprintf_chk(char *__x0, int __x1, unsigned int __x2,
+ char const *__x3, __builtin_va_list __x4);
- int __builtin_abs(int);
+ int __builtin_abs(int __x0);
- double __builtin_acos(double);
+ double __builtin_acos(double __x0);
- float __builtin_acosf(float);
+ float __builtin_acosf(float __x0);
- double __builtin_acosh(double);
+ double __builtin_acosh(double __x0);
- float __builtin_acoshf(float);
+ float __builtin_acoshf(float __x0);
- long double __builtin_acoshl(long double);
+ long double __builtin_acoshl(long double __x0);
- long double __builtin_acosl(long double);
+ long double __builtin_acosl(long double __x0);
- void *__builtin_alloca(unsigned int);
+ void *__builtin_alloca(unsigned int __x0);
- double __builtin_asin(double);
+ double __builtin_asin(double __x0);
- float __builtin_asinf(float);
+ float __builtin_asinf(float __x0);
- double __builtin_asinh(double);
+ double __builtin_asinh(double __x0);
- float __builtin_asinhf(float);
+ float __builtin_asinhf(float __x0);
- long double __builtin_asinhl(long double);
+ long double __builtin_asinhl(long double __x0);
- long double __builtin_asinl(long double);
+ long double __builtin_asinl(long double __x0);
- double __builtin_atan(double);
+ double __builtin_atan(double __x0);
- double __builtin_atan2(double, double);
+ double __builtin_atan2(double __x0, double __x1);
- float __builtin_atan2f(float, float);
+ float __builtin_atan2f(float __x0, float __x1);
- long double __builtin_atan2l(long double, long double);
+ long double __builtin_atan2l(long double __x0, long double __x1);
- float __builtin_atanf(float);
+ float __builtin_atanf(float __x0);
- double __builtin_atanh(double);
+ double __builtin_atanh(double __x0);
- float __builtin_atanhf(float);
+ float __builtin_atanhf(float __x0);
- long double __builtin_atanhl(long double);
+ long double __builtin_atanhl(long double __x0);
- long double __builtin_atanl(long double);
+ long double __builtin_atanl(long double __x0);
- unsigned short __builtin_bswap16(unsigned short);
+ unsigned short __builtin_bswap16(unsigned short __x0);
- unsigned int __builtin_bswap32(unsigned int);
+ unsigned int __builtin_bswap32(unsigned int __x0);
- unsigned long long __builtin_bswap64(unsigned long long);
+ unsigned long long __builtin_bswap64(unsigned long long __x0);
- void *__builtin_calloc(unsigned int, unsigned int);
+ void *__builtin_calloc(unsigned int __x0, unsigned int __x1);
- double __builtin_cbrt(double);
+ double __builtin_cbrt(double __x0);
- float __builtin_cbrtf(float);
+ float __builtin_cbrtf(float __x0);
- long double __builtin_cbrtl(long double);
+ long double __builtin_cbrtl(long double __x0);
- double __builtin_ceil(double);
+ double __builtin_ceil(double __x0);
- float __builtin_ceilf(float);
+ float __builtin_ceilf(float __x0);
- long double __builtin_ceill(long double);
+ long double __builtin_ceill(long double __x0);
- int __builtin_constant_p(int);
+ int __builtin_constant_p(int __x0);
- double __builtin_copysign(double, double);
+ double __builtin_copysign(double __x0, double __x1);
- float __builtin_copysignf(float, float);
+ float __builtin_copysignf(float __x0, float __x1);
- long double __builtin_copysignl(long double, long double);
+ long double __builtin_copysignl(long double __x0, long double __x1);
- double __builtin_cos(double);
+ double __builtin_cos(double __x0);
- float __builtin_cosf(float);
+ float __builtin_cosf(float __x0);
- double __builtin_cosh(double);
+ double __builtin_cosh(double __x0);
- float __builtin_coshf(float);
+ float __builtin_coshf(float __x0);
- long double __builtin_coshl(long double);
+ long double __builtin_coshl(long double __x0);
- long double __builtin_cosl(long double);
+ long double __builtin_cosl(long double __x0);
- double __builtin_erf(double);
+ double __builtin_erf(double __x0);
- double __builtin_erfc(double);
+ double __builtin_erfc(double __x0);
- float __builtin_erfcf(float);
+ float __builtin_erfcf(float __x0);
- long double __builtin_erfcl(long double);
+ long double __builtin_erfcl(long double __x0);
- float __builtin_erff(float);
+ float __builtin_erff(float __x0);
- long double __builtin_erfl(long double);
+ long double __builtin_erfl(long double __x0);
- void __builtin_exit(int);
+ void __builtin_exit(int __x0);
- double __builtin_exp(double);
+ double __builtin_exp(double __x0);
- double __builtin_exp2(double);
+ double __builtin_exp2(double __x0);
- float __builtin_exp2f(float);
+ float __builtin_exp2f(float __x0);
- long double __builtin_exp2l(long double);
+ long double __builtin_exp2l(long double __x0);
- long __builtin_expect(long, long);
+ long __builtin_expect(long __x0, long __x1);
- float __builtin_expf(float);
+ float __builtin_expf(float __x0);
- long double __builtin_expl(long double);
+ long double __builtin_expl(long double __x0);
- double __builtin_expm1(double);
+ double __builtin_expm1(double __x0);
- float __builtin_expm1f(float);
+ float __builtin_expm1f(float __x0);
- long double __builtin_expm1l(long double);
+ long double __builtin_expm1l(long double __x0);
- double __builtin_fabs(double);
+ double __builtin_fabs(double __x0);
- float __builtin_fabsf(float);
+ float __builtin_fabsf(float __x0);
- long double __builtin_fabsl(long double);
+ long double __builtin_fabsl(long double __x0);
- double __builtin_fdim(double, double);
+ double __builtin_fdim(double __x0, double __x1);
- float __builtin_fdimf(float, float);
+ float __builtin_fdimf(float __x0, float __x1);
- long double __builtin_fdiml(long double, long double);
+ long double __builtin_fdiml(long double __x0, long double __x1);
- int __builtin_ffs(unsigned int);
+ int __builtin_ffs(unsigned int __x0);
- int __builtin_ffsl(unsigned long);
+ int __builtin_ffsl(unsigned long __x0);
- int __builtin_ffsll(unsigned long long);
+ int __builtin_ffsll(unsigned long long __x0);
- double __builtin_floor(double);
+ double __builtin_floor(double __x0);
- float __builtin_floorf(float);
+ float __builtin_floorf(float __x0);
- long double __builtin_floorl(long double);
+ long double __builtin_floorl(long double __x0);
- double __builtin_fma(double, double, double);
+ double __builtin_fma(double __x0, double __x1, double __x2);
- float __builtin_fmaf(float, float, float);
+ float __builtin_fmaf(float __x0, float __x1, float __x2);
- long double __builtin_fmal(long double, long double, long double);
+ long double __builtin_fmal(long double __x0, long double __x1,
+ long double __x2);
- double __builtin_fmax(double, double);
+ double __builtin_fmax(double __x0, double __x1);
- float __builtin_fmaxf(float, float);
+ float __builtin_fmaxf(float __x0, float __x1);
- long double __builtin_fmaxl(long double, long double);
+ long double __builtin_fmaxl(long double __x0, long double __x1);
- double __builtin_fmin(double, double);
+ double __builtin_fmin(double __x0, double __x1);
- float __builtin_fminf(float, float);
+ float __builtin_fminf(float __x0, float __x1);
- long double __builtin_fminl(long double, long double);
+ long double __builtin_fminl(long double __x0, long double __x1);
- double __builtin_fmod(double);
+ double __builtin_fmod(double __x0);
- float __builtin_fmodf(float);
+ float __builtin_fmodf(float __x0);
- long double __builtin_fmodl(long double);
+ long double __builtin_fmodl(long double __x0);
- int __builtin_fprintf(void *, char const * , ...);
+ int __builtin_fprintf(void *__x0, char const *__x1 , ...);
- int __builtin_fputs(char const *, void *);
+ int __builtin_fputs(char const *__x0, void *__x1);
- void *__builtin_frame_address(unsigned int);
+ void *__builtin_frame_address(unsigned int __x0);
- void __builtin_free(void *);
+ void __builtin_free(void *__x0);
- double __builtin_frexp(double, int *);
+ double __builtin_frexp(double __x0, int *__x1);
- float __builtin_frexpf(float, int *);
+ float __builtin_frexpf(float __x0, int *__x1);
- long double __builtin_frexpl(long double, int *);
+ long double __builtin_frexpl(long double __x0, int *__x1);
- int __builtin_fscanf(void *, char const * , ...);
+ int __builtin_fscanf(void *__x0, char const *__x1 , ...);
double __builtin_huge_val(void);
@@ -235,11 +242,11 @@
long double __builtin_huge_vall(void);
- double __builtin_hypot(double, double);
+ double __builtin_hypot(double __x0, double __x1);
- float __builtin_hypotf(float, float);
+ float __builtin_hypotf(float __x0, float __x1);
- long double __builtin_hypotl(long double, long double);
+ long double __builtin_hypotl(long double __x0, long double __x1);
void __builtin_ia32_lfence(void);
@@ -247,11 +254,11 @@
void __builtin_ia32_sfence(void);
- double __builtin_ilogb(double);
+ double __builtin_ilogb(double __x0);
- float __builtin_ilogbf(float);
+ float __builtin_ilogbf(float __x0);
- long double __builtin_ilogbl(long double);
+ long double __builtin_ilogbl(long double __x0);
double __builtin_inf(void);
@@ -259,677 +266,710 @@
long double __builtin_infl(void);
- int __builtin_isalnum(int);
+ int __builtin_isalnum(int __x0);
- int __builtin_isalpha(int);
+ int __builtin_isalpha(int __x0);
- int __builtin_isblank(int);
+ int __builtin_isblank(int __x0);
- int __builtin_iscntrl(int);
+ int __builtin_iscntrl(int __x0);
- int __builtin_isdigit(int);
+ int __builtin_isdigit(int __x0);
- int __builtin_isgraph(int);
+ int __builtin_isgraph(int __x0);
- int __builtin_islower(int);
+ int __builtin_islower(int __x0);
- int __builtin_isprint(int);
+ int __builtin_isprint(int __x0);
- int __builtin_ispunct(int);
+ int __builtin_ispunct(int __x0);
- int __builtin_isspace(int);
+ int __builtin_isspace(int __x0);
- int __builtin_isupper(int);
+ int __builtin_isupper(int __x0);
- int __builtin_isxdigit(int);
+ int __builtin_isxdigit(int __x0);
- long __builtin_labs(long);
+ long __builtin_labs(long __x0);
- double __builtin_ldexp(double, int);
+ double __builtin_ldexp(double __x0, int __x1);
- float __builtin_ldexpf(float, int);
+ float __builtin_ldexpf(float __x0, int __x1);
- long double __builtin_ldexpl(long double, int);
+ long double __builtin_ldexpl(long double __x0, int __x1);
- double __builtin_lgamma(double);
+ double __builtin_lgamma(double __x0);
- float __builtin_lgammaf(float);
+ float __builtin_lgammaf(float __x0);
- long double __builtin_lgammal(long double);
+ long double __builtin_lgammal(long double __x0);
- long long __builtin_llabs(long long);
+ long long __builtin_llabs(long long __x0);
- long long __builtin_llrint(double);
+ long long __builtin_llrint(double __x0);
- long long __builtin_llrintf(float);
+ long long __builtin_llrintf(float __x0);
- long long __builtin_llrintl(long double);
+ long long __builtin_llrintl(long double __x0);
- long long __builtin_llround(double);
+ long long __builtin_llround(double __x0);
- long long __builtin_llroundf(float);
+ long long __builtin_llroundf(float __x0);
- long long __builtin_llroundl(long double);
+ long long __builtin_llroundl(long double __x0);
- double __builtin_log(double);
+ double __builtin_log(double __x0);
- double __builtin_log10(double);
+ double __builtin_log10(double __x0);
- float __builtin_log10f(float);
+ float __builtin_log10f(float __x0);
- long double __builtin_log10l(long double);
+ long double __builtin_log10l(long double __x0);
- double __builtin_log1p(double);
+ double __builtin_log1p(double __x0);
- float __builtin_log1pf(float);
+ float __builtin_log1pf(float __x0);
- long double __builtin_log1pl(long double);
+ long double __builtin_log1pl(long double __x0);
- double __builtin_log2(double);
+ double __builtin_log2(double __x0);
- float __builtin_log2f(float);
+ float __builtin_log2f(float __x0);
- long double __builtin_log2l(long double);
+ long double __builtin_log2l(long double __x0);
- double __builtin_logb(double);
+ double __builtin_logb(double __x0);
- float __builtin_logbf(float);
+ float __builtin_logbf(float __x0);
- long double __builtin_logbl(long double);
+ long double __builtin_logbl(long double __x0);
- float __builtin_logf(float);
+ float __builtin_logf(float __x0);
- long double __builtin_logl(long double);
+ long double __builtin_logl(long double __x0);
- long __builtin_lrint(double);
+ long __builtin_lrint(double __x0);
- long __builtin_lrintf(float);
+ long __builtin_lrintf(float __x0);
- long __builtin_lrintl(long double);
+ long __builtin_lrintl(long double __x0);
- long __builtin_lround(double);
+ long __builtin_lround(double __x0);
- long __builtin_lroundf(float);
+ long __builtin_lroundf(float __x0);
- long __builtin_lroundl(long double);
+ long __builtin_lroundl(long double __x0);
- void *__builtin_malloc(unsigned int);
+ void *__builtin_malloc(unsigned int __x0);
- void *__builtin_memchr(void const *, int, unsigned int);
+ void *__builtin_memchr(void const *__x0, int __x1, unsigned int __x2);
- int __builtin_memcmp(void const *, void const *, unsigned int);
+ int __builtin_memcmp(void const *__x0, void const *__x1, unsigned int __x2);
- void *__builtin_memcpy(void *, void const *, unsigned int);
+ void *__builtin_memcpy(void *__x0, void const *__x1, unsigned int __x2);
- void *__builtin_mempcpy(void *, void const *, unsigned int);
+ void *__builtin_mempcpy(void *__x0, void const *__x1, unsigned int __x2);
- void *__builtin_memset(void *, int, unsigned int);
+ void *__builtin_memset(void *__x0, int __x1, unsigned int __x2);
- double __builtin_modf(double, double *);
+ double __builtin_modf(double __x0, double *__x1);
- float __builtin_modff(float, float *);
+ float __builtin_modff(float __x0, float *__x1);
- long double __builtin_modfl(long double, long double *);
+ long double __builtin_modfl(long double __x0, long double *__x1);
- double __builtin_nan(char const *);
+ double __builtin_nan(char const *__x0);
- float __builtin_nanf(char const *);
+ float __builtin_nanf(char const *__x0);
- long double __builtin_nanl(char const *);
+ long double __builtin_nanl(char const *__x0);
- double __builtin_nans(char const *);
+ double __builtin_nans(char const *__x0);
- float __builtin_nansf(char const *);
+ float __builtin_nansf(char const *__x0);
- long double __builtin_nansl(char const *);
+ long double __builtin_nansl(char const *__x0);
- double __builtin_nearbyint(double);
+ double __builtin_nearbyint(double __x0);
- float __builtin_nearbyintf(float);
+ float __builtin_nearbyintf(float __x0);
- long double __builtin_nearbyintl(long double);
+ long double __builtin_nearbyintl(long double __x0);
__builtin_va_list __builtin_next_arg(void);
- double __builtin_nextafter(double, double);
+ double __builtin_nextafter(double __x0, double __x1);
- float __builtin_nextafterf(float, float);
+ float __builtin_nextafterf(float __x0, float __x1);
- long double __builtin_nextafterl(long double, long double);
+ long double __builtin_nextafterl(long double __x0, long double __x1);
- double __builtin_nexttoward(double, long double);
+ double __builtin_nexttoward(double __x0, long double __x1);
- float __builtin_nexttowardf(float, long double);
+ float __builtin_nexttowardf(float __x0, long double __x1);
- long double __builtin_nexttowardl(long double, long double);
+ long double __builtin_nexttowardl(long double __x0, long double __x1);
- unsigned int __builtin_object_size(void *, int);
+ unsigned int __builtin_object_size(void *__x0, int __x1);
- unsigned int __builtin_offsetof(unsigned int);
+ unsigned int __builtin_offsetof(unsigned int __x0);
- int __builtin_parity(unsigned int);
+ int __builtin_parity(unsigned int __x0);
- int __builtin_parityl(unsigned long);
+ int __builtin_parityl(unsigned long __x0);
- int __builtin_parityll(unsigned long long);
+ int __builtin_parityll(unsigned long long __x0);
- double __builtin_pow(double, double);
+ double __builtin_pow(double __x0, double __x1);
- float __builtin_powf(float, float);
+ float __builtin_powf(float __x0, float __x1);
- double __builtin_powi(double, int);
+ double __builtin_powi(double __x0, int __x1);
- float __builtin_powif(float, int);
+ float __builtin_powif(float __x0, int __x1);
- long double __builtin_powil(long double, int);
+ long double __builtin_powil(long double __x0, int __x1);
- long double __builtin_powl(long double, long double);
+ long double __builtin_powl(long double __x0, long double __x1);
- void __builtin_prefetch(void const * , ...);
+ void __builtin_prefetch(void const *__x0 , ...);
- int __builtin_printf(char const * , ...);
+ int __builtin_printf(char const *__x0 , ...);
- int __builtin_putchar(int);
+ int __builtin_putchar(int __x0);
- int __builtin_puts(char const *);
+ int __builtin_puts(char const *__x0);
- void *__builtin_realloc(void *, unsigned int);
+ void *__builtin_realloc(void *__x0, unsigned int __x1);
- double __builtin_remainder(double, double);
+ double __builtin_remainder(double __x0, double __x1);
- float __builtin_remainderf(float, float);
+ float __builtin_remainderf(float __x0, float __x1);
- long double __builtin_remainderl(long double, long double);
+ long double __builtin_remainderl(long double __x0, long double __x1);
- double __builtin_remquo(double, double, int *);
+ double __builtin_remquo(double __x0, double __x1, int *__x2);
- float __builtin_remquof(float, float, int *);
+ float __builtin_remquof(float __x0, float __x1, int *__x2);
- long double __builtin_remquol(long double, long double, int *);
+ long double __builtin_remquol(long double __x0, long double __x1, int *__x2);
- void __builtin_return(void const *);
+ void __builtin_return(void const *__x0);
- void *__builtin_return_address(unsigned int);
+ void *__builtin_return_address(unsigned int __x0);
- double __builtin_rint(double);
+ double __builtin_rint(double __x0);
- float __builtin_rintf(float);
+ float __builtin_rintf(float __x0);
- long double __builtin_rintl(long double);
+ long double __builtin_rintl(long double __x0);
- double __builtin_round(double);
+ double __builtin_round(double __x0);
- float __builtin_roundf(float);
+ float __builtin_roundf(float __x0);
- long double __builtin_roundl(long double);
+ long double __builtin_roundl(long double __x0);
- double __builtin_scalbln(double, long);
+ double __builtin_scalbln(double __x0, long __x1);
- float __builtin_scalblnf(float, long);
+ float __builtin_scalblnf(float __x0, long __x1);
- long double __builtin_scalblnl(long double, long);
+ long double __builtin_scalblnl(long double __x0, long __x1);
- double __builtin_scalbn(double, int);
+ double __builtin_scalbn(double __x0, int __x1);
- float __builtin_scalbnf(float, int);
+ float __builtin_scalbnf(float __x0, int __x1);
- long double __builtin_scalbnl(long double, int);
+ long double __builtin_scalbnl(long double __x0, int __x1);
- int __builtin_scanf(char const * , ...);
+ int __builtin_scanf(char const *__x0 , ...);
- double __builtin_sin(double);
+ double __builtin_sin(double __x0);
- float __builtin_sinf(float);
+ float __builtin_sinf(float __x0);
- double __builtin_sinh(double);
+ double __builtin_sinh(double __x0);
- float __builtin_sinhf(float);
+ float __builtin_sinhf(float __x0);
- long double __builtin_sinhl(long double);
+ long double __builtin_sinhl(long double __x0);
- long double __builtin_sinl(long double);
+ long double __builtin_sinl(long double __x0);
- int __builtin_snprintf(char *, unsigned int, char const * , ...);
+ int __builtin_snprintf(char *__x0, unsigned int __x1, char const *__x2 , ...);
- int __builtin_sprintf(char *, char const * , ...);
+ int __builtin_sprintf(char *__x0, char const *__x1 , ...);
- double __builtin_sqrt(double);
+ double __builtin_sqrt(double __x0);
- float __builtin_sqrtf(float);
+ float __builtin_sqrtf(float __x0);
- long double __builtin_sqrtl(long double);
+ long double __builtin_sqrtl(long double __x0);
- int __builtin_sscanf(char const *, char const * , ...);
+ int __builtin_sscanf(char const *__x0, char const *__x1 , ...);
- void __builtin_stdarg_start(__builtin_va_list);
+ void __builtin_stdarg_start(__builtin_va_list __x0);
- char *__builtin_stpcpy(char *, char const *);
+ char *__builtin_stpcpy(char *__x0, char const *__x1);
- char *__builtin_strcat(char *, char const *);
+ char *__builtin_strcat(char *__x0, char const *__x1);
- char *__builtin_strchr(char *, int);
+ char *__builtin_strchr(char *__x0, int __x1);
- int __builtin_strcmp(char const *, char const *);
+ int __builtin_strcmp(char const *__x0, char const *__x1);
- char *__builtin_strcpy(char *, char const *);
+ char *__builtin_strcpy(char *__x0, char const *__x1);
- unsigned int __builtin_strcspn(char const *, char const *);
+ unsigned int __builtin_strcspn(char const *__x0, char const *__x1);
- unsigned int __builtin_strlen(char const *);
+ unsigned int __builtin_strlen(char const *__x0);
- char *__builtin_strncat(char *, char const *, unsigned int);
+ char *__builtin_strncat(char *__x0, char const *__x1, unsigned int __x2);
- int __builtin_strncmp(char const *, char const *, unsigned int);
+ int __builtin_strncmp(char const *__x0, char const *__x1, unsigned int __x2);
- char *__builtin_strncpy(char *, char const *, unsigned int);
+ char *__builtin_strncpy(char *__x0, char const *__x1, unsigned int __x2);
- char *__builtin_strpbrk(char const *, char const *);
+ char *__builtin_strpbrk(char const *__x0, char const *__x1);
- char *__builtin_strrchr(char const *, int);
+ char *__builtin_strrchr(char const *__x0, int __x1);
- unsigned int __builtin_strspn(char const *, char const *);
+ unsigned int __builtin_strspn(char const *__x0, char const *__x1);
- char *__builtin_strstr(char const *, char const *);
+ char *__builtin_strstr(char const *__x0, char const *__x1);
- double __builtin_tan(double);
+ double __builtin_tan(double __x0);
- float __builtin_tanf(float);
+ float __builtin_tanf(float __x0);
- double __builtin_tanh(double);
+ double __builtin_tanh(double __x0);
- float __builtin_tanhf(float);
+ float __builtin_tanhf(float __x0);
- long double __builtin_tanhl(long double);
+ long double __builtin_tanhl(long double __x0);
- long double __builtin_tanl(long double);
+ long double __builtin_tanl(long double __x0);
- double __builtin_tgamma(double);
+ double __builtin_tgamma(double __x0);
- float __builtin_tgammaf(float);
+ float __builtin_tgammaf(float __x0);
- long double __builtin_tgammal(long double);
+ long double __builtin_tgammal(long double __x0);
- int __builtin_tolower(int);
+ int __builtin_tolower(int __x0);
- int __builtin_toupper(int);
+ int __builtin_toupper(int __x0);
- double __builtin_trunc(double);
+ double __builtin_trunc(double __x0);
- float __builtin_truncf(float);
+ float __builtin_truncf(float __x0);
- long double __builtin_truncl(long double);
+ long double __builtin_truncl(long double __x0);
- int __builtin_types_compatible_p(unsigned int, unsigned int);
+ int __builtin_types_compatible_p(unsigned int __x0, unsigned int __x1);
void __builtin_unreachable(void);
- void __builtin_va_arg(__builtin_va_list, unsigned int, void *);
+ void __builtin_va_arg(__builtin_va_list __x0, unsigned int __x1, void *__x2);
- void __builtin_va_copy(__builtin_va_list, __builtin_va_list);
+ void __builtin_va_copy(__builtin_va_list __x0, __builtin_va_list __x1);
- void __builtin_va_end(__builtin_va_list);
+ void __builtin_va_end(__builtin_va_list __x0);
- void __builtin_va_start(__builtin_va_list);
+ void __builtin_va_start(__builtin_va_list __x0);
- void __builtin_varargs_start(__builtin_va_list);
+ void __builtin_varargs_start(__builtin_va_list __x0);
- int __builtin_vfprintf(void *, char const *, __builtin_va_list);
+ int __builtin_vfprintf(void *__x0, char const *__x1, __builtin_va_list __x2);
- int __builtin_vfscanf(void *, char const *, __builtin_va_list);
+ int __builtin_vfscanf(void *__x0, char const *__x1, __builtin_va_list __x2);
- int __builtin_vprintf(char const *, __builtin_va_list);
+ int __builtin_vprintf(char const *__x0, __builtin_va_list __x1);
- int __builtin_vscanf(char const *, __builtin_va_list);
+ int __builtin_vscanf(char const *__x0, __builtin_va_list __x1);
- int __builtin_vsnprintf(char *, unsigned int, char const *, __builtin_va_list);
+ int __builtin_vsnprintf(char *__x0, unsigned int __x1, char const *__x2,
+ __builtin_va_list __x3);
- int __builtin_vsprintf(char *, char const *, __builtin_va_list);
+ int __builtin_vsprintf(char *__x0, char const *__x1, __builtin_va_list __x2);
- int __builtin_vsscanf(char const *, char const *, __builtin_va_list);
+ int __builtin_vsscanf(char const *__x0, char const *__x1,
+ __builtin_va_list __x2);
- short __sync_add_and_fetch_int16_t(short volatile *, short , ...);
+ short __sync_add_and_fetch_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_add_and_fetch_int32_t(int volatile *, int , ...);
+ int __sync_add_and_fetch_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_add_and_fetch_int64_t(long long volatile *, long long , ...);
+ long long __sync_add_and_fetch_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_add_and_fetch_int8_t(signed char volatile *, signed char
- , ...);
+ signed char __sync_add_and_fetch_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_add_and_fetch_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_add_and_fetch_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_add_and_fetch_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_add_and_fetch_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_add_and_fetch_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_add_and_fetch_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1
+ , ...);
- unsigned char __sync_add_and_fetch_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_add_and_fetch_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
- short __sync_and_and_fetch_int16_t(short volatile *, short , ...);
+ short __sync_and_and_fetch_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_and_and_fetch_int32_t(int volatile *, int , ...);
+ int __sync_and_and_fetch_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_and_and_fetch_int64_t(long long volatile *, long long , ...);
+ long long __sync_and_and_fetch_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_and_and_fetch_int8_t(signed char volatile *, signed char
- , ...);
+ signed char __sync_and_and_fetch_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_and_and_fetch_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_and_and_fetch_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_and_and_fetch_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_and_and_fetch_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_and_and_fetch_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_and_and_fetch_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1
+ , ...);
- unsigned char __sync_and_and_fetch_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_and_and_fetch_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
- int __sync_bool_compare_and_swap_int16_t(short volatile *, short, short , ...);
+ int __sync_bool_compare_and_swap_int16_t(short volatile *__x0, short __x1,
+ short __x2 , ...);
- int __sync_bool_compare_and_swap_int32_t(int volatile *, int, int , ...);
+ int __sync_bool_compare_and_swap_int32_t(int volatile *__x0, int __x1,
+ int __x2 , ...);
- int __sync_bool_compare_and_swap_int64_t(long long volatile *, long long,
- long long , ...);
+ int __sync_bool_compare_and_swap_int64_t(long long volatile *__x0,
+ long long __x1, long long __x2 , ...);
- int __sync_bool_compare_and_swap_int8_t(signed char volatile *, signed char,
- signed char , ...);
+ int __sync_bool_compare_and_swap_int8_t(signed char volatile *__x0,
+ signed char __x1, signed char __x2
+ , ...);
- int __sync_bool_compare_and_swap_uint16_t(unsigned short volatile *,
- unsigned short, unsigned short
- , ...);
+ int __sync_bool_compare_and_swap_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1,
+ unsigned short __x2 , ...);
- int __sync_bool_compare_and_swap_uint32_t(unsigned int volatile *,
- unsigned int, unsigned int , ...);
+ int __sync_bool_compare_and_swap_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1,
+ unsigned int __x2 , ...);
- int __sync_bool_compare_and_swap_uint64_t(unsigned long long volatile *,
- unsigned long long,
- unsigned long long , ...);
+ int __sync_bool_compare_and_swap_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1,
+ unsigned long long __x2 , ...);
- int __sync_bool_compare_and_swap_uint8_t(unsigned char volatile *,
- unsigned char, unsigned char , ...);
+ int __sync_bool_compare_and_swap_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1,
+ unsigned char __x2 , ...);
- short __sync_fetch_and_add_int16_t(short volatile *, short , ...);
+ short __sync_fetch_and_add_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_fetch_and_add_int32_t(int volatile *, int , ...);
+ int __sync_fetch_and_add_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_fetch_and_add_int64_t(long long volatile *, long long , ...);
+ long long __sync_fetch_and_add_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_fetch_and_add_int8_t(signed char volatile *, signed char
- , ...);
+ signed char __sync_fetch_and_add_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_fetch_and_add_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_fetch_and_add_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_fetch_and_add_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_fetch_and_add_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_fetch_and_add_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_fetch_and_add_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1
+ , ...);
- unsigned char __sync_fetch_and_add_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_fetch_and_add_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
- short __sync_fetch_and_and_int16_t(short volatile *, short , ...);
+ short __sync_fetch_and_and_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_fetch_and_and_int32_t(int volatile *, int , ...);
+ int __sync_fetch_and_and_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_fetch_and_and_int64_t(long long volatile *, long long , ...);
+ long long __sync_fetch_and_and_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_fetch_and_and_int8_t(signed char volatile *, signed char
- , ...);
+ signed char __sync_fetch_and_and_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_fetch_and_and_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_fetch_and_and_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_fetch_and_and_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_fetch_and_and_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_fetch_and_and_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_fetch_and_and_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1
+ , ...);
- unsigned char __sync_fetch_and_and_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_fetch_and_and_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
- short __sync_fetch_and_nand_int16_t(short volatile *, short , ...);
+ short __sync_fetch_and_nand_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_fetch_and_nand_int32_t(int volatile *, int , ...);
+ int __sync_fetch_and_nand_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_fetch_and_nand_int64_t(long long volatile *, long long , ...);
+ long long __sync_fetch_and_nand_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_fetch_and_nand_int8_t(signed char volatile *, signed char
- , ...);
+ signed char __sync_fetch_and_nand_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_fetch_and_nand_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_fetch_and_nand_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_fetch_and_nand_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_fetch_and_nand_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_fetch_and_nand_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_fetch_and_nand_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1
+ , ...);
- unsigned char __sync_fetch_and_nand_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_fetch_and_nand_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
- short __sync_fetch_and_or_int16_t(short volatile *, short , ...);
+ short __sync_fetch_and_or_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_fetch_and_or_int32_t(int volatile *, int , ...);
+ int __sync_fetch_and_or_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_fetch_and_or_int64_t(long long volatile *, long long , ...);
+ long long __sync_fetch_and_or_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_fetch_and_or_int8_t(signed char volatile *, signed char
- , ...);
+ signed char __sync_fetch_and_or_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_fetch_and_or_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_fetch_and_or_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_fetch_and_or_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_fetch_and_or_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_fetch_and_or_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_fetch_and_or_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1 , ...);
- unsigned char __sync_fetch_and_or_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_fetch_and_or_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
- short __sync_fetch_and_sub_int16_t(short volatile *, short , ...);
+ short __sync_fetch_and_sub_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_fetch_and_sub_int32_t(int volatile *, int , ...);
+ int __sync_fetch_and_sub_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_fetch_and_sub_int64_t(long long volatile *, long long , ...);
+ long long __sync_fetch_and_sub_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_fetch_and_sub_int8_t(signed char volatile *, signed char
- , ...);
+ signed char __sync_fetch_and_sub_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_fetch_and_sub_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_fetch_and_sub_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_fetch_and_sub_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_fetch_and_sub_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_fetch_and_sub_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_fetch_and_sub_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1
+ , ...);
- unsigned char __sync_fetch_and_sub_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_fetch_and_sub_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
- short __sync_fetch_and_xor_int16_t(short volatile *, short , ...);
+ short __sync_fetch_and_xor_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_fetch_and_xor_int32_t(int volatile *, int , ...);
+ int __sync_fetch_and_xor_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_fetch_and_xor_int64_t(long long volatile *, long long , ...);
+ long long __sync_fetch_and_xor_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_fetch_and_xor_int8_t(signed char volatile *, signed char
- , ...);
+ signed char __sync_fetch_and_xor_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_fetch_and_xor_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_fetch_and_xor_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_fetch_and_xor_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_fetch_and_xor_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_fetch_and_xor_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_fetch_and_xor_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1
+ , ...);
- unsigned char __sync_fetch_and_xor_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_fetch_and_xor_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
- void __sync_lock_release_int16_t(short volatile * , ...);
+ void __sync_lock_release_int16_t(short volatile *__x0 , ...);
- void __sync_lock_release_int32_t(int volatile * , ...);
+ void __sync_lock_release_int32_t(int volatile *__x0 , ...);
- void __sync_lock_release_int64_t(long long volatile * , ...);
+ void __sync_lock_release_int64_t(long long volatile *__x0 , ...);
- void __sync_lock_release_int8_t(signed char volatile * , ...);
+ void __sync_lock_release_int8_t(signed char volatile *__x0 , ...);
- void __sync_lock_release_uint16_t(unsigned short volatile * , ...);
+ void __sync_lock_release_uint16_t(unsigned short volatile *__x0 , ...);
- void __sync_lock_release_uint32_t(unsigned int volatile * , ...);
+ void __sync_lock_release_uint32_t(unsigned int volatile *__x0 , ...);
- void __sync_lock_release_uint64_t(unsigned long long volatile * , ...);
+ void __sync_lock_release_uint64_t(unsigned long long volatile *__x0 , ...);
- void __sync_lock_release_uint8_t(unsigned char volatile * , ...);
+ void __sync_lock_release_uint8_t(unsigned char volatile *__x0 , ...);
- short __sync_lock_test_and_set_int16_t(short volatile *, short , ...);
+ short __sync_lock_test_and_set_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_lock_test_and_set_int32_t(int volatile *, int , ...);
+ int __sync_lock_test_and_set_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_lock_test_and_set_int64_t(long long volatile *, long long
- , ...);
+ long long __sync_lock_test_and_set_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_lock_test_and_set_int8_t(signed char volatile *,
- signed char , ...);
+ signed char __sync_lock_test_and_set_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_lock_test_and_set_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_lock_test_and_set_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_lock_test_and_set_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_lock_test_and_set_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_lock_test_and_set_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_lock_test_and_set_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1
+ , ...);
- unsigned char __sync_lock_test_and_set_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_lock_test_and_set_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
- short __sync_nand_and_fetch_int16_t(short volatile *, short , ...);
+ short __sync_nand_and_fetch_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_nand_and_fetch_int32_t(int volatile *, int , ...);
+ int __sync_nand_and_fetch_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_nand_and_fetch_int64_t(long long volatile *, long long , ...);
+ long long __sync_nand_and_fetch_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_nand_and_fetch_int8_t(signed char volatile *, signed char
- , ...);
+ signed char __sync_nand_and_fetch_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_nand_and_fetch_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_nand_and_fetch_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_nand_and_fetch_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_nand_and_fetch_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_nand_and_fetch_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_nand_and_fetch_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1
+ , ...);
- unsigned char __sync_nand_and_fetch_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_nand_and_fetch_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
- short __sync_or_and_fetch_int16_t(short volatile *, short , ...);
+ short __sync_or_and_fetch_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_or_and_fetch_int32_t(int volatile *, int , ...);
+ int __sync_or_and_fetch_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_or_and_fetch_int64_t(long long volatile *, long long , ...);
+ long long __sync_or_and_fetch_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_or_and_fetch_int8_t(signed char volatile *, signed char
- , ...);
+ signed char __sync_or_and_fetch_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_or_and_fetch_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_or_and_fetch_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_or_and_fetch_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_or_and_fetch_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_or_and_fetch_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_or_and_fetch_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1 , ...);
- unsigned char __sync_or_and_fetch_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_or_and_fetch_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
- short __sync_sub_and_fetch_int16_t(short volatile *, short , ...);
+ short __sync_sub_and_fetch_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_sub_and_fetch_int32_t(int volatile *, int , ...);
+ int __sync_sub_and_fetch_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_sub_and_fetch_int64_t(long long volatile *, long long , ...);
+ long long __sync_sub_and_fetch_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_sub_and_fetch_int8_t(signed char volatile *, signed char
- , ...);
+ signed char __sync_sub_and_fetch_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_sub_and_fetch_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_sub_and_fetch_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_sub_and_fetch_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_sub_and_fetch_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_sub_and_fetch_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_sub_and_fetch_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1
+ , ...);
- unsigned char __sync_sub_and_fetch_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_sub_and_fetch_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
void __sync_synchronize(...);
- short __sync_val_compare_and_swap_int16_t(short volatile *, short, short
- , ...);
+ short __sync_val_compare_and_swap_int16_t(short volatile *__x0, short __x1,
+ short __x2 , ...);
- int __sync_val_compare_and_swap_int32_t(int volatile *, int, int , ...);
+ int __sync_val_compare_and_swap_int32_t(int volatile *__x0, int __x1,
+ int __x2 , ...);
- long long __sync_val_compare_and_swap_int64_t(long long volatile *,
- long long, long long , ...);
+ long long __sync_val_compare_and_swap_int64_t(long long volatile *__x0,
+ long long __x1, long long __x2
+ , ...);
- signed char __sync_val_compare_and_swap_int8_t(signed char volatile *,
- signed char, signed char , ...);
+ signed char __sync_val_compare_and_swap_int8_t(signed char volatile *__x0,
+ signed char __x1,
+ signed char __x2 , ...);
- unsigned short __sync_val_compare_and_swap_uint16_t(unsigned short volatile *,
- unsigned short,
- unsigned short , ...);
+ unsigned short __sync_val_compare_and_swap_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1,
+ unsigned short __x2 , ...);
- unsigned int __sync_val_compare_and_swap_uint32_t(unsigned int volatile *,
- unsigned int, unsigned int
- , ...);
+ unsigned int __sync_val_compare_and_swap_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1,
+ unsigned int __x2 , ...);
- unsigned long long __sync_val_compare_and_swap_uint64_t(unsigned long long volatile *,
- unsigned long long,
- unsigned long long
+ unsigned long long __sync_val_compare_and_swap_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1,
+ unsigned long long __x2
, ...);
- unsigned char __sync_val_compare_and_swap_uint8_t(unsigned char volatile *,
- unsigned char,
- unsigned char , ...);
+ unsigned char __sync_val_compare_and_swap_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1,
+ unsigned char __x2 , ...);
- short __sync_xor_and_fetch_int16_t(short volatile *, short , ...);
+ short __sync_xor_and_fetch_int16_t(short volatile *__x0, short __x1 , ...);
- int __sync_xor_and_fetch_int32_t(int volatile *, int , ...);
+ int __sync_xor_and_fetch_int32_t(int volatile *__x0, int __x1 , ...);
- long long __sync_xor_and_fetch_int64_t(long long volatile *, long long , ...);
+ long long __sync_xor_and_fetch_int64_t(long long volatile *__x0,
+ long long __x1 , ...);
- signed char __sync_xor_and_fetch_int8_t(signed char volatile *, signed char
- , ...);
+ signed char __sync_xor_and_fetch_int8_t(signed char volatile *__x0,
+ signed char __x1 , ...);
- unsigned short __sync_xor_and_fetch_uint16_t(unsigned short volatile *,
- unsigned short , ...);
+ unsigned short __sync_xor_and_fetch_uint16_t(unsigned short volatile *__x0,
+ unsigned short __x1 , ...);
- unsigned int __sync_xor_and_fetch_uint32_t(unsigned int volatile *,
- unsigned int , ...);
+ unsigned int __sync_xor_and_fetch_uint32_t(unsigned int volatile *__x0,
+ unsigned int __x1 , ...);
- unsigned long long __sync_xor_and_fetch_uint64_t(unsigned long long volatile *,
- unsigned long long , ...);
+ unsigned long long __sync_xor_and_fetch_uint64_t(unsigned long long volatile *__x0,
+ unsigned long long __x1
+ , ...);
- unsigned char __sync_xor_and_fetch_uint8_t(unsigned char volatile *,
- unsigned char , ...);
+ unsigned char __sync_xor_and_fetch_uint8_t(unsigned char volatile *__x0,
+ unsigned char __x1 , ...);
int max(int i, int j)
{
diff --git a/tests/syntax/oracle/vdescr_bts1387.res.oracle b/tests/syntax/oracle/vdescr_bts1387.res.oracle
index a5c81d268f53e53ef3daac9619cf2d5378f26381..fa87e2625fbac770015eb9e9cadc1e097a6e4442 100644
--- a/tests/syntax/oracle/vdescr_bts1387.res.oracle
+++ b/tests/syntax/oracle/vdescr_bts1387.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing tests/syntax/vdescr_bts1387.i (no preprocessing)
[kernel] Variable f has vdescr ''
-[kernel] Variable has vdescr ''
+[kernel] Variable __x0 has vdescr ''
[kernel] Variable g has vdescr ''
-[kernel] Variable has vdescr ''
+[kernel] Variable __x0 has vdescr ''
[kernel] Variable fptr has vdescr ''
[kernel] Variable main has vdescr ''
[kernel] Variable j has vdescr ''
diff --git a/tests/value/oracle/bug0223.0.res.oracle b/tests/value/oracle/bug0223.0.res.oracle
index 95216a488d0cd5ba9ab0bb184bf366158fec215e..60ea63f4943e1283c987763f5aa1609c5505571e 100644
--- a/tests/value/oracle/bug0223.0.res.oracle
+++ b/tests/value/oracle/bug0223.0.res.oracle
@@ -48,7 +48,7 @@
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function F:
- \result FROM \nothing
+ \result FROM __x0; __x1
[from] Function my_strcnmp:
\result FROM n
[from] Function h2:
diff --git a/tests/value/oracle/bug0223.1.res.oracle b/tests/value/oracle/bug0223.1.res.oracle
index 95216a488d0cd5ba9ab0bb184bf366158fec215e..60ea63f4943e1283c987763f5aa1609c5505571e 100644
--- a/tests/value/oracle/bug0223.1.res.oracle
+++ b/tests/value/oracle/bug0223.1.res.oracle
@@ -48,7 +48,7 @@
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function F:
- \result FROM \nothing
+ \result FROM __x0; __x1
[from] Function my_strcnmp:
\result FROM n
[from] Function h2:
diff --git a/tests/value/oracle/from_call.0.res.oracle b/tests/value/oracle/from_call.0.res.oracle
index 90af155562b9b8797ae7bcbd68e0ee6bd42434e9..3c1554933630cb972f005d119af7e5131ad64662 100644
--- a/tests/value/oracle/from_call.0.res.oracle
+++ b/tests/value/oracle/from_call.0.res.oracle
@@ -233,7 +233,7 @@
[from] call to g at tests/value/from_call.i:20 (by f):
\result FROM t; w
[from] call to h at tests/value/from_call.i:20 (by f):
- \result FROM \nothing
+ \result FROM __x0
[from] call to return_A1 at tests/value/from_call.i:44 (by dispatcher2):
\result FROM A1
[from] call to return_A2 at tests/value/from_call.i:44 (by dispatcher2):
@@ -247,15 +247,15 @@
[from] call to f at tests/value/from_call.i:81 (by main):
b FROM a; p; f_previous
f_previous FROM p
- \result FROM a; t; p; f_previous
+ \result FROM a; x; t; p; f_previous
[from] call to f at tests/value/from_call.i:82 (by main):
c FROM b; p; f_previous
f_previous FROM p
- \result FROM b; t; p; f_previous
+ \result FROM b; x; t; p; f_previous
[from] call to f at tests/value/from_call.i:82 (by main):
d FROM c; p; f_previous
f_previous FROM p
- \result FROM c; t; p; f_previous
+ \result FROM c; x; t; p; f_previous
[from] call to dispatcher at tests/value/from_call.i:83 (by main):
\result FROM c_0; y_0
[from] call to dispatcher at tests/value/from_call.i:84 (by main):
@@ -281,8 +281,8 @@
b FROM a; f_previous
c FROM a; f_previous
d FROM a; f_previous
- y FROM a; t; f_previous
- z FROM a; t; f_previous
+ y FROM a; x; t; f_previous
+ z FROM a; x; t; f_previous
R1 FROM A1
R2 FROM A4
R3 FROM A4; A5; r
diff --git a/tests/value/oracle/from_call.1.res.oracle b/tests/value/oracle/from_call.1.res.oracle
index eb4493ddfd3a65d3dfce413d96809353d388e0e9..8c4d385823045d66ea53f176df188e4c31960b04 100644
--- a/tests/value/oracle/from_call.1.res.oracle
+++ b/tests/value/oracle/from_call.1.res.oracle
@@ -179,13 +179,13 @@
[from] Function g:
\result FROM direct: t; w
[from] Function h:
- \result FROM \nothing
+ \result FROM direct: __x0
[from] Function f:
b FROM indirect: p; f_previous; direct: a; b; c (and SELF)
c FROM indirect: p; f_previous; direct: a; b; c (and SELF)
d FROM indirect: p; f_previous; direct: a; b; c (and SELF)
f_previous FROM direct: p
- \result FROM indirect: p; f_previous; direct: a; b; c; d; t
+ \result FROM indirect: p; f_previous; direct: a; b; c; d; x; t
[from] Function return_A1:
\result FROM direct: A1
[from] Function return_A2:
@@ -205,8 +205,8 @@
b FROM indirect: f_previous; direct: a; b; c (and SELF)
c FROM indirect: f_previous; direct: a; b; c (and SELF)
d FROM indirect: f_previous; direct: a; b; c (and SELF)
- y FROM indirect: f_previous; direct: a; b; c; d; t
- z FROM indirect: f_previous; direct: a; b; c; d; t
+ y FROM indirect: f_previous; direct: a; b; c; d; x; t
+ z FROM indirect: f_previous; direct: a; b; c; d; x; t
R1 FROM direct: A1; A2
R2 FROM direct: A3; A4
R3 FROM indirect: r; direct: A4; A5
diff --git a/tests/value/oracle/resolve.res.oracle b/tests/value/oracle/resolve.res.oracle
index 49a9d91450d37554a884986c1280d4208214afca..05b5f86f0764be2e8b6ce56670ca501162673cf4 100644
--- a/tests/value/oracle/resolve.res.oracle
+++ b/tests/value/oracle/resolve.res.oracle
@@ -22,7 +22,7 @@
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function f:
- \result FROM \nothing
+ \result FROM __x0; __x1
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
diff --git a/tests/value/oracle/va_list2.1.res.oracle b/tests/value/oracle/va_list2.1.res.oracle
index a3b3d14e82c077e0377b92df53337ce4b7b54ece..4cae1c2cf4ddd9c1b9018b1cb195b15e5065ffd2 100644
--- a/tests/value/oracle/va_list2.1.res.oracle
+++ b/tests/value/oracle/va_list2.1.res.oracle
@@ -22,6 +22,7 @@
accessing uninitialized left-value.
assert \initialized(&tmp);
(tmp from vararg)
+[eva] tests/value/va_list2.c:16: Frama_C_show_each_i: [-2147483648..2147483647]
[eva] computing for function __builtin_va_arg <- main.
Called from tests/value/va_list2.c:20.
[eva] Done for function __builtin_va_arg
@@ -29,15 +30,23 @@
accessing uninitialized left-value.
assert \initialized(&tmp_0);
(tmp_0 from vararg)
+[eva:alarm] tests/value/va_list2.c:20: Warning:
+ non-finite float value. assert \is_finite(tmp_0);
+ (tmp_0 from vararg)
+[eva] tests/value/va_list2.c:21:
+ Frama_C_show_each_f: [-3.40282346639e+38 .. 3.40282346639e+38]
[eva] tests/value/va_list2.c:12: starting to merge loop iterations
[eva:alarm] tests/value/va_list2.c:13: Warning:
out of bounds read. assert \valid_read(fmt);
[eva] computing for function __builtin_va_arg <- main.
Called from tests/value/va_list2.c:15.
[eva] Done for function __builtin_va_arg
+[eva] tests/value/va_list2.c:16: Frama_C_show_each_i: [-2147483648..2147483647]
[eva] computing for function __builtin_va_arg <- main.
Called from tests/value/va_list2.c:20.
[eva] Done for function __builtin_va_arg
+[eva] tests/value/va_list2.c:21:
+ Frama_C_show_each_f: [-3.40282346639e+38 .. 3.40282346639e+38]
[eva] computing for function __builtin_va_end <- main.
Called from tests/value/va_list2.c:28.
[kernel:annot:missing-spec] tests/value/va_list2.c:28: Warning:
@@ -46,10 +55,6 @@
[eva] Done for function __builtin_va_end
[eva] Recording results for main
[eva] done for function main
-[eva] tests/value/va_list2.c:15:
- assertion 'Eva,initialization' got final status invalid.
-[eva] tests/value/va_list2.c:20:
- assertion 'Eva,initialization' got final status invalid.
[scope:rm_asserts] removing 1 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -65,7 +70,8 @@
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function __builtin_va_arg:
- NO EFFECTS
+ tmp FROM __x0; __x1; tmp; tmp_0 (and SELF)
+ tmp_0 FROM __x0; __x1; tmp; tmp_0 (and SELF)
[from] Function __builtin_va_end:
NO EFFECTS
[from] Function __builtin_va_start:
@@ -74,6 +80,6 @@
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
- fmt; i; f
+ fmt; i; tmp; f; tmp_0
[inout] Inputs for function main:
S_fmt[0..1]
diff --git a/tests/value/oracle_gauges/va_list2.1.res.oracle b/tests/value/oracle_gauges/va_list2.1.res.oracle
index 6af1df391437f951baaad48f4a545991f74459f3..86ce6779e00f527779982716836f130ede14bd7b 100644
--- a/tests/value/oracle_gauges/va_list2.1.res.oracle
+++ b/tests/value/oracle_gauges/va_list2.1.res.oracle
@@ -1,13 +1,19 @@
-40a41,52
+49a50,67
> [eva] computing for function __builtin_va_arg <- main.
> Called from tests/value/va_list2.c:15.
> [eva] Done for function __builtin_va_arg
+> [eva] tests/value/va_list2.c:16: Frama_C_show_each_i: [-2147483648..2147483647]
> [eva] computing for function __builtin_va_arg <- main.
> Called from tests/value/va_list2.c:20.
> [eva] Done for function __builtin_va_arg
+> [eva] tests/value/va_list2.c:21:
+> Frama_C_show_each_f: [-3.40282346639e+38 .. 3.40282346639e+38]
> [eva] computing for function __builtin_va_arg <- main.
> Called from tests/value/va_list2.c:15.
> [eva] Done for function __builtin_va_arg
+> [eva] tests/value/va_list2.c:16: Frama_C_show_each_i: [-2147483648..2147483647]
> [eva] computing for function __builtin_va_arg <- main.
> Called from tests/value/va_list2.c:20.
> [eva] Done for function __builtin_va_arg
+> [eva] tests/value/va_list2.c:21:
+> Frama_C_show_each_f: [-3.40282346639e+38 .. 3.40282346639e+38]