aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.mli
Commit message (Collapse)AuthorAgeFilesLines
* Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-131-0/+3
|
* Removed struct passing/return from ConfigurationsBernhard Schommer2018-02-161-21/+0
|
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-0/+3
| | | | | | | | | | | | 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.
* Introduced configuration variable for gnu systems.Bernhard Schommer2017-02-131-0/+3
| | | | | | | 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.
* fix merge conflictsMichael Schmidt2016-08-171-0/+8
|\
| * Added support for quoting for diab backend.Bernhard Schommer2016-07-211-0/+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/+7
| | | | | | | | | | | | | | | | 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/+3
|/ | | | | | | | 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-3/+0
| | | | | | The configuration advanced debug is removed and now full debug information is also generated for ia32 and arm. Bug 17609
* Code cleanup.Bernhard Schommer2016-03-101-0/+11
| | | | | | Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394.
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-1/+1
|
* Removed the version from the compcert.ini file and add it again in a ↵Bernhard Schommer2015-07-011-2/+0
| | | | separate file.
* Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-251-0/+2
| | | | | | | | | | | | 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/+2
| | | | | | Conflicts: Makefile driver/Driver.ml
* Improvements in the StructReturn transformation (ABI conformance for passing ↵Xavier Leroy2015-03-201-0/+55
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.