diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index f57f863648ae9a63cdeebef01b1dccb5f6db723b..e3f5fce6cc868ee3e5e9dc619d71c46652e8101f 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