diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index ca1847c257adda363197d1c5bf583f2eee49073f..d7a95024779daa31e2a2c069307f9f3818b672b1 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 ****)