aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'master' into cleanupBernhard Schommer2016-03-213-162/+265
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-202-154/+257
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-061-5/+7
| | |
| | * Strengthen the main compiler correctness results to account for separate ↵Xavier Leroy2016-03-061-149/+250
| | | | | | | | | | | | | | | | | | 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.
| * | Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-151-2/+2
| |/ | | | | | | | | | | 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.
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-152-39/+39
| | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* | Code cleanup.Bernhard Schommer2016-03-103-60/+68
|/ | | | | | 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 more support for gcc options.Bernhard Schommer2016-03-021-4/+75
| | | | | | | | | | | | | | | | | | | | | | | 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
* Merge remote-tracking branch 'origin/configuration-split'Bernhard Schommer2016-02-291-3/+12
|\
| * 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.
* | Added gcc's Xassembler option.Bernhard Schommer2016-02-291-3/+8
| | | | | | | | | | | | | | 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
* | Fixed typo. Bug 18066Bernhard Schommer2016-02-291-3/+4
| |
* | Added some gcc linker options.Bernhard Schommer2016-02-261-0/+22
|/ | | | | | | | | | | CompCert now recognizes the gcc linker options: -nostartfiles -nodefaultlibs -nostdlib -s -Xlinker <opt> -u <symb> Bug 18066.
* bug 18209, make message compatible to clangMichael Schmidt2016-02-231-1/+1
|
* bug 18209, check that input files existMichael Schmidt2016-02-231-0/+14
|
* Added new option for static linking.Bernhard Schommer2016-02-161-0/+2
| | | | | The new option -static passes the -static flag to the linker. Bug 18066.
* Fixed regression introduced by refactoring of Driver.ml.Bernhard Schommer2016-02-151-3/+7
|
* Added gcc cmd-line option -include.Bernhard Schommer2016-02-031-0/+3
| | | | | | | 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.
* Added version and compiler working directory to options dump.Bernhard Schommer2016-01-271-0/+4
|
* Added new option -doptions.Bernhard Schommer2016-01-272-4/+58
| | | | | | The new options dumps the compiler options in a json file per. This includes the clflags, compcert.ini and machine settings. Bug 17988.
* Added printer for Configuration and finished Clflags.Bernhard Schommer2016-01-253-69/+122
|
* Started implementing a printer for Clflags.Bernhard Schommer2016-01-252-0/+42
|
* Added option to dump preprocessed source code.Bernhard Schommer2016-01-222-4/+13
| | | | The new option -dprepro allows it to keep the preprocessed source code files.
* More descriptive error message for failed command.Bernhard Schommer2016-01-111-4/+14
| | | | | | | 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
* add options for include paths also to the command line of the assembler, bug ↵Michael Schmidt2015-12-231-2/+4
| | | | 17838
* Merge pull request #79 from AbsInt/config-optionXavier Leroy2015-12-192-8/+31
|\ | | | | Add "-conf <filename>" command-line option. Support relative paths for stdlib and tools.
| * Removed the open Filename.Bernhard Schommer2015-12-111-9/+8
| |
| * Add a target option.Bernhard Schommer2015-12-112-3/+7
| | | | | | | | | | | | 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
* | Revise and simplify the -fstruct-return and -fstruct-passing options.Xavier Leroy2015-12-082-33/+9
|/ | | | | | - 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.
* New option --conf.Bernhard Schommer2015-11-262-18/+31
| | | | | The option --conf allows it to overwrite the compcert.ini file. Bug 17431.
* Separate assembler options for the diab backend.Bernhard Schommer2015-11-201-1/+4
| | | | | | The diab backend calls the assembler directly and does not call the compiler like for the gcc based backends. Fix 17668.
* Added the compilation unit in the json export. Bug 17659.Bernhard Schommer2015-11-191-4/+4
|
* Added now option to control debug output.Bernhard Schommer2015-11-162-3/+10
| | | | | | | | | | | 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.
* Harden Driver.command against EINTR errorsXavier Leroy2015-11-101-1/+5
| | | | 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.
* New option to control the debug information build.Bernhard Schommer2015-11-042-0/+3
| | | | | | The new option -gonly-global allows the generation of debuging information for global variables only. Bug 17566.
* Added additional option for the renaming of the suffix of the sdumpBernhard Schommer2015-10-231-2/+6
| | | | | | | | file. The new option -sdump-suffix allows it to specify another suffix for the sdump file. Bug 17326
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-202-16/+10
|\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: arm/TargetPrinter.ml backend/CMparser.mly backend/SelectLongproof.v backend/Selectionproof.v cfrontend/C2C.ml checklink/Asm_printers.ml checklink/Check.ml checklink/Fuzz.ml common/AST.v debug/DebugInformation.ml debug/DebugInit.ml debug/DwarfPrinter.ml debug/DwarfTypes.mli debug/Dwarfgen.ml exportclight/ExportClight.ml ia32/TargetPrinter.ml powerpc/Asm.v powerpc/SelectOpproof.v powerpc/TargetPrinter.ml
| * Do not dump the .sdump files.Bernhard Schommer2015-10-161-15/+2
| | | | | | | | Bug 16529.
| * Implemented the usage of DW_AT_ranges for non-contiguous address ranges.Bernhard Schommer2015-10-162-1/+8
| | | | | | | | | | | | | | | | | | | | The gcc produces DW_AT_ranges for non-contiguous address ranges, like compilation units containing functions which are placed in different ELF-sections or lexical scopes that are split up. With this commit CompCert also uses this DWARF v3 feature for gnu backend based targets. In order to ensure backward compability a flag is added which avoids this and produces debug info in DWARF v2 format. Bug 17392.
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-142-36/+36
| |
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-145-18/+18
| |
* | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-207-54/+54
| |
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-3/+3
|/ | | | | | | | | | The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.
* Push the linker args separate.Bernhard Schommer2015-10-061-2/+4
|
* More refactoring of the Debug Information.Bernhard Schommer2015-09-271-1/+1
| | | | | | | In order to remove unnecessary dependecies the implemenation type is made and the DebugInit file initializes the fields in the record. This allows it to move more functions behind the Debug interface without introducing circular dependencies.
* Move more functionality in the new interface.Bernhard Schommer2015-09-161-4/+5
| | | | | | Added functions to add more information to the debuging interface, like the struct layout with offsets, bitifiled layout and removed the no longer needed mapping from stamp to atom.
* Add the debug interface file.Bernhard Schommer2015-09-161-0/+1
| | | | | | | | The new file Debug.ml contains the interface for generating and printing debug information. In order to generate debug information the init function initializes the necessary functions depending on the -g flag. If the -g is not there all functions are dummy functions which do nothing.
* Merge branch 'new-builtins'Bernhard Schommer2015-09-013-3/+14
|\
generated by cgit (git 2.34.1) at 2024-06-29 04:35:08 +0000