aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | 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
* Deactivate options target dependend.Bernhard Schommer2016-06-242-110/+131
| | | | | | 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
* Driveraux.mli: fix documentation commentXavier Leroy2016-06-221-1/+1
|
* Added version string to Clightgen.Bernhard Schommer2016-05-241-1/+1
| | | | | | Clightgen now also prints a version string. Also the CompCert version string is now similar in both modes. Bug 18768.
* Moved shared frontend code in own file.Bernhard Schommer2016-05-246-275/+327
| | | | | | | 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
* Moved some system functions into own module.Bernhard Schommer2016-05-243-68/+120
| | | | | | The process handling is now in its own file, like the output name generation etc. Bug 18768
* Added option to pass linker options to gcc.Bernhard Schommer2016-05-131-0/+2
| | | | | | | | 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.
* bug 18004, fix file extensions for dparse optionMichael Schmidt2016-04-251-1/+1
|
* Enabled Werror via command line option.Bernhard Schommer2016-04-251-0/+1
| | | | | | The new command line option -Werror activates the treatment of warnings as errors. Bug 18004
* 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
generated by cgit (git 2.34.1) at 2024-06-26 18:19:40 +0000