| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As suggested in #282, it can be useful to #ifdef code depending on
specific versions of CompCert.
Assuming a version number of the form MM.mm ,
the following macros are predefined:
__COMPCERT_MAJOR__=MM (the major version number)
__COMPCERT_MINOR__=mm (the minor version number)
__COMPCERT_VERSION__=MMmm (two decimal digits for the minor, e.g. 305 for version 3.5)
We also define __COMPCERT_BUILDNR__ if the build number is not empty in file ./VERSION.
Closes: #282
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Since the size of integer registers is not identical to the size of pointers
for the ppc64 and e5500 model the check for register pairs in
ExtendedAsm does not work correctly.
In order to avoid this a new field sizeof_intreg is introduced in the
Machine configuration which describes the size of integer registers.
New configurations for the ppc64 and e5500 model are added
and used.
Bug 24273
|
| |
|
| |
The `-iquote` option was passed to the GNU preprocessor as `-iquore`
|
| |
|
|
|
|
|
|
| |
These macros can be defined to indicate that variable length
arrays, the _Complex type, atomics and threads are not supported.
Since the _Complex type is not supported, we also need
to undefine __STDC_IEC_559_COMPLEX__
Bug 23408
|
| |
|
|
|
|
| |
Since the used configuration for passing and returning values
struct values is pretty much static it can be hardwired into the
machine settings.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/
* Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the
Diagnostics module.
* Raise on error before calling external tools.
* Added diagnostics to clightgen.
* Fix error handling of AsmToJson.
* Cleanup error handling of Elab and C2C.
*The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
|
| |
|
|
|
| |
The initialization of Machine.config, as well as the calls to various initialization functions for the C front-end, are now performed by the new `Frontend.init` function.
This avoids code duplication in driver/Driver.ml and exportclight/Clightgen.ml.
|
| |
|
|
|
| |
This time with the correct place for setting the destination files.
Bug 20521
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
Instead of escaping all newlines etc for the help options use
quoted strings.
Bug 19872
|
| |
|
|
|
|
| |
The function to call the assembler and the linker are now in own
files like the preprocessor.
Bug 19197
|
| |
|
|
|
|
| |
Options only available for gnu systems or arm target arch are no
longer displayed in the help and cannot be selected any longer.
Bug 19197
|
|
|
Clightgen and CompCert share the code for preprocessing as well as
parsing C files. The code as well as command line switches is moved
in the new module Frontend.
Bug 18768
|
