aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* PowerPC: make sure evaluation of conditions do not destroy any registerXavier Leroy2019-05-204-54/+155
| | | | | | | | | | | | | | | This will be useful to implement a "select" (conditional move) operation later. - Introduce `Asmgen.loadimm64_notemp` to load a 64-bit integer constant into a register without going through memory and without needing a temporary register. - Use `Asmgen.loadimm64_notemp` instead of `Asmgen.loadimm64` in the compilation of conditions, so that GPR12 is no longer needed as a temporary. - Share code and proofs common to the two `Asmgen.loadimm64_` functions as the `Asmgen.loadimm64_32s` function.
* Prepend $(DESTDIR) to the installation target (#169)Bernhard Schommer2019-05-172-16/+16
| | | | | | | | Following the gnu Makefile Conventions the variable $(DESTDIR) should be prepended to all installation commands. This allows staged installs.
* Reworked elaboration of declarations/definitions.Bernhard Schommer2019-05-101-140/+138
| | | | | | | | | | | | Since a definition/declaration is completed with after the separator to the next init group member it is also possible to use it for example in the next init group member: char s[]="miaou", buf[sizeof s]; In order to ensure that this works the declarations are added to the environment directly during the elaboration of the init member group instead of later.
* Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-108-15/+41
| | | | | | | | | | The option -fcommon controls whether uninitialized global variables are placed in the COMMON section. If the option is given in the negated form, -fno-common, variables are not placed in the COMMON section. They are placed in the same sections as gcc does. If the variables are not placed in the COMMON section merging of tentative definitions is inhibited and multiple definitions lead to a linker error, as it does for gcc.
* Change to AbsInt version string.Bernhard Schommer2019-05-105-6/+6
| | | | | The AbsInt build number no longer contains "release", so it must be printed additionally.
* Check for reserved keywords.Bernhard Schommer2019-05-101-1/+8
| | | | | | `_Complex` and `_Imaginary` are reserved keywords. Since CompCert does not support these types they could be used as identifiers. However the standard requires to reject this.
* Fix various scoping issues (#163)Bernhard Schommer2019-05-101-51/+56
| | | | | | | | | Pass the environment to all expr eval functions since the functions themselve may be called recursively and modify the environment. The other change introduces new scopes that are strict subsets of their surrounding scopes for if, switch, while, do and for statement, as prescribed by ISO C standards.
* Ensure flushing of the error formatter.Bernhard Schommer2019-05-101-0/+4
| | | | | Since the error formatter is not automatically flushed at program exit we need to ensure that it is flushed at exit.
* Expand the responsefiles earlierBernhard Schommer2019-05-105-17/+17
| | | | | | | | | * Move the expansion of response files to module Commandline, during the initialization of `Commandline.argv`. This way we're sure it's done exactly once. * Make `Commandline.argv` a `string array` instead of a `string array ref`. We no longer need to update it after initialization! * Improve reporting of errors during expansion of response files.
* Check for alignment of command-line switches.Bernhard Schommer2019-05-102-6/+10
| | | | | | Add a check for alignment on command-line switches `-falign-*`. The check is similar to the one for the alignment attribute and ensures that only powers of two can be specified.
* More efficient test for powers of twoXavier Leroy2019-05-092-26/+105
| | | | | | The previous implementation used to build the full powers-of-two decomposition of the number. The present implementation recognizes powers of two directly, then takes the log2.
* Make scripts compatible with new behavior of field_simplify (#291)Vincent Laporte2019-05-062-3/+3
| | | | | | | | The `field_simplify` tactics will be improved soon (https://github.com/coq/coq/pull/9854). Flocq was made compatible with this improvement (https://gitlab.inria.fr/flocq/flocq/commit/0752761a6a344d62f6bc728eac442ebb4ba655ac). This commit updates CompCert's copy of Flocq accordingly.
* Rename Fappli_IEEE_extra.v into IEEE754_extra.vXavier Leroy2019-04-263-2/+2
| | | | | To match the new module names from version 3 of Flocq. Plus, it's shorter.
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-2613-884/+1031
| | | | | | | | | | The module Integers.Make contained lots of definitions and theorems about Z integers that were independent of the word size. These definitions and theorems are useful outside Integers.Make, but it felt unnatural to fetch them from modules Int or Int64. This commit moves the word-size-independent definitions and theorems to a new module, lib/Zbits.v, and fixes their uses in the code base.
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-2315-135/+52
| | | | | Instead, use definitions and lemmas from the Coq standard library (ZArith, Znumtheory).
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-2311-68/+45
| | | | | | | Use Z.to_nat theorems from the standard Coq library in preference to our theorems in lib/Coqlib.v. Simplify lib/Coqlib.v accordingly.
* Problems with Dwarf ranges (#159)Xavier Leroy2019-04-239-56/+96
|\ | | | | | | Merge of branch dwarf-ranges
| * Simplified offset printing.Bernhard Schommer2019-04-161-2/+3
| | | | | | | | | | | | | | Instead of printing an the start label and adding the offset by computing the difference of the range label and the start label use the range label directly. Bug 26234
| * Print only debug info for printed functions.Bernhard Schommer2019-04-166-14/+18
| | | | | | | | | | | | | | | | | | | | | | Functions that are removed from the compilation unit, for example inline functions without extern, should not produce debug information. This commit reuses the mechanism used for variables in order to track additionally the printed functions. Therefore the printed variable versions are exchanged for a printed symbol version. Bug 26234
| * Reworked range entries.Bernhard Schommer2019-04-163-39/+71
| | | | | | | | | | | | | | | | | | | | | | | | The fist changes changes the offset for range entries to used labels instead of integer constants, leaving the computation to the assembler. The second part of the change the address changes the way ranges entries of scopes are printed. They need to be relative to the start address of the code in the section they are included. Bug 26234
| * Reset scope ids later.Bernhard Schommer2019-04-161-1/+1
| | | | | | | | | | | | | | In order to avoid adding ranges to the wrong scopes due to inlining they are numbered consecutively for the whole compilation unit. Bug 26234
| * Avoid generation of empty ranges.Bernhard Schommer2019-04-161-1/+4
| | | | | | | | | | | | As noted in the DWARF 3 specification empty ranges have no effect and can be left out. Bug 26234
| * Relax requirement for ranges for compilation unit.Bernhard Schommer2019-04-161-1/+1
|/ | | | | | Ranges for non-contiguous address ranges are already part of dwarf version 3. Bug 26234
* Typo in comment about Ijumptable in RTL.vAlix Trieu2019-04-151-1/+1
|
* Fix typo in section name in Selectionproof.v Alix Trieu2019-04-151-2/+2
| | | SEL_SWITH_INT -> SEL_SWITCH_INT
* Floats.v: remove leftover Print commandsXavier Leroy2019-04-041-5/+1
| | | | These were committed by mistake.
* Floats.v: avoid using module Zlogarithm in the proofsXavier Leroy2019-04-031-10/+19
| | | | | | | | Rumor has it that this module is scheduled for removal. This is based on pull request #286, with a different implementation. Closes: #286
* Correct typo in Clightnorm.ml (#285)Alix Trieu2019-03-271-1/+1
| | | | In the `Sswitch` case, the original expression was used instead of the result of `norm_expr`.
* Ignore more of Coq's cache filesXavier Leroy2019-03-271-1/+4
| | | | | A grep through Coq's source files show that it uses more cache files than just .lia.cache. Ignore them all.
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-2746-7841/+9954
| | | | | | | | | | | | Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully).
* Define macros with CompCert's version number (#284)Xavier Leroy2019-03-271-2/+24
| | | | | | | | | | | | | | | | As suggested in #282, it can be useful to #ifdef code depending on specific versions of CompCert. Assuming a version number of the form MM.mm , the following macros are predefined: __COMPCERT_MAJOR__=MM (the major version number) __COMPCERT_MINOR__=mm (the minor version number) __COMPCERT_VERSION__=MMmm (two decimal digits for the minor, e.g. 305 for version 3.5) We also define __COMPCERT_BUILDNR__ if the build number is not empty in file ./VERSION. Closes: #282
* Harden configure against weird Menhir installationsXavier Leroy2019-03-251-2/+8
| | | | | | | | | | | As reported in #281, the Menhir packages in Fedora 29 and perhaps in other distributions can cause `menhir --suggest-menhirLib` to fail and return an empty path. This commit detects this situation and aborts configurations. Also, it hardens the generated Makefile against spaces and special characters in the path returned by `menhir --suggest-menhirLib`.
* RTLgenproof: destruct too deepXavier Leroy2019-03-251-2/+2
| | | | | | | `external_call_mem_extends` returns a conjunction of 4 properties, but the destruct pattern was 5 level deep. (Reported by Jeremie Koenig in pull request #278.)
* Integers.v: add modulus_gt_one (#259)Xavier Leroy2019-03-251-1/+7
| | | | | | | Since the number of bits is > 0, it is guaranteed that modulus > 1, not just that modulus > 0. (Suggested by Jake Waksbaum @jbaum.)
* Update the comment of the free operation (#277)chaomaer2019-03-251-1/+1
| | | | The comment says "writable" but it should be "freeable".
* Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-252-3/+3
| | | Preparation for Coq PR 9725 that may make `eauto` stronger.
* Improve overflow check for integer literals (#157)Michael Schmidt2019-03-201-2/+4
| | | | | | The previous check was incomplete for integer literals in base 10. Bug 26119
* Update version number for 3.5v3.5Xavier Leroy2019-02-281-1/+1
|
* Update HTML doc for release 3.5Xavier Leroy2019-02-271-1/+1
|
* Update Changelog in preparation for release 3.5Xavier Leroy2019-02-261-1/+1
|
* Maximum supported Menhir version (#275)Xavier Leroy2019-02-261-1/+1
| | | | | Follow-up to commit fc9bc643. The latest Menhir version compatible with the current code base is actually 20181113.
* Update Changelog in preparation for release 3.5Xavier Leroy2019-02-251-0/+35
|
* Maximum supported Menhir version (#275)Jacques-Henri Jourdan2019-02-251-2/+3
| | | The Coq backend of Menhir will soon enjoy a large refactoring, making it incompatible with the version of MenhirLib currently in CompCert. This commit adds a check in configure to make sure that the version of Menhir is not more modern than the current one (20181026).
* Revised attachment of name attributes to structs, unions, enumsXavier Leroy2019-02-253-6/+29
| | | | | | | | | | | | | | | | | | Consider: ``` struct s { ... } __attribute((aligned(N))); struct t { ... } __attribute((aligned(N))) struct t x; ``` In the first case, the aligned attribute should be attached to struct s, so that further references to struct s are aligned. In the second case, the aligned attribute should be attached to the variable x, because if we attach it to struct t, it will be ignored and cause a warning. This commit changes the attachment rule so that it treats both cases right. Extend regression test for "aligned" attribute accordingly, by testing aligned attribute applied to a name of struct type.
* Reject object-related and struct-related attributes on typedefsXavier Leroy2019-02-254-8/+19
| | | | | | | | | | | | | | | | | | | | This commit adds a check to reject type definitions such as ``` typedef __attribute((section "foo")) int fooint; ``` GCC and Clang also reject this as an error. Without the check, the behavior is somewhat surprising: ``` fooint x; // placed in section "foo" fooint * x; // placed in default section, attribute "foo" is ignored ``` Note that the following must be accepted: ``` typedef struct { ... } __attribute((packed)) t; ``` The "packed" attribute is correctly attached to the struct type and should not be checked. This is achieved by using `attribute_of_type_no_expand` to get the attributes of the typedef-ed type, excluding the attributes carried by a struct/union or another typedef.
* Add regression test for "aligned" attributeXavier Leroy2019-02-253-1/+120
| | | | Expected results were obtained with GCC 5.4 and Clang 8.0
* Distinguish object-related and name-related attributesXavier Leroy2019-02-254-13/+24
| | | | | | | | | | | | | | | | | This is a second step towards mimicking GCC/Clang's handling of attributes. This commit introduces a distinction between - Object-related attributes, such as "section", which apply to the object (function, variable) being defined; - Name-related attributes, such as "aligned", which apply to the name (object, struct/union member, struct/union/enum tag) being defined. In particular, "aligned" is now attached to "struct" and "union" definitions, while it used to be "floated up" before. The C11 _Alignas modifier is treated like an object-related attribute, so that ``` struct s { ... }; _Alignas(64) struct s x; ``` correctly associates the alignment with "x" and not with "struct s", where it would be ignored because it was not part of the original definition of s.
* Do not expand type names when floating attributes "up" a declarationXavier Leroy2019-02-253-2/+24
| | | | | | | | | | | | | | | | | | | | | During elaboration of type declarators, non-type-related attributes such as "aligned" or "section" are "floated up" so that they apply to the thing being declared. For example, consider: ``` __attribute((aligned(16))) int * p; ``` The attribute is first attached to type `int`, then floated up to type `int *`, so that it finally applies to `p`, giving a 16-aligned pointer to int, and not a naturally-aligned pointer to 16-aligned int. What happens when the non-type-related attribute comes from a typedef? ``` typedef __attribute((aligned(16))) int i16; i16 * p; ``` CompCert used to expand the typedef then float up the attribute, resulting in `p` being a 16-aligned pointer to int. GCC and Clang produce a naturally-aligned pointer, so they do not expand the typedef before floating. The old CompCert behavior is somewhat surprising, and potentially less useful than the GCC/Clang behavior. This commit changes the floating up of non-type-related attributes so that typedefs and struct/union/enum definitions are not expanded when determining which attributes to float up. This is a first step towards mimicking the GCC/Clang behavior.
* Ignore and clean file .lia.cacheXavier Leroy2019-02-122-1/+4
| | | | This file is created by Coq when running some tactics
* Make the checker happy (#272)Vincent Laporte2019-02-123-19/+17
| | | Previously, the coqchk type- and proof-checker would take forever on some of CompCert's modules. This commit makes minimal changes to the problematic proofs so that all of CompCert can be checked with coqchk. Tested with Coq versions 8.8.2 and 8.9.0.
generated by cgit (git 2.34.1) at 2024-06-29 11:34:53 +0000