diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index c980a64c6bb71830cbcf8250bc6dee37fbeeae61..262085f022449d4c450cf7da06fc854349b4a91e 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4792,9 +4792,9 @@ and doAttr ghost (a: A.attribute) : attribute list =
         end
       | A.CONSTANT (A.CONST_FLOAT str) ->
         ACons ("__fc_float", [AStr str])
-      | A.CALL({expr_node = A.VARIABLE n}, args, ghost) -> begin
+      | A.CALL({expr_node = A.VARIABLE n}, args, []) -> begin
           let n' = if strip then stripUnderscore n else n in
-          let ae' = List.map ae (args@ghost) in
+          let ae' = List.map ae args in
           ACons(n', ae')
         end
       | A.EXPR_SIZEOF e -> ASizeOfE (ae e)