diff --git a/src/plugins/variadic/generic.ml b/src/plugins/variadic/generic.ml index c139cd1a7a66b8e6f5efdce0ba52969fc8a71fd3..4d1eb37692875bf70e99886faca311010e15d92b 100644 --- a/src/plugins/variadic/generic.ml +++ b/src/plugins/variadic/generic.ml @@ -159,8 +159,12 @@ let translate_call ~fundec ~ghost block loc mk_call callee pars = let vis = List.mapi add_var v_exps in (* Build an array to store addresses *) - let ty = Build.(array (ptr void) ~size:(List.length vis)) in - let vargs = Build.(local ty "__va_args" ~init:(List.map addr vis)) in + let init = match vis with (* C standard forbids arrays of size 0 *) + | [] -> [Build.of_init (Cil.makeZeroInit ~loc Cil.voidPtrType)] + | l -> List.map Build.addr l + in + let ty = Build.(array (ptr void) ~size:(List.length init)) in + let vargs = Build.(local ty "__va_args" ~init) in (* Translate the call *) let new_arg = Build.(cil_exp ~loc (cast' (vpar_typ []) (addr vargs))) in diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml index 5d31f0ed063e279bd70e278db2331fbcc53eea9f..3076f8e9394c84ed645dd498b4ae419e56ce59a9 100644 --- a/src/plugins/variadic/standard.ml +++ b/src/plugins/variadic/standard.ml @@ -219,8 +219,11 @@ let aggregator_call ~fundec ~ghost aggregator scope loc mk_call vf args = let module Build = Cil_builder.Stateful (struct let loc = loc end) in Build.open_block ~into:fundec ~ghost (); - let init = List.map Build.of_exp args_middle - and size = List.length args_middle in + let init = match args_middle with (* C standard forbids arrays of size 0 *) + | [] -> [Build.of_init (Cil.makeZeroInit ~loc ptyp)] + | l -> List.map Build.of_exp l + in + let size = List.length init in let vaggr = Build.(local (array ~size (of_ctyp ptyp)) pname ~init) in let new_args = args_left @ [Build.(cil_exp ~loc (addr vaggr))] @ args_right in let new_args,_ = match_args tparams new_args 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 8163b08cd5b80ffd8230adf8079829f27b02aeaf..77d342b3dd8113ce3c181cca5993138243e6bbe4 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 @@ -25,7 +25,7 @@ int main(void) { int __retres; { - void *__va_args[0] = {}; + void *__va_args[1] = {(void *)0}; f(1,2,3,(void * const *)(__va_args)) /*@ ghost (4) */; } __retres = 0; 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 de788c9929d3b9f0848d7e372c7a3bc19181882d..c028e9e151d91ac8f3d848668a9ead0863bef9f1 100644 --- a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle +++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle @@ -23,7 +23,7 @@ int main(void) { int __retres; { - void *__va_args[0] = {}; + void *__va_args[1] = {(void *)0}; f(1,2,3,(void * const *)(__va_args)); } __retres = 0; diff --git a/src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle b/src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle index a485fce2d7fd1127894d15c847ac7f93f9fd1ab1..7f338532acdc46cb6ab68dfd84819601cf787197 100644 --- a/src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle @@ -37,7 +37,7 @@ int main(void) { int tmp; { - void *__va_args[0] = {}; + void *__va_args[1] = {(void *)0}; tmp = sum(0,(void * const *)(__va_args)); } return tmp; diff --git a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle index 3c962f76c0ce29a86219ef5c6cca7e0c640d71f7..9fcbfae2ed2afb6f4498cd8fc01efebb747ea53f 100644 --- a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle +++ b/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[0] = {}; + void *__va_args[1] = {(void *)0}; tmp = f(a - 1,(void * const *)(__va_args)); } __retres = tmp; @@ -41,7 +41,7 @@ int main(void) { int tmp; { - void *__va_args[0] = {}; + void *__va_args[1] = {(void *)0}; tmp = f(7,(void * const *)(__va_args)); } return tmp;