aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
Commit message (Collapse)AuthorAgeFilesLines
* Global register variables result in fatal error.Bernhard Schommer2015-09-081-1/+1
| | | | | If they only report an error an assertion failure in Reame.ml was triggered.
* Simplify the handling of extended inline asm, taking advantage of the new, ↵Xavier Leroy2015-08-211-6/+5
| | | | structured builtin arguments and results.
* Remove non digit and non letter chars from filename used in renaming of ↵Bernhard Schommer2015-07-151-0/+1
| | | | static variables to avoid problems with files such as "a b.c".
* Reject incomplete types as return type.Bernhard Schommer2015-07-141-1/+4
|
* Use env1 instead of env to also have the type specifiers used in the return ↵Bernhard Schommer2015-07-091-1/+1
| | | | parameter.
* Propagated the composed type constructed build during identifier lookup.Bernhard Schommer2015-07-091-6/+6
|
* Turn off copy optimization when returning a composite by reference.Xavier Leroy2015-07-081-4/+10
| | | | | | The copy optimization is not correct in case of overlap between destination and source. We would need to use an hypothetical __builtin_memmove_aligned that can cope with overlap to implement the copy at return of callee.
* Add implicit "return 0;" at end of function "main".Xavier Leroy2015-07-081-1/+13
| | | | | | | | As per ISO C99, "hosted environment". "return 0" is added at the end of any function named "main" that has "int" as return type. If the name is "main" but the return type is not "int", emit a warning and do not add anything.
* Turn "redefinition with an incompatible type" warning into an error.Xavier Leroy2015-07-081-1/+6
| | | | Also: improve error message by showing old and new types.
* Fix issue with bit fields of type _BoolXavier Leroy2015-07-081-6/+22
| | | | | | cparser/Bitfields.ml: when assigning to a bit field of type _Bool, the right-hand side must be normalized to 0 or 1 via a cast to _Bool. test/regression/bitfields{1,9}.c: add corresponding test cases.
* Merge github.com:AbsInt/CompCertBernhard Schommer2015-07-071-2/+5
|\
| * Change the definition of Typles.tupleJacques-Henri Jourdan2015-07-071-2/+5
| |
* | Diab defines w_char to be unsigned short.Bernhard Schommer2015-07-073-1/+7
|/
* Merge branch 'master' into json_exportBernhard Schommer2015-07-061-0/+1
|\ | | | | | | | | Conflicts: driver/Driver.ml
| * Simple fix for problem with local extern.Bernhard Schommer2015-06-241-0/+1
| |
* | Merge branch 'master' into json_exportBernhard Schommer2015-06-171-3/+9
|\|
| * Turn the error on anonymous structs/unions into a warning.Xavier Leroy2015-06-111-1/+1
| | | | | | | | | | Otherwise we get too many errors on glibc's standard headers. A real error will occur when the anonymous struct/union is accessed.
| * Error if, in the same scope, a typedef is redefined as a variable, or a ↵Xavier Leroy2015-06-061-2/+8
| | | | | | | | variable is redefined as a typedef.
* | Added flag for the renaming of static functions.Bernhard Schommer2015-05-193-8/+24
|/
* Make a register as storage specify to a fatal error.Bernhard Schommer2015-05-141-1/+1
|
* Changed the enter_or_refine_ident function to produce an error if a ↵Bernhard Schommer2015-05-131-6/+14
| | | | non-static declaration is followed by a static declaration/definition.
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-091-3/+4
| | | | | | | | | | - Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting
* 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
| |
generated by cgit (git 2.34.1) at 2024-07-01 08:10:40 +0000