From aeed7fed9917969a942994646ad75b348be393ae Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Fri, 2 Aug 2024 15:13:05 -0700 Subject: [PATCH 1/2] 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) From 92b84200f52cfebd37cbb1db4b45429bc3dd80e0 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Fri, 2 Aug 2024 15:14:53 -0700 Subject: [PATCH 2/2] Remove debug message --- backend/cn/lib/sctypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backend/cn/lib/sctypes.ml b/backend/cn/lib/sctypes.ml index b6bd8cafc..d413ba26b 100644 --- a/backend/cn/lib/sctypes.ml +++ b/backend/cn/lib/sctypes.ml @@ -191,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 (!^"YAV C-type" ^^^ Cerb_frontend.Pp_core_ctype.pp_ctype ct) + | None -> Tools.unsupported loc (!^"Unsupported C-type" ^^^ Cerb_frontend.Pp_core_ctype.pp_ctype ct) let pp t = Pp_core_ctype.pp_ctype (to_ctype t)