aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.ml
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-0/+1
|\
| * Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-131-0/+1
| |
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-1/+1
|\ \ | |/ |/| | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * "macosx" is now called "macos"Xavier Leroy2021-01-181-1/+1
| | | | | | | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
* | k1c -> kvx changesDavid Monniaux2020-05-261-1/+1
| |
* | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-201-1/+1
|\| | | | | | | mppa-work-upstream-merge
| * AArch64 portXavier Leroy2019-08-081-1/+1
| | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-031-3/+3
|\| | | | | | | mppa-if-conversion
| * Expand the responsefiles earlierBernhard Schommer2019-05-101-3/+3
| | | | | | | | | | | | | | | | | | * 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.
* | Hook for MPPA_K1c (generates Risc-V code for now)Cyril SIX2018-04-041-1/+1
|/
* Removed struct passing/return from ConfigurationsBernhard Schommer2018-02-161-28/+0
|
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-0/+2
| | | | | | | | | | | | The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call.
* RISC-V port and assorted changesXavier Leroy2017-04-281-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Introduced configuration variable for gnu systems.Bernhard Schommer2017-02-131-15/+11
| | | | | | | The variable gnu_toolchain is true if a gnu toolchain is used and false in all other cases. The variable avoids the explicit test whether the system string is diab and should be easier to change. Bug 20521.
* remove unused file, update tests for arch-field of configuration filesMichael Schmidt2016-11-031-1/+1
|
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-1/+1
| | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* fix merge conflictsMichael Schmidt2016-08-171-0/+12
|\
| * Added support for quoting for diab backend.Bernhard Schommer2016-07-211-0/+2
| | | | | | | | | | | | 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/+10
| | | | | | | | | | | | | | | | 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
* | Implement support for big endian arm targets.Bernhard Schommer2016-08-051-0/+5
|/ | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* Activate advanced debug information for arm, ia32.Bernhard Schommer2016-06-281-7/+1
| | | | | | The configuration advanced debug is removed and now full debug information is also generated for ia32 and arm. Bug 17609
* Split up tools and options.Bernhard Schommer2016-02-251-3/+12
| | | | | | Added additional configuration entries to seperate tools from options in the .ini files. Internally they are just concatenated in Configuration.ml which allows it to still use old .ini files.
* Removed the open Filename.Bernhard Schommer2015-12-111-9/+8
|
* Add a target option.Bernhard Schommer2015-12-111-2/+5
| | | | | | This option allows it to specify a .ini file that is in the usual search path. Bug 17431
* Allow relative paths for the tools.Bernhard Schommer2015-12-011-10/+21
| | | | | | | | The tools now can be specified by 3 ways: -Relative to the compcert.ini file -With absolute path to the location -As a simple filename which lies on the PATH variable. Bug 17431
* Allow relative library path.Bernhard Schommer2015-11-301-2/+11
| | | | | | The path to the libcompert folder can be specified relative to the location of the compcert.ini file. Bug 17431
* New option --conf.Bernhard Schommer2015-11-261-18/+30
| | | | | The option --conf allows it to overwrite the compcert.ini file. Bug 17431.
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-6/+6
|
* Added the directory ../share/compcert to the search path for .ini files and ↵Bernhard Schommer2015-08-231-9/+12
| | | | replaced the if else for the different possibilities by a List.find.
* Removed the version from the compcert.ini file and add it again in a ↵Bernhard Schommer2015-07-011-1/+0
| | | | separate file.
* Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-251-0/+5
| | | | | | | | | | | | This branch provides implementations of the following standard headers: <float.h> <stdarg.h> <stdbool.h> <stddef.h> <varargs.h> These are the headers that are provided by GCC and Clang, as opposed to being provided by Glibc and similar C standard libraries. Configuration flag "-no-standard-headers" deactivates the installation and use of these headers. Lightly tested so far (IA32 Linux).
* Merge branch 'master' into dwarfBernhard Schommer2015-03-311-0/+27
|\ | | | | | | | | | | Conflicts: Makefile driver/Driver.ml
| * Improvements in the StructReturn transformation (ABI conformance for passing ↵Xavier Leroy2015-03-201-0/+27
| | | | | | | | | | | | | | | | 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.
* | Started implementing the printing functions for the debug info. Added a ↵Bernhard Schommer2015-03-161-0/+6
|/ | | | global target dependend option to activate the printing only for targets wher it works.
* Use Unix.create_process instead of Sys.command (continued).Xavier Leroy2014-12-291-62/+63
|
* Stdlib path is ignored when the configuration has_runtime_lib is set to false.Bernhard Schommer2014-12-151-2/+7
|
* Removed unused variable and changed the search for the installation ↵Bernhard Schommer2014-12-041-1/+1
| | | | directory. Use Sys.executable_name instead of Sys.argv.(0).
* Removed environment variable for the stdlib_path and added a new variable ↵Bernhard Schommer2014-10-061-11/+15
| | | | for the configuration file.
* Change the way the tools like the linker, assembler, etc. are specified by ↵Bernhard Schommer2014-09-301-0/+86
including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
generated by cgit (git 2.34.1) at 2024-05-20 05:15:25 +0000