From 24ed39208d9c02f44ce823c83a367431cb33221b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 26 Jul 2021 18:43:22 +0200
Subject: [PATCH] [typing] no anonymous parameters in function definitions as
 well as prototype

Not sure this is really conforming to C standard, but gcc accepts that anyways
---
 src/kernel_internals/typing/cabs2cil.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index f57f863648a..e3f5fce6cc8 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9234,11 +9234,17 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
 
         (* Create the formals and add them to the environment. *)
         (* sfg: extract tsets for the formals from dt *)
+        let cnt = ref 0 in
         let doFormal (loc : location) ((fn, ft, fa) as fd) =
           let ghost = ghost || isGhostFormalVarDecl fd in
           let f = makeVarinfo ~ghost ~temp:false ~loc false true fn ft in
-          (f.vattr <- fa;
-           alphaConvertVarAndAddToEnv true f)
+          f.vattr <- fa;
+          if f.vname = "" then begin
+            f.vname <- "__x" ^ (string_of_int !cnt);
+            incr cnt;
+            f.vattr <- addAttribute anonymous_attribute f.vattr;
+          end;
+          alphaConvertVarAndAddToEnv true f
         in
         let rec doFormals fl' ll' =
           begin
-- 
GitLab