diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-03-23 11:30:27 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-03-23 11:30:27 +0100 |
| commit | 6c295e28af6a7facd10bd8672a8857a6b1b4971c (patch) | |
| tree | 7104ca42aa38829c809f757a9a87ee2436a4bb29 /cparser | |
| parent | 3f83ae50789d44c49bec5db292d58db3f02d5f79 (diff) | |
| download | compcert-6c295e28af6a7facd10bd8672a8857a6b1b4971c.tar.gz compcert-6c295e28af6a7facd10bd8672a8857a6b1b4971c.zip | |
Do not allow inline on main and warn for Noreturn (#63)
* Do not allow inline on main().
The C99 standard says that in a hosted environment inline shall
not appear in a declaration of main.
Bug 23274
* Added warning for _Noreturn on main().
The C11 standard does not allow any function specifier on the
main function.
Bug 23274
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Elab.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 4de43fe0..97ee4f76 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2334,6 +2334,10 @@ let elab_fundef env spec name defs body loc = (* Special treatment of the "main" function. *) let body2 = if s = "main" then begin + if inline then + error loc "'main' is not allowed to be declared inline"; + if noret then + warning loc Unnamed "'main' is not allowed to be declared _Noreturn"; match unroll env ty_ret with | TInt(IInt, []) -> (* Add implicit "return 0;" at end of function body. |