aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.ml
Commit message (Collapse)AuthorAgeFilesLines
* 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.