From f1d236b83003eda71e12840732d159fd23b1b771 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Apr 2014 13:58:18 +0000 Subject: Integration of Jacques-Henri Jourdan's verified parser. (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'Changelog') diff --git a/Changelog b/Changelog index 7c0c982..d0f9172 100644 --- a/Changelog +++ b/Changelog @@ -1,7 +1,17 @@ Language features: - Support for C99 designated initializers. (ISO C99 section 6.7.8.) +- Traditional, pre-Standard function definitions are no longer supported, e.g. + int f(i) int i; { return i + 1; } // no longer supported + Use Standard form instead: + int f(int i) { return i + 1; } Improvements in confidence: +- The parser is now formally verified against the ISO C99 grammar plus + CompCert's extensions. The verification proves that the parser + recognizes exactly the language specified by the grammar, and that + the grammar has no ambiguities. For more details, see the paper + "Validating LR(1) parsers" by Jacques-Henri Jourdan, François Pottier, + and Xavier Leroy, ESOP 2012, http://dx.doi.org/10.1007/978-3-642-28869-2_20 - More theorems proved about float<->integer conversions. Optimizations: -- cgit v1.2.3