From e1367ffc5ee4ebd7b7a17cfed2fe8a615ab6da82 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 25 Mar 2020 12:44:24 +0100
Subject: [PATCH] =?UTF-8?q?[eacsl:codegen]=C2=A0Support=20of=20variadic=20?=
=?UTF-8?q?functions=20in=20`Constructor.mk=5Flib=5Fcall`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
.../e-acsl/src/code_generator/constructor.ml | 35 ++++++++++++-------
1 file changed, 22 insertions(+), 13 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml
index 8146800bdab..106efe3abbb 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.ml
+++ b/src/plugins/e-acsl/src/code_generator/constructor.ml
@@ -69,21 +69,30 @@ let mk_lib_call ~loc ?result fname args =
let vi = Misc.get_lib_fun_vi fname in
let f = Cil.evar ~loc vi in
vi.vreferenced <- true;
- let make_args args param_ty =
- List.map2
- (fun (_, ty, _) arg ->
- let e =
- match ty, Cil.unrollType (Cil.typeOf arg), arg.enode with
- | TPtr _, TArray _, Lval lv -> Cil.new_exp ~loc (StartOf lv)
- | TPtr _, TArray _, _ -> assert false
- | _, _, _ -> arg
- in
- Cil.mkCast ~force:false ~newt:ty ~e)
- param_ty
- args
+ let make_args ~variadic args param_ty =
+ let rec make_rev_args res args param_ty =
+ match args, param_ty with
+ | arg :: args_tl, (_, ty, _) :: param_ty_tl ->
+ let e =
+ match ty, Cil.unrollType (Cil.typeOf arg), arg.enode with
+ | TPtr _, TArray _, Lval lv -> Cil.new_exp ~loc (StartOf lv)
+ | TPtr _, TArray _, _ -> assert false
+ | _, _, _ -> arg
+ in
+ let e = Cil.mkCast ~force:false ~newt:ty ~e in
+ make_rev_args (e :: res) args_tl param_ty_tl
+ | arg :: args_tl, [] when variadic -> make_rev_args (arg :: res) args_tl []
+ | [], [] -> res
+ | _, _ ->
+ Options.fatal
+ "Mismatch between the number of expressions given and the number \
+ of arguments in the signature when calling function '%s'"
+ fname
+ in
+ List.rev (make_rev_args [] args param_ty)
in
let args = match Cil.unrollType vi.vtype with
- | TFun(_, Some params, _, _) -> make_args args params
+ | TFun(_, Some params, variadic, _) -> make_args ~variadic args params
| TFun(_, None, _, _) -> []
| _ -> assert false
in
--
GitLab