aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
* Wrong handling of block-local function declarations (again)Xavier Leroy2015-01-011-12/+7
| | | | | Reapply commit c3b615f875ed2cf8418453c79c4621d2dc61b0a0 which was overwritten by 2d32afc5daf16c75d1a34f2716c34ae2e1efcce4
* Revised type compatibility check w.r.t. handling of attributes.Xavier Leroy2015-01-014-49/+93
| | | | | | | We now distinguish 3 modes (instead of 2 previously) for attributes: 1- strict compatibility, 2- ignore top-level attrs, 3- ignore all attrs recursively. In strict mode, const/volatile/restrict attributes must be identical, but nonstandard attributes may vary. Also: ignore top-level attrs when comparing function argument types, like GCC/Clang do. Net result is fewer warnings and type-checking that is closer to GCC/Clang.
* PR#12: regression introduced in commit 2d32afcXavier Leroy2014-12-301-2/+0
|
* PR#6: fix handling of wchar_t and assignments from wide string literals.Xavier Leroy2014-12-305-9/+31
| | | | | | | | | | - cparser/Machine indicates whether wchar_t is signed or not (it is signed int in Linux and BSD, but unsigned short in Win32) - The type of a wide string literal is "wchar_t *" if the typedef "wchar_t" exists in the environment (e.g. after #include <stddef.h>). Only if wchar_t is not defined do we use the default from Machine. - Permit initialization of any integer array from a wide string literal, not just an array of wchar_t.
* PR#11: support sizeof(struct {...}) and _Alignof(struct {...})Xavier Leroy2014-12-301-25/+38
| | | | This is a partial fix because other cases of struct definitions within type-names are still not handled, e.g. (struct { ... } *) <expr>. However, error reporting was improved for these cases.
* Improve printing of errors.Xavier Leroy2014-12-301-3/+11
|
* PR#10 continued: disambiguate record to avoid OCaml warningXavier Leroy2014-12-301-1/+1
|
* PR#10: composite definitions must be maintained in the environment.Xavier Leroy2014-12-301-6/+15
|
* Recognize more of GCC's alternate keywords (e.g. "__signed").Xavier Leroy2014-12-291-21/+24
| | | | | Based on the source of GCC 4.9.2. Plus: reordered keywords in alphabetic order to facilitate comparison.
* Support "asm volatile" (closes: PR#5).Xavier Leroy2014-12-292-1/+3
| | | | The CompCert back-end already treats "asm" inserts as "volatile" in GCC's sense (performing unpredictable side-effects), so no change is required outside of the parser.
* No longer include a pre-generated Parser.v in the distribution.Xavier Leroy2014-12-181-61669/+0
| | | | Assorted updates to configure and Makefile.
* Wrong handling of block-local function declarations (in Elab.ml).Xavier Leroy2014-11-261-12/+7
|
* Moved the timing facility to a seperate file.Bernhard Schommer2014-09-291-3/+3
|
* GCCism: accept __volatile and __volatile__Xavier Leroy2014-09-211-0/+2
| | | | | These alternate keywords for "volatile" are used in some header files in the wild.
* Error instead of warning on illegal escape sequences.Xavier Leroy2014-09-211-1/+1
| | | | | | | | The previous behavior for illegal escape sequences (e.g. '\%') in character and string literals was to emit an error, then treat "\x" as "x". As reported by a user, this is dangerous, because the warning can go unnoticed, and other compilers can treat "\x" as "\\x" (backslash followed by 'x'). Better to error out.
* Support C99 compound literals (by expansion in Unblock pass).xleroy2014-08-2111-453/+625
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improve error reporting for unsupported compound literals.xleroy2014-08-201-1/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2608 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improve error detection and error messages for enums.xleroy2014-08-171-3/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2568 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Spurious error on a local static function declarationxleroy2014-08-131-0/+1
| | | | | | | ("static int f(void);" inside a function). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2563 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Make Alphabet.v compatible with an environnment where Containers is installedjjourdan2014-07-041-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2521 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Empty declarationsjjourdan2014-05-233-11180/+11249
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In enter_or_refine_ident: revised handling of "extern" decls.xleroy2014-05-181-29/+38
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Another corner case for string literal initializers: char * x[] = { "lit" }xleroy2014-05-181-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2498 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typo in struct_declaration_list causing conflicts.xleroy2014-05-181-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Re-added support for "__func__" identifier as per ISO C99.xleroy2014-05-155-5746/+5462
| | | | | | | | - Support for empty structs and unions - Better handling of "extern" and "extern inline" function definitions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2493 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Assorted fixes to fix parsing issues and be more GCC-like:xleroy2014-05-127-13538/+14066
| | | | | | | | | | - Moved scanning of char constants and string literals entirely to Lexer - Parser: separate STRING_LITERAL from CONSTANT to be closer to ISO C99 grammar - pre_parser: adapted + "asm" takes string_literal, not CONSTANT - Revised errors "inline doesnt belong here" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2492 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Incorrect conversion of K&R functions. Example of problem:xleroy2014-05-122-2/+10
| | | | | | | void * foo(s, u) ... git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2491 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix string litteral parsingjjourdan2014-05-112-3/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2490 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed regression on initializers of the form T x[N] = "literal";xleroy2014-05-081-8/+10
| | | | | | | where T is a typedef for a character type. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2488 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Added alternate keywords __inline, __restrict, etc, for GCC compatibilityxleroy2014-05-081-2/+24
| | | | | | | - Skip comments that might remain after preprocessing git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2487 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Stern warning on non-prototype function definitions.xleroy2014-05-051-0/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2480 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Do not allow typedef_name in identifier lists of K&R style definitionsjjourdan2014-05-051-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2479 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for old-style K&R function definitions.xleroy2014-05-056-4545/+5621
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2478 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Treat all identifiers as VAR_NAME by default (i.e. if not bound by a ↵xleroy2014-05-052-15/+8
| | | | | | typedef). This produces better error messages for unbound variable names (proper error message in Elab rather than cryptic syntax error in pre_parser). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2477 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Be less picky in the way we parse '#' linesxleroy2014-05-021-11/+23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2472 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-2931-3153/+66118
| | | | | | | (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Clean-up pass on C types:xleroy2014-04-234-44/+55
| | | | | | | | | | | | | - Ctypes: add useful functions on attributes; remove attrs in typeconv (because attributes are meaningless on r-values) - C2C: fixed missing or redundant Evalof - Cop: ignore attributes in ptr + int and ptr - int (meaningless on r-values); add sanity check between typeconv/classify_binarith and the C99 standard. - cparser: fixed several cases where incorrect type annotations were put on expressions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2457 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch linear-typing:xleroy2014-04-063-12/+13
| | | | | | | | | | | | | | | | | | | | | | | 1) Revised division of labor between RTLtyping and Lineartyping: - RTLtyping no longer keeps track of single-precision floats, switches from subtype-based inference to unification-based inference. - Unityping: new library for unification-based inference. - Locations: don't normalize at assignment in a stack slot - Allocation, Allocproof: simplify accordingly. - Lineartyping: add inference of locations that contain a single-precision float. - Stackingproof: adapted accordingly. This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c). This corresponds to commits 2435+2436 plus improvements in Lineartyping. 2) Add -dtimings option to measure compilation times. Moved call to C parser from Elab to Parse, to make it easier to measure parsing time independently of elaboration time. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2449 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* "->" can also be applied to array types, not just pointer types.xleroy2014-03-301-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2442 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* C: Support array initializers that are too short + default init for remainder.xleroy2014-03-285-140/+361
| | | | | | | | Elab: Handle C99 designated initializers. C2C, Initializers: more precise intermediate AST for initializers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Do not transform __builtin_va_arg for a struct or union type, this causesxleroy2014-02-241-31/+37
| | | | | | | | an ugly error message in the back-end. Rather, leave it as is, and let C2C handle the error. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2422 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong type used for transforming lval = f(...)xleroy2014-02-211-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2413 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-9/+15
| | | | | | | | Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-1/+4
| | | | | | | - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Experimental support for <stdarg.h>, the GCC way. Works on IA32. To be ↵xleroy2014-01-011-4/+8
| | | | | | tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Catch and report Env errors arising out of some Cutil functionsxleroy2013-12-302-8/+9
| | | | | | | (incomplete_type, sizeof, etc). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2393 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Elab.ml: more warnings.xleroy2013-12-302-6/+16
| | | | | | | Cutil.ml: fix sizeof calculation of structs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2391 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved detection of variables with incomplete types.xleroy2013-12-301-4/+9
| | | | | | | Additional warnings for empty initializer braces and zero-sized arrays. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2390 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Check in C2C that packed structs were properly emulated.xleroy2013-12-281-3/+8
| | | | | | | PackedStructs.ml: remove "packed" attribute once processed. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2388 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simpler, more robust emulation of calls to variadic functions:xleroy2013-12-285-5/+9
| | | | | | | | | | | | | | - C function types and Cminor signatures annotated by calling conventions. esp. vararg / not vararg - Cshmgen: generate correct code for function call where there are more arguments than listed in the function prototype. This is still undefined behavior according to the formal semantics, but correct code is generated. - C2C, */PrintAsm.ml: remove "printf$iif" hack. - powerpc/, checklink/: don't generate stubs for variadic functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-29 02:03:48 +0000