aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
* Detect uses of anonymous structs/unions (a C2011 feature and GCC extension) ↵Xavier Leroy2015-04-301-0/+14
| | | | and produce a diagnostic instead of ignoring them.
* Detect and reject "&" operator applied to "register" local variable or to a ↵Xavier Leroy2015-04-283-0/+34
| | | | bit field.
* Bitfield improvements continued: perform bitfield expansion before ↵Xavier Leroy2015-04-282-180/+210
| | | | unblocking; improve translation of bitfield initializers and compound literals.
* Extended inline asm: handle missing cases.Xavier Leroy2015-04-286-19/+46
| | | | | | Bitfields: better translation of initializers and compound literals; run this pass before unblocking. Transform.stmt: extend with ability to treat unblocked code. test/regression: more bitfield tests.
* Allow "scratch" (non-allocatable temporary registers) to be mentioned in asm ↵Xavier Leroy2015-04-231-0/+1
| | | | clobber lists.
* Extended asm: more lenient treatment of constraints.Xavier Leroy2015-04-221-10/+21
| | | | | We can ignore alternatives as long as one of the constraints we handle (r, m, i, n) is there.
* Avoid multiple errors being reported in the case #outputs >= 2.Xavier Leroy2015-04-211-2/+6
|
* Proper treatment of extended asm.Xavier Leroy2015-04-211-1/+5
|
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-211-0/+183
| | | | | | | | - support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-178-21/+168
|
* Merge branch 'master' into dwarfBernhard Schommer2015-04-141-0/+7
|\
| * Detect (and reject with an error) preprocessing numbers that are not valid ↵Xavier Leroy2015-04-061-0/+7
| | | | | | | | integer or floating constants.
* | Merge branch 'master' into dwarfBernhard Schommer2015-03-316-88/+480
|\| | | | | | | | | | | Conflicts: Makefile driver/Driver.ml
| * "ecomma" smart constructor: reassociate to the left so that it prints more ↵Xavier Leroy2015-03-201-2/+8
| | | | | | | | nicely.
| * Improvements in the StructReturn transformation (ABI conformance for passing ↵Xavier Leroy2015-03-203-66/+45
| | | | | | | | | | | | | | | | composites). - Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD. - Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions. - More comprehensive interoperability test in regression/interop1.c.
| * Merge branch 'master' into struct-passingXavier Leroy2015-03-141-7/+12
| |\
| * | Improve performance and configurability for the StructReturn pass.Xavier Leroy2015-03-143-54/+110
| | | | | | | | | | | | | | | | | | | | | | | | configure: special ABI value for IA32/MacOSX and PowerPC/Linux cparser/Machine: special config for PowerPC/Linux cparser/StructReturn: generate better code for return-as-int driver/Clflags, driver/Driver: add options -fstruct-return=<convention> and -fstruct-passing=<convention> to simplify testing
| * | ABI compatibility for struct/union function arguments passed by value.Xavier Leroy2015-01-276-69/+420
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The passing of struct/union arguments by value implemented in the verified part of CompCert is not compatible with the ARM, PowerPC and x86 ABI. Here we enrich the StructReturn source-to-source emulation pass so that it implements the calling conventions defined in these ABIs. Plus: for x86, implement the returning of struct/union results by value in a way compatible with the ABI.
* | | Compute the size of structs using the result of the packing and bitfield ↵Bernhard Schommer2015-03-261-10/+10
| | | | | | | | | | | | transformations.
* | | Added missing functions for printing the structs and unions. Still missing ↵Bernhard Schommer2015-03-242-5/+10
| | | | | | | | | | | | printing of packed structs.
* | | Added translation fucntion for declarations and fundefinitions.Bernhard Schommer2015-03-231-0/+2
| |/ |/|
* | Issue #26: problems with big escape sequences in string/char literals.Xavier Leroy2015-03-071-7/+12
|/ | | | | | - Error instead of warning if escape sequence overflows one character. - Wrong normalization of L'x' to char instead of wchar_t. - More careful overflow tests.
* Merge branch 'named-structs'Xavier Leroy2015-01-231-2/+4
|\ | | | | | | | | | | | | | | | | | | | | | | | | - Switch CompCert C / Clight AST of composite types (structs and unions) from a structural representation to a nominal representation, closer to concrete syntax. - This avoids algorithmic inefficiencies due to the structural representation. - Closes PR#4. - Smallstep: make small-step semantics more polymorphic in the type of the global environment. - Globalenvs: introduce Senv.t (symbol environments) as a restricted view on Genv.t (full global environments). - Events, Smallstep: use Senv instead of Genv to talk about global names.
| * Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-311-2/+4
| | | | | | | | | | Use these constructor functions in C2C to rely less on the types produced by the unverified elaborator.
* | Delay reads from !Machine.config before it is properly initialized.Xavier Leroy2015-01-227-66/+86
| | | | | | | | | | | | | | | | | | | | | | | | | | Several definitions in Cutil and elsewhere were accessing the default value of !Machine.config, before it is properly initialized in Driver. Delay evaluation of these definitions, and initialize Machine.config to nonsensical values so that lack of initialization is caught early (e.g. in Cutil.find_matching_*_kind). Also, following up on commit [3b8a094], don't use "wchar_t" typedef to type wide string literals, even if this typedef is in scope. The risk here is to hide an inconsistency between "wchar_t"'s definition in standard headers and CompCert's built-in definition.
* | 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
generated by cgit (git 2.34.1) at 2024-07-01 23:53:53 +0000