aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Updates for release 3.4v3.4Xavier Leroy2018-09-172-2/+2
|
* Bug 24510Bernhard Schommer2018-09-140-0/+0
|
* flocq: minor cleaning (#257)Vincent Laporte2018-09-141-3/+2
| | | | | | This change avoids relying on generated names, making the proof script compatible with ongoing evolutions of the `zify` tactic. A similar cleanup was already performed in Flocq's master sources.
* Update change log for 3.4, continuedXavier Leroy2018-09-141-2/+5
|
* Improved diagnostics: spelling, wording, etc (#138)Michael Schmidt2018-09-145-15/+15
| | | | | | | | | | | | | | | | | | * bug 24268: avoid assertion after reporting error for invalid call to builtin_debug * bug 24268, remove duplicated warning tag in lexer messages * bug 24268, fix spelling in array element designator message * bug 24268, unify 'consider adding option ...' messages * bug 24268, add spacing for icbi operands * bug 24268, uniform use of Ignored_attributes class for identical warnings * bug 24268, unify message for 'assignment to const type' to error from error/fatal error * bug 24268, in handcrafted.messages, "a xxx have been recognized" -> "a xxx has been recognized"
* Simplified code. Bug 24067Bernhard Schommer2018-09-121-8/+8
|
* Tentatively support Coq 8.8.2Xavier Leroy2018-09-121-2/+2
| | | | | It's not out yet, but based on the state of the v8.8 branch of Coq, it is very likely to be compatible with CompCert.
* Typo in OCaml version numberXavier Leroy2018-09-121-1/+1
|
* Update version and change log in preparation for public release 3.4Xavier Leroy2018-09-122-1/+63
|
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-1214-28/+64
| | | | | | | | | | | | | | | | | | | | | | | | | | * Generate a nop instruction after ais annotations. In order to prevent the merging of ais annotations with following Labels a nop instruction is inserted, but only if the annotation is followed immediately by a label. The insertion of nop instructions is performed during the expansion of builtin and pseudo assembler instructions and is processor independent, by inserting a __builtin_nop built-in. * Add Pnop instruction to ARM, RISC-V, and x86 ARM as well as RISC-V don't have nop instructions that can be easily encoded by for example add with zero instructions. For x86 we used to use `mov X0, X0` for nop but this may not be as efficient as the true nop instruction. * Implement __builtin_nop on all supported target architectures. This builtin is not yet made available on the C side for all architectures. Bug 24067
* Fatal error instead of error for bit-fields.Bernhard Schommer2018-09-121-1/+1
| | | | | | Since the following offsetof cannot handle bit-fields we should stop earlier. Bug 24480
* Attach _Alignas to names and refactor _Alignas checks (#133)Bernhard Schommer2018-09-106-20/+22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Refactor common code of alignas. Instead of working on attributes the function now works directly on the type since the check always performed an extraction of attributes from a type. Bug 23393 * Attach _Alignas to the name. Bug 23393 * Attach "aligned" attributes to names So that __attribute((aligned(N))) remains consistent with _Alignas(N). gcc and clang apply "aligned" attributes to names, with a special case for typedefs: typedef __attribute((aligned(16))) int int_al_16; int_al_16 * p; __attribute((aligned(16))) int * q; For gcc, p is naturally-aligned pointer to 16-aligned int and q is 16-aligned pointer to naturally-aligned int. For CompCert with this commit, both p and q are 16-aligned pointers to naturally-aligned int. * Resurrect the alignment test involving typedef The test was removed because it involved an _Alignas in a typedef, which is no longer supported. However the same effect can be achieved with an "aligned" attribute, which is still supported in typedef.
* Ignore generated conflict file. Bug 24455Bernhard Schommer2018-09-101-0/+1
|
* Bug 23389Bernhard Schommer2018-09-040-0/+0
|
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2018-09-041-1/+1
|\
| * Typo in commentXavier Leroy2018-09-031-1/+1
| |
* | document new named warning class 'reduced-alignment', bug 23389Michael Schmidt2018-09-041-0/+4
|/
* Move parameter check.Bernhard Schommer2018-09-031-2/+6
| | | | | | Instead of performing the check only for parameters of function definitions also perform it for function declarations. Bug 23393
* New diagnostic for reduced alignment (#117)Bernhard Schommer2018-08-293-3/+38
| | | | | | | The new diagnostic triggers if an `_Alignas` or an `aligned` attribute or a `packed` attribute requests an alignment smaller than the natural alignment. Bug 23389
* Bug 24374Bernhard Schommer2018-08-290-0/+0
|
* Merge pull request #251 from AbsInt/configure-error-behaviorXavier Leroy2018-08-291-0/+14
|\ | | | | Improve behavior of configure script in case of configuration errors
| * Improve reporting of configuration errorsXavier Leroy2018-08-281-0/+10
| | | | | | | | | | | | | | | | | | | | | | | | The full "usage" text is so long that the actual error message scrolls off the screen. With this commit, instead, a short (3-line) error message is printed, with a suggestion to do `./configure -help`. The whole "usage" text is printed by `./configure -help`. Also: better error message for unknown options (arguments starting with `-`).
| * Remove leftover Makefile.config before configurationXavier Leroy2018-08-281-0/+4
| | | | | | | | | | | | | | So that if an error occurs during configuration, there is no Makefile.config file and "make" will fail. Closes: #244
* | Bug 24366Bernhard Schommer2018-08-280-0/+0
| |
* | Import prim token notations before using them, continuedXavier Leroy2018-08-271-0/+1
| | | | | | | | | | Follow-up to f6f537d. "list" scope must be opened to counterbalance opening of "string" scope.
* | Import prim token notations before using themJason Gross2018-08-274-1/+4
| | | | | | | | | | | | | | | | | | This is required for compatibility with https://github.com/coq/coq/pull/8064, where prim token notations no longer follow `Require`, but instead follow `Import`. Closes #246 Closes #250
* | Bug 24351Bernhard Schommer2018-08-270-0/+0
|/
* Make generated file cparser/Parser.v read-onlyXavier Leroy2018-08-271-0/+2
| | | | | | | For consistency with other generated .v files, and because it protects against editing the generated file, see Github issue #248. Closes: #248
* Improve execution of regression testsXavier Leroy2018-08-244-16/+45
| | | | | | - Make it possible to skip tests on some platforms - Make it possible to expect a failure (typically: of the reference interpreter) - Stop on error
* Edit documentation comments for [alignas_attribute] and [has_std_alignas]Xavier Leroy2018-08-241-2/+3
|
* More standard compliant handling of _Alignas.Bernhard Schommer2018-08-241-0/+11
| | | | | | | | | | | The C11 standard disallows the usage of _Alignas for: - Bit-field members of struct or union types - Typedefs - Function Defintions - Parameters of functions It is still allowed to use the gcc attribute for these constructs. Bug 23391
* Add check for _Alignas attribute.Bernhard Schommer2018-08-242-0/+6
| | | | | | The check tests whether the standard _Alignas is contained within a given attribute list. Bug 23391
* Reimplement attr_array_applicable in terms of class_of_attributeXavier Leroy2018-08-241-3/+2
| | | | | | | | | | | | | Since commit 5963ac4, "aligned" attributes and _Alignas qualifiers are represented differently, causing them to be treated differently by the previous implementation of Cutil.attr_array_applicable. This is incorrect and inconsistent with what happens during elaboration of array types in Elab. This PR reimplements attr_array_applicable in terms of class_of_attribute. Just like during elaboration, attributes of the Attr_type class are applied to the type of array elements, other attributes stay attached to the array type.
* Preserve attribute(("aligned")) in the AST, don't map it to _AlignasXavier Leroy2018-08-242-2/+3
| | | | | | | | | | | | | | We used to recognize attribute(("aligned"(N))) and map it to _Alignas(N) during elaboration. However, we want to restrict the places where _Alignas can occur, as standardized in ISO C11, while leaving more freedom for the placement of the "aligned" attribute. As a first step in this direction, this commit keeps the "aligned" attribute unchanged in the AST, and distinct from _Alignas attributes. Both attributes are honored when it comes to determining the actual alignment of a type.
* Fix typo in pattern match of error case, bug 24326Michael Schmidt2018-08-221-1/+1
|
* Document new named warning for tentative static definitions with incomplete ↵Michael Schmidt2018-08-211-0/+4
| | | | type, bug 23377
* Document new named warning for flexible arrays, bug 23324Michael Schmidt2018-08-211-1/+1
|
* Document new named warning for flexible arrays, bug 23324Michael Schmidt2018-08-211-0/+4
|
* Fix passing of -u to linker.Bernhard Schommer2018-08-211-1/+1
| | | | | | Instead of just passing -u to the linker also pass the value of the option to the linker. Bug 24316
* Diagnostic for wrong application of restrict (#119)Bernhard Schommer2018-08-213-7/+33
| | | | | | Restrict is only allowed for pointers whose referenced type is an object type or incomplete type, but not a function type. Bug 23397
* Harden the extasm.c test, continuedXavier Leroy2018-08-202-5/+5
| | | | | Follow-up to b9a6a50. clang is not happy with COMPCERT_MODEL=32sse2 ("bad suffix on integer"), so use MODEL_32sse2 and ARCH_x86 instead.
* Improve support and diagnostic for type qualified arrays (#118)Bernhard Schommer2018-08-203-1/+18
| | | | | | | | | | | | | | | | * Add diagnostic for type qualified arrays that occur in the wrong place Arrays with type qualifiers (e.g. int t[const 5]) are only allowed as function parameters and for them only the outermost array type derivation. Bug 23400 * Keep attributes from array for argument conversion Type qualifiers of arrays in function parameters are just syntactic sugar to allow adding them to the resulting pointer type. Hence, when a qualified array type such as `int t[const 5]` decays into a pointer type during argument conversion, the pointer type should be qualified, e.g. `int * const t`.
* Added warning for incomplete tentative static defs (#114)Bernhard Schommer2018-08-203-4/+11
| | | | | | Tentative static definitions with incomplete type are not allowed in C99. However most popular compilers support them and warn about them. Bug 23377
* Harden the extasm.c testXavier Leroy2018-08-202-2/+7
| | | | | | | Pass more info from CompCert's configuration as #define on command line. Use this info to improve the "64 bit" detection in extasm.c. (Before it fails with powerpc-ppc64, which has 64-bit int regs but couldn't be detected with #ifdefs.)
* Additional checks for flex arrays in structs (#93)Bernhard Schommer2018-08-205-5/+30
| | | | | | | | | | | | | | | * Error for structs with only flex array member Flexible array members are only allowed if another member exists. Bug 23324 * Added checks for nesting of structs with flex array members Warn if a struct with a flex array member is used as array element or member of another struct. Such usage is dubious. Bug 23324 Don't warn if the struct-with-flex-array is a member of an union.
* Add sizeof_reg and new Machine configurations (#129)Bernhard Schommer2018-08-204-5/+25
| | | | | | | | | | | | | Since the size of integer registers is not identical to the size of pointers for the ppc64 and e5500 model the check for register pairs in ExtendedAsm does not work correctly. In order to avoid this a new field sizeof_intreg is introduced in the Machine configuration which describes the size of integer registers. New configurations for the ppc64 and e5500 model are added and used. Bug 24273
* Turn error into fatal error for unnamed parameter.Bernhard Schommer2018-08-201-2/+4
| | | | | | Since the parameter name gets used in other error messages it results in messages without names. Bug 24283
* For "packed" attribute, check that 3rd parameter is 0 or 1Xavier Leroy2018-08-171-1/+1
| | | | | | | It's meant as a Boolean (byte-swap or not), so any other value is dangerous. The error message is the generic "ill-formed 'packed' attribute". Maybe we don't need a custom error message.
* Wrong AST for GCC-style attributesXavier Leroy2018-08-171-1/+1
| | | | | The list of arguments to the attribute was missing a reverse, hence attribute(("foo"(1,2,3))) was actually read as attribute(("foo"(3,2,1))).
* Check for bit-fields in __builtin_offsetofXavier Leroy2018-08-171-1/+4
| | | | __builtin_offsetof(struct s, f) is an error if f is a bit-field.
generated by cgit (git 2.34.1) at 2024-06-11 23:37:35 +0000