From bbd151137a139c9c057e41650c18d6954fa8ea60 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 12 Jan 2022 17:17:44 +0100
Subject: [PATCH] [Kernel] avoid crash due to invalid variadic builtin usage

---
 src/kernel_services/ast_printing/cil_printer.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index ca1847c257a..d7a95024779 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1223,8 +1223,12 @@ class cil_printer () = object (self)
     | Some vi ->
       let formals = Cil.getFormalsDecl vi in
       match List.rev formals with
-      | [] -> assert false (* Typing error, this function is variadic and should
-                              have at least one argument *)
+      | [] ->
+        (* Typing error, this function should
+           have at least one named argument *)
+        Kernel.abort ~current:true
+          "%s should have at least one named argument"
+          vi.vname
       | f :: _ -> Cil.new_exp ~loc:f.vdecl (Lval (Cil.var f))
 
   (**** STATEMENTS ****)
-- 
GitLab