diff options
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. |