aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
* Introduced configuration variable for gnu systems.Bernhard Schommer2017-02-137-28/+21
| | | | | | | 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.
* Merge branch 'elaboration-of-attributes'Xavier Leroy2017-02-061-0/+1
|\
| * Refactor the classification of attributesXavier Leroy2017-02-031-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Introduce Cutil.class_of_attribute to return the class of the given attribute: one among Attr_type attribute related to types (e.g. "aligned") Attr_struct attribute related to struct/union/enum types (e.g. "packed") Attr_function attribute related to function types (e.g. "noreturn") Attr_name attribute related to variable and function declarations (e.g. "section") Attr_unknown attribute was not declared Cutil.declare_attribute is used to associate a class to a custom attribute. Standard attributes (const, volatile, _Alignas, etc) are Attr_type. cfronted/C2C.ml: declare the few attributes that CompCert honors currently. cparser/GCC.ml: a bigger list of attributes taken from GCC, for reference only.
* | Remove overriding open in Interp.Bernhard Schommer2017-02-031-11/+11
|/
* Fixed indention of help.Bernhard Schommer2017-01-271-3/+3
|
* Added option -fmax-errors.Bernhard Schommer2017-01-262-0/+22
| | | | | | | The option -fmax-errors limits the number of errors that are reported before the compilation is aborted. The default 0 means no limit. Bug 19872
* Allow .sx files for preprocessed assembler files.Bernhard Schommer2017-01-251-0/+3
| | | | | GCC treats files with .sx extension in the same way as it treats files with .S suffix.
* Use quoted strings.Bernhard Schommer2017-01-184-127/+138
| | | | | | Instead of escaping all newlines etc for the help options use quoted strings. Bug 19872
* Added backtrace handler.Bernhard Schommer2017-01-171-0/+2
| | | | | | | | If CompCert crashes because of an uncaught exception the exception is caught toplevel and the backtrace is printed plus an additional message to include the backtrace in a support request, if buildnr and tag are available. Bug 20681.
* add parameter to enforce a specific compcert build number for QSKs (bug 20595)Michael Schmidt2016-12-161-2/+14
|
* Also exit on errors. Bug 19872Bernhard Schommer2016-12-151-1/+1
|
* Check errors at the end. Bug 19872Bernhard Schommer2016-12-151-0/+1
|
* remove unused file, update tests for arch-field of configuration filesMichael Schmidt2016-11-031-1/+1
|
* Merge pull request #145 from AbsInt/64Xavier Leroy2016-10-273-11/+14
|\ | | | | | | Support for 64-bit target processors + support for x86 in 64-bit mode
| * Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-271-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | -> 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).
| * driver/Interp: updateXavier Leroy2016-10-241-8/+8
| | | | | | | | | | Cherry-pick commit d1311e6 from trunk. Simplify convert_external_arg so that it works both in 32 and 64 bits.
| * Support for 64-bit architectures: update the PowerPC portXavier Leroy2016-10-011-456/+0
| | | | | | | | | | The PowerPC port remains 32-bit only, no support is added for PPC 64. This shows how much work is needed to update an existing port a minima.
| * Support for 64-bit architectures: generic supportXavier Leroy2016-10-013-4/+463
| | | | | | | | | | | | | | | | | | | | | | - 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.
* | Document -target and -conf. Bug 20210Bernhard Schommer2016-10-181-0/+2
| |
* | Refactored debugging options.Bernhard Schommer2016-10-142-29/+6
| | | | | | | | | | | | | | The options controlling the generation of debugging information are now moved into the Debug module. Futhermore the -gdepth options are replaced in favor of a more gcc compatible version. Bug 20193
* | Remove undocumented option. Bug 20193Bernhard Schommer2016-10-143-8/+2
| |
* | Fix minor typoMichael Schmidt2016-10-121-1/+1
| |
* | Fixed regression in printing of floats.Bernhard Schommer2016-10-041-1/+1
|/ | | | | Commit 60402c5 breaks printing of default floats by adding support for %lf. This commit adds back support for %f.
* Allow %lf type specifier in printf.Bernhard Schommer2016-09-221-1/+1
| | | | | %lf is official part of the C99 standard. Bug 19877
* Ignore also ignores the argunment. Bug 18004Bernhard Schommer2016-09-202-2/+7
|
* Merge pull request #139 from AbsInt/advanced-diagnosticsBernhard Schommer2016-09-203-31/+40
|\ | | | | Advanced diagnostics
| * Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-297-20/+93
| |\
| * | Additional test for color output.Bernhard Schommer2016-08-053-26/+33
| | | | | | | | | | | | | | | | | | Color output is only enabled if stderr is a tty, and the environment variable TERM is not empty or dumb. Bug 18004
| * | Classified all warnings and added various options.Bernhard Schommer2016-07-291-5/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now each warning either has a name and can be turned on/off, made into an error,etc. or is a warning that always will be triggered. The message of the warnings are similar to the ones emited by gcc/clang and all fit into one line. Furthermore the diagnostics are now colored if colored output is available. Bug 18004
* | | Added option to specify sdump folder. Fix 19816.Bernhard Schommer2016-09-161-2/+7
| |/ |/|
* | Merge pull request #118 from AbsInt/armebXavier Leroy2016-08-243-1/+11
|\ \ | | | | | | Support for ARM Big Endian
| * \ fix merge conflictsMichael Schmidt2016-08-177-10/+61
| |\ \
| * | | Implement support for big endian arm targets.Bernhard Schommer2016-08-053-1/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* | | | Print whole command line.Bernhard Schommer2016-08-221-8/+8
| |/ / |/| | | | | | | | | | | | | | | | | When response files are used CompCert should still print all command line arguments since the response file is deleted after usage. Bug 19297.
* | | Merge pull request #107 from AbsInt/add-fileXavier Leroy2016-08-176-8/+57
|\ \ \ | | | | | | | | Add support for response files
| * | | Moved quoting functions in ResponsefileBernhard Schommer2016-08-163-34/+8
| | | | | | | | | | | | | | | | | | | | | | | | Also corrected some typos and corrected exception handling for expandargv. Bug 18308
| * | | Added missing begin end around quoting. Bug 18308.Bernhard Schommer2016-08-101-2/+2
| | | |
| * | | Corrected diab quoting. Bug 18308Bernhard Schommer2016-07-211-8/+11
| | | |
| * | | Added support for quoting for diab backend.Bernhard Schommer2016-07-213-1/+20
| | | | | | | | | | | | | | | | | | | | | | | | 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-204-9/+31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| * | | Merged responfile function into command.Bernhard Schommer2016-07-195-49/+33
| | | | | | | | | | | | | | | | | | | | | | | | Command now decides whether to use a responsefile or call the external command directly. Bug 18004
| * | | Added heuristic for passing arg via responsefiles.Bernhard Schommer2016-07-125-11/+51
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Since gnu make and other tools under windows seem to have a limit of around 8000 bytes per command line the arguments should be passed via responsefiles instead. Bug 18308
| * | | Added responsefile support for commandline.Bernhard Schommer2016-07-082-1/+8
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Commandline can now be passed in a file specifed with @file on the Commandline. The quoting convention is similar to the one used by gcc, etc. Options are separated by whitespaces and options with whitespaecs need to be quoted. Bug 18303
* | | | Fixed issue with emulation of printfBernhard Schommer2016-08-171-2/+4
| |/ / |/| | | | | | | | | | | | | | The emulated printf in the interpreter did always return 0 instead of the numbers of bytes printed. Bug 19564
* | | Added -dall which enables all tracing.Bernhard Schommer2016-08-021-0/+12
| |/ |/|
* | add missing asmexpand step to cminor handler in driverMichael Schmidt2016-07-011-21/+27
|/
* Activate advanced debug information for arm, ia32.Bernhard Schommer2016-06-283-11/+1
| | | | | | The configuration advanced debug is removed and now full debug information is also generated for ia32 and arm. Bug 17609
* Also add braces for arm. Bug 19197Bernhard Schommer2016-06-241-2/+2
|
* Added braces back. Bug 19197Bernhard Schommer2016-06-241-16/+16
|
* Moved assembler and linker into own files.Bernhard Schommer2016-06-249-122/+210
| | | | | | The function to call the assembler and the linker are now in own files like the preprocessor. Bug 19197
generated by cgit (git 2.34.1) at 2024-06-28 21:57:19 +0000