diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-05 23:48:59 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-05 23:48:59 +0200 |
commit | 7c8693320818d00b26b4c36c2a01a5fe67c0c71b (patch) | |
tree | a0c3000416e92078255fdd759ea12338df57fec4 /cparser/Elab.ml | |
parent | 8df444cbc4aa78d4effb03474b3709925ac7002a (diff) | |
download | compcert-7c8693320818d00b26b4c36c2a01a5fe67c0c71b.tar.gz compcert-7c8693320818d00b26b4c36c2a01a5fe67c0c71b.zip |
Handle the special case of a typedef to void funciton parameter to be
handled as a function with void parameter.
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r-- | cparser/Elab.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index d1dce41f..4d3d1d02 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -558,9 +558,9 @@ and elab_parameters env params = | _ -> (* Prototype introduces a new scope *) let (vars, _) = mmap elab_parameter (Env.new_scope env) params in - (* Catch special case f(void) *) + (* Catch special case f(t) where t is void or a typedef to void *) match vars with - | [ ( {name=""}, TVoid _) ] -> Some [] + | [ ( {name=""}, t) ] when is_void_type env t -> Some [] | _ -> Some vars (* Elaboration of a function parameter *) |