aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* x86: wrong modeling of ZF flag for FP comparisonsXavier Leroy2018-12-202-130/+66
| | | | | | | | | | | | | | As written in the comment, ZF should be set if the two floats are equal or unordered. The "or unordered" case was missing in the original modeling of FP comparisons. - Set ZF flag correctly in the Asm.compare_floats and Asm.compare_floats32 functions. - Update the proofs in Asmgenproof1 accordingly. No change required to the code generated for FP comparisons: this code already anticipated the "or unordered" case. Problem reported by Alix Trieu.
* Add functions "ordered" and "compare" to Float and Float32Xavier Leroy2018-12-201-9/+20
| | | | | | | "compare" returns the 4 possible results w/ type "option comparison". "ordered" returns a Boolean. These functions will be used soon in the x86 port.
* Fix fixme in PackedStructs.Bernhard Schommer2018-11-201-4/+4
| | | | | | | | Instead of relying testing that the size of pointers is 64bit the size of registers should be tested. Also it should be a fatal error to reverse a long long on an architecture that does not support reverse 64bit read/writes. Bug 24982
* Fix typo in asmexpand. Bug 24953Bernhard Schommer2018-11-071-1/+1
|
* Use 'gpr_or_zero' for base register of indexed load/stores, bug 24776Michael Schmidt2018-10-202-5/+10
|
* Catch exception from elab_attr_arg.Bernhard Schommer2018-10-181-1/+4
| | | | | | Catch the exception from a non constant argument of a packed attribute and print an error. Bug 24748
* Switch conditions for eref plattforms.Bernhard Schommer2018-09-191-4/+4
| | | | | Otherwise an isel is generated if no isel is needed at all. Bug 24516
* Support __builtin_isel64 for non-EREF PPC64 platforms (#141)Xavier Leroy2018-09-181-22/+28
| | | | | | If the isel instruction is missing, it can be emulated just like we do in the 32-bit case (__builtin_isel). Follow-up to commit 51d32b92. Bug 24516
* Add builtin isel (conditional move) for int64, uint64 and _Bool (#140)Bernhard Schommer2018-09-182-1/+16
| | | | | New builtin isel variants to support conditional moves for 64bit integers and _Bool values. Bug 24516
* Bug 24518Bernhard Schommer2018-09-170-0/+0
|
* 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
generated by cgit (git 2.34.1) at 2024-07-03 08:39:40 +0000