aboutsummaryrefslogtreecommitdiffstats
path: root/configure
Commit message (Collapse)AuthorAgeFilesLines
* Install Coq development (.vo files) if requested (#232)Xavier Leroy2018-05-301-3/+26
| | | | | | | | | .vo files are installed if configure options -install-coqdev or -clightgen or -coqdevdir are given. Installation directory is $(PREFIX)/lib/compcert/coq by default and can be changed by configure option -coqdevdir. Closes: #227
* Support Coq version 8.8.0Xavier Leroy2018-04-251-3/+3
|
* Support Coq 8.7.2Xavier Leroy2018-02-191-3/+3
|
* Removed struct passing/return from ConfigurationsBernhard Schommer2018-02-161-40/+0
|
* Rename abi for ppc-linux targets.Bernhard Schommer2018-02-161-2/+2
|
* Fix typo in commentMichael Schmidt2018-02-161-1/+1
|
* Add support for x86_64 BSD (#56)Xavier Leroy2018-02-091-3/+19
|
* Configure check for PIE (#55)Michael Schmidt2018-02-081-5/+12
| | | | | When checking for -no-pie and -nopie, evaluate gcc output for error message like 'unknown argument'. (Relying on the error code is not enough.)
* Removed superfluous check.Bernhard Schommer2018-02-061-4/+0
|
* Improved message recommending an OCaml version to useXavier Leroy2018-01-131-1/+1
|
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-051-0/+3
| | | | | | | | | | | Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent. This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed. Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST which is not in lib/
* Coq 8.7.1 supportXavier Leroy2017-12-181-3/+3
| | | | It is compatible with 8.7.0 and 8.6.1, no changes required to the Coq sources of CompCert.
* Coq 8.7.0 supportXavier Leroy2017-10-201-3/+3
| | | | | | configure: accept Coq 8.7.0 and 8.6.1. (Coq 8.6 became incompatible with commit b4f59c4.) Changelog: updated.
* Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203)Gergö Barany2017-09-181-2/+9
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Clarify that ARMv6 is in fact ARMv6T2 The ARMv6 comes in two flavors depending on the version of the Thumb instruction set supported: ARMv6 for the original Thumb, ARMv6T2 for Thumb2. CompCert only supports Thumb2, so its ARMv6 architecture should really be called ARMv6T2. This makes a difference: the GNU assembler rejects most of the instructions CompCert generates for ARMv6 with "-mthumb" if the architecture is specified as ".arch armv6" as opposed to ".arch armv6t2". This patch fixes the architecture specification in the target printer and the internal name of the architecture. It does not change the configure script's flags to avoid breaking changes. * Always use ARM movw/movt to load large immediates These move-immediate instructions used to be only emitted in Thumb mode, not in ARM mode. As far as I understand ARM's documentation, these instructions are available in *both* modes in ARMv6T2 and above. This should cover all of CompCert's ARM targets. Tested for ARMv6 and ARMv7, both with and without Thumb2. The behavior is now identical to Clang, and the GNU assembler accepts these instructions in all configurations. * Separate ARMv6 and ARMv6T2; no movw/movt on ARMv6 - define separate architecture models for ARMv6 and ARMv6T2 - introduce `Archi.move_imm` parameter on ARM to identify models with `movw`/`movt` move-immediate instructions (all except ARMv6, in both ARM and Thumb mode) * Fixes for support for architectures with Thumb2 - rename relevant parameter to `Archi.thumb2_support` - on ARMv6 without Thumb2, silently accept -marm flag (but not -mthumb) - allow generation of `sbfx` in ARM mode if Thumb2 is supported
* configure for x86-32/Cygwin: ignore __attribute__Xavier Leroy2017-09-111-1/+1
| | | | Even with __GNUC__ undefined, the standard header files contain bizarre __attribute__ declarations that CompCert fails to parse.
* configure: Wording and formatting of the Skylake/OCaml warningXavier Leroy2017-08-181-2/+3
|
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2017-07-311-1/+3
|\
| * Mention rv32- and rv64- configurations in the help messageXavier Leroy2017-07-311-0/+2
| | | | | | | | These are the configurations for the new RISC-V port.
| * Accept Coq version 8.6.1 as supportedXavier Leroy2017-07-311-1/+1
| | | | | | | | 8.6.1 works just fine with the current CompCert.
* | Warning for Skylake/Kabylake systems.Bernhard Schommer2017-07-311-0/+4
|/
* use TMPDIR also for asm-cfi testMichael Schmidt2017-07-271-5/+5
|
* generalize test for compiler optionsMichael Schmidt2017-07-271-15/+22
|
* Add a -ignore-coq-version flag to configure (continued)Xavier Leroy2017-07-061-2/+2
| | | | These Coq people have version "numbers" that look nothing like numbers, such as "trunk". Also, they didn't test their pull request #188. Fixing this.
* Merge branch 'master' of github.com:AbsIntPrivate/CompCertBernhard Schommer2017-07-051-0/+30
|\
| * add check for -no-pie at configure-timeMichael Schmidt2017-07-041-0/+30
| |
* | Add a -ignore-coq-version flag to configure (continued)Xavier Leroy2017-07-051-1/+1
| | | | | | | | Typo in configure help message.
* | Add a -ignore-coq-version flag to configureXavier Leroy2017-07-051-2/+10
|/ | | | | Pull request #188 from Maxime Dénès. This flag makes it easier for the Coq people to test CompCert with in-development versions of Coq.
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
* Always generate .merlin and _CoqProject files.Bernhard Schommer2017-04-281-19/+7
|
* Add a switch to generate a _CoqProject file.Bernhard Schommer2017-02-231-0/+22
|
* Bump required version of Menhir to 20161201.Maxime Dénès2017-01-091-1/+1
| | | | Menhir's Coq backend has been updated to support Coq 8.6.
* Configure now expects to find Coq 8.6.0.Maxime Dénès2017-01-091-3/+3
|
* Removed folders from .merlin.Bernhard Schommer2016-11-091-4/+0
|
* Added ${arch}_${bitsize} for x86 to .merlinBernhard Schommer2016-11-091-1/+4
|
* allow Cow version 8.5pl3Michael Schmidt2016-11-041-1/+1
|
* Merge pull request #145 from AbsInt/64Xavier Leroy2016-10-271-28/+86
|\ | | | | | | Support for 64-bit target processors + support for x86 in 64-bit mode
| * Documentation updates to mention 64-bit mode and x86_64 portXavier Leroy2016-10-271-5/+8
| |
| * Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-271-25/+33
| | | | | | | | | | | | | | | | | | | | | | | | -> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
| * configure for ia32-macosx: update for MacOS 10.12Xavier Leroy2016-10-131-1/+1
| |
| * x86-64 MacOS X supportXavier Leroy2016-10-111-0/+16
| | | | | | | | | | - Avoid absolute addressing for labels, use RIP-relative addressing - Different, RIP-relative implementation of jump tables
| * Support for 64-bit architectures: x86 in 64-bit modeXavier Leroy2016-10-011-4/+35
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model. To activate x86-64 bit support, configure with "x86_64-linux". Main steps: - Enrich Op.v and Asm.v with 64-bit operations - SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers - Conventions1: support x86-64 ABI in addition to the 32-bit ABI. - Add support for the new 64-bit operations everywhere. - runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode To do: - More optimizations are possible on 64-bit integer arithmetic operations. - Could add new chunks to load, say, an unsigned byte into a 64-bit long (currently we load as a 32-bit int then zero-extend). - Implements the wrong ABI for struct passing.
* | Merge pull request #147 from m-schmidt/masterXavier Leroy2016-10-241-0/+1
|\ \ | | | | | | Add a man page
| * | Add a man-pageMichael Schmidt2016-10-141-0/+1
| | |
* | | Query menhir for location of menhir lib in config.Bernhard Schommer2016-10-181-1/+3
|/ / | | | | | | | | | | Since the menhir version required supports the --suggest-menhirLib flag we can query it already in the configure script simplifying the Makefile.menhir
* / Added configure switch for merlin.Bernhard Schommer2016-10-061-0/+35
|/ | | | | | The new configure switch generates a .merlin file and adds the -bin-annot flag to the compile options. Bug 20081
* undefine _Nullable to add some compatibility with macOS 10.12 SDKMichael Schmidt2016-09-231-1/+1
|
* fix merge conflictsMichael Schmidt2016-08-171-0/+6
|\
| * Added support for quoting for diab backend.Bernhard Schommer2016-07-211-1/+1
| | | | | | | | | | | | The diab data compiler has different quoting conventions compared to the gnu tools. Bug 18308.
| * Added simplified reader and printer for gnu @filesBernhard Schommer2016-07-201-0/+6
| | | | | | | | | | | | | | | | The functions expandargv and writeargv resemble the functions from the libiberity that are used by the gnu tools. Additionaly a new configuration is added in order to determine which kind of response files are supported for calls to other tools. Bug 18308
* | update help text in configure scriptMichael Schmidt2016-08-081-13/+14
| |
generated by cgit (git 2.34.1) at 2024-06-29 05:52:32 +0000