diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-22 11:13:23 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-22 11:13:23 +0200 |
commit | ef16a51223a4b73eed74c40ce9938248ab6b4b8a (patch) | |
tree | 12a81f7818a01eab08b71b253320c11ebb364447 /common | |
parent | 5dd1544021c608060d8ee5ba052cc82132fff741 (diff) | |
download | compcert-ef16a51223a4b73eed74c40ce9938248ab6b4b8a.tar.gz compcert-ef16a51223a4b73eed74c40ce9938248ab6b4b8a.zip |
In AST.calling_conventions, record whether the original C function was "old-style" unprototyped.
Use this info in printing function types for Csyntax and Clight.
Diffstat (limited to 'common')
-rw-r--r-- | common/AST.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/common/AST.v b/common/AST.v index 08a19789..387eb6b2 100644 --- a/common/AST.v +++ b/common/AST.v @@ -100,12 +100,13 @@ These signatures are used in particular to determine appropriate calling conventions for the function. *) Record calling_convention : Type := mkcallconv { - cc_vararg: bool; - cc_structret: bool + cc_vararg: bool; (**r variable-arity function *) + cc_unproto: bool; (**r old-style unprototyped function *) + cc_structret: bool (**r function returning a struct *) }. Definition cc_default := - {| cc_vararg := false; cc_structret := false |}. + {| cc_vararg := false; cc_unproto := false; cc_structret := false |}. Record signature : Type := mksignature { sig_args: list typ; |