| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
The configuration advanced debug is removed and now full debug
information is also generated for ia32 and arm.
Bug 17609
|
| |
|
| |
|
|
|
|
|
|
| |
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
|
|\ |
|
| |\
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This pull request implements "approach A" to separate compilation in CompCert from the paper
Lightweight verification of separate compilation
by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis,
POPL 2016, pages 178-190
In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program.
This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
compilation and linking
Define a "match_prog" relation corresponding to the composition of CompCert's passes. Use it to show semantic preservation (backward/forward simulations) not just for the compilation of whole programs, but also for the separate compilation of multiple units followed by linking.
|
| |/
| |
| |
| |
| |
| | |
As suggested in GPR#84, use '%.15F' to force the printing of more significant digits. (The '%F' format previously used prints only 6.) This is enough to represent the FP number exactly most of the time (but not always).
Once OCaml 4.03 is out and CompCert switches to this version of OCaml, we'll be able to use hexadecimal floats for printing.
|
| |
| |
| |
| |
| |
| | |
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
|
|\ |
|
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| | |
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
|
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| |
| |
| |
| |
| |
| | |
The path to the libcompert folder can be specified relative to the
location of the compcert.ini file.
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
The new option gdepth subumes the gonly-globals. The option
allows it to control the level of information that is produced.
This option allows it to generate debugging inforation for:
-Only globals
-Global and local variables but without location information for
the local variable
-Full information
Bug 17638.
|
|
|
|
| |
Sometimes, Unix.waitpid returns early with a EINTR error code, e.g. if a signal was handled. (Observed while running ccomp under the lldb debugger in MacOS X). Just restart Unix.waitpid in this case.
|