From e9a6869da3167c09b0ba562bb7a3fe4f0adca9a0 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 31 Aug 2020 15:07:31 +0200
Subject: [PATCH] [variadic] prevent the generation of arrays of size 0
---
src/plugins/variadic/generic.ml | 8 ++++++--
src/plugins/variadic/standard.ml | 7 +++++--
.../declared/oracle/empty-vpar-with-ghost.res.oracle | 2 +-
.../variadic/tests/declared/oracle/empty-vpar.res.oracle | 2 +-
.../variadic/tests/defined/oracle/empty-vpar.res.oracle | 2 +-
.../variadic/tests/defined/oracle/recursive.res.oracle | 4 ++--
6 files changed, 16 insertions(+), 9 deletions(-)
diff --git a/src/plugins/variadic/generic.ml b/src/plugins/variadic/generic.ml
index c139cd1a7a6..4d1eb376928 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 5d31f0ed063..3076f8e9394 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 8163b08cd5b..77d342b3dd8 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 de788c9929d..c028e9e151d 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 a485fce2d7f..7f338532acd 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 3c962f76c0c..9fcbfae2ed2 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;
--
GitLab