From 70f8e613f717a8820e52bcc89343699b968bf7c7 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Fri, 2 Aug 2024 15:13:05 -0700 Subject: [PATCH] Translate FunctionNoParams as a function without parameters. Fixes #438 --- backend/cn/lib/sctypes.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/backend/cn/lib/sctypes.ml b/backend/cn/lib/sctypes.ml index 7b488a2bd..b6bd8cafc 100644 --- a/backend/cn/lib/sctypes.ml +++ b/backend/cn/lib/sctypes.ml @@ -171,7 +171,14 @@ let rec of_ctype (Ctype.Ctype (_, ct_)) = in let@ ret_ct = of_ctype ret_ct in return (Function ((ret_q, ret_ct), args, variadic)) - | Ctype.FunctionNoParams _ -> fail + + (* The meaning of a function with no parameters depends on the version of C, + but here we treat it as if it really has no parameter (i.e., like `void`) + which is what more recent versions of the standard do. *) + | Ctype.FunctionNoParams (ret_q, ret_ct) -> + let@ ret_ct = of_ctype ret_ct in + return (Function ((ret_q, ret_ct), [], false)) + | Ctype.Pointer (_qualifiers, ctype) -> let@ t = of_ctype ctype in return (Pointer t) @@ -184,7 +191,7 @@ let of_ctype_unsafe loc ct = let open Cerb_pp_prelude in match of_ctype ct with | Some ct -> ct - | None -> Tools.unsupported loc (!^"C-type" ^^^ Cerb_frontend.Pp_core_ctype.pp_ctype ct) + | None -> Tools.unsupported loc (!^"YAV C-type" ^^^ Cerb_frontend.Pp_core_ctype.pp_ctype ct) let pp t = Pp_core_ctype.pp_ctype (to_ctype t)