| Commit message (Collapse) | Author | Age | Files | Lines |
|\
| |
| |
| | |
Support for 64-bit target processors + support for x86 in 64-bit mode
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
-> 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).
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- 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.
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
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
|
| | |
|
|/ |
|
|\
| |
| | |
Advanced diagnostics
|
| |\ |
|
| | |
| | |
| | |
| | |
| | |
| | | |
Color output is only enabled if stderr is a tty, and the
environment variable TERM is not empty or dumb.
Bug 18004
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
|
| |/
|/| |
|
|\ \ |
|
| |\ \
| | | |
| | | | |
Add support for response files
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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
|
|/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
|
| |/
|/| |
|
|/ |
|
| |
|
|
|
|
|
|
| |
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 now also prints a version string. Also the CompCert version
string is now similar in both modes.
Bug 18768.
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
The process handling is now in its own file, like the output name
generation etc.
Bug 18768
|
|
|
|
|
|
|
|
| |
Some gcc options have influence on the linking (especially -march,
etc.). The new -WUl options allows it to pass the options to the
gcc called for linking instead of passing them to the linker
directly.
Bug 18949.
|
| |
|
|
|
|
|
|
| |
The new command line option -Werror activates the treatment of
warnings as errors.
Bug 18004
|
|
|
|
|
|
| |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Added the gcc options for the preprocessor:
-Xpreprocessor
-M
-MM
-MF
-MG
-MP
-MT
-MQ
-nostdinc
-imacros
-idirafter
-isystem
-iquote
-P
-C
-CC
Also warn for not supported GCC options in the diab case.
Bug 18066
|
|
|
|
|
|
|
| |
The Xassembler option passes one option to the assembler and can
be used to pass options to the underlying assembler that the gcc
driver does not recognize.
Bug 18066
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
CompCert now recognizes the gcc linker options:
-nostartfiles
-nodefaultlibs
-nostdlib
-s
-Xlinker <opt>
-u <symb>
Bug 18066.
|
| |
|
| |
|
|
|
|
|
| |
The new option -static passes the -static flag to the linker.
Bug 18066.
|
| |
|
|
|
|
|
|
|
| |
The -include option is passed to the preprocessor and -include <file>
is equivalent to writting #include "<file>" as first line in the
primary source file.
Bug 18066.
|
|
|
|
|
|
| |
The new options dumps the compiler options in a json file per.
This includes the clflags, compcert.ini and machine settings.
Bug 17988.
|
| |
|
| |
|
|
|
|
| |
The new option -dprepro allows it to keep the preprocessed source code files.
|
|
|
|
|
|
|
| |
CompCert now prints if the assembler, linker or preprocessor
command failed and a hint for the user to get the full command
line.
Bug 17894
|
|
|
|
| |
17838
|
|\
| |
| | |
Add "-conf <filename>" command-line option. Support relative paths for stdlib and tools.
|
| |
| |
| |
| |
| |
| | |
This option allows it to specify a .ini file that is in the usual
search path.
Bug 17431
|
|/
|
|
|
|
| |
- Rename '-fstruct-return' into '-fstruct-passing', because this emulation affects both function result passing and function argument passing. Keep '-fstruct-return' as a deprecated synonymous for '-fstruct-passing'
- Remove the ability to change the ABI for struct passing via the '-fstruct-passing=<abi>' and '-fstruct-return=<abi>' command-line flags. This was more confusing than useful.
- Produce an error if a struct/union is passed as function argument and '-fstruct-passing' is not set. This used to be supported, using CompCert's default ABI for passing struct arguments. However, this default ABI does not match any of the standard ABIs of our target platforms, so it is better to reject than to silently produce ABI-incompatible code.
|
|
|
|
|
| |
The option --conf allows it to overwrite the compcert.ini file.
Bug 17431.
|
|
|
|
|
|
| |
The diab backend calls the assembler directly and does not call
the compiler like for the gcc based backends.
Fix 17668.
|
| |
|