aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
* Add -main option to specify entrypoint function in interpreter mode (#374)Xavier Leroy2020-10-303-19/+41
| | | | | | | When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function. This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option. The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0.
* Remove -version-file optionXavier Leroy2020-10-121-19/+2
| | | | It is specific to AbsInt's commercial version of CompCert.
* Add missing comment for print_version_file_and_exitChristoph Cullmann2020-07-301-0/+1
|
* No trailing commas for --version-file option.Bernhard Schommer2020-07-091-1/+1
|
* Fix typo.Bernhard Schommer2020-07-081-1/+1
|
* Revert "Use the same version string."Bernhard Schommer2020-07-081-3/+10
| | | | This reverts commit 1a01ad629109cdb60fddae3787e3a589d20e9790.
* Use the same version string.Bernhard Schommer2020-07-081-10/+3
| | | | | | The version string dumped in the file should be the same as the version string printed by `-version`. The option is also not printed by `-help` since it is for internal use only.
* Remove no longer needed option enforce-buildnrBernhard Schommer2020-07-081-10/+1
|
* Introduce additional "branch" build information.Bernhard Schommer2020-07-081-3/+5
|
* Add option to print version information in fileBernhard Schommer2020-07-081-1/+17
|
* Move Commandline to the lib/ directoryXavier Leroy2020-05-052-196/+0
| | | | | | The Commandline module is reusable in other projects, and its license (GPL) allows such reuse, so its natural place is in lib/ rather than in driver/
* Move reserved_registers to CPragmas.Bernhard Schommer2020-04-201-0/+1
| | | | | | | The list of reserved_registers is never reset between the compilation of multiple files. Instead of storing them in IRC they are moved in the CPragmas file and reset in the a new reset function for Cpragmas whic is called per file.
* Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-211-2/+2
| | | | | | "open!" is the form used in the examples in the OCaml manual. Based on a quick poll it seems to be the preferred form of the OCaml core dev team.
* Refine the type of function results in AST.signatureXavier Leroy2020-02-211-1/+1
| | | | | | | | | | Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions.
* AArch64 portXavier Leroy2019-08-082-1/+2
| | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* Remove the cparser/Builtins moduleXavier Leroy2019-07-171-1/+1
| | | | | | | | | Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`.
* -O0 now implies -fno-inliningMichael Schmidt2019-07-091-1/+1
|
* Compatibility with OCaml 4.08 (#302)Xavier Leroy2019-07-081-2/+2
| | | | | | | | | | | | | | | | * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300
* Update documentation of -ObranchlessXavier Leroy2019-07-051-1/+1
| | | | Updated man page + better usage message.
* Rename option `-ffavor-branchless` into `-Obranchless`Xavier Leroy2019-07-052-4/+4
| | | | | Easier to type, and consistent with `-Os` (optimize for smaller code / optimize for fewer conditional branches).
* If-conversion optimizationXavier Leroy2019-06-062-2/+10
| | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-312-3/+3
| | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
* Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-102-0/+3
| | | | | | | | | | The option -fcommon controls whether uninitialized global variables are placed in the COMMON section. If the option is given in the negated form, -fno-common, variables are not placed in the COMMON section. They are placed in the same sections as gcc does. If the variables are not placed in the COMMON section merging of tentative definitions is inhibited and multiple definitions lead to a linker error, as it does for gcc.
* Change to AbsInt version string.Bernhard Schommer2019-05-101-2/+2
| | | | | The AbsInt build number no longer contains "release", so it must be printed additionally.
* Expand the responsefiles earlierBernhard Schommer2019-05-103-13/+13
| | | | | | | | | * Move the expansion of response files to module Commandline, during the initialization of `Commandline.argv`. This way we're sure it's done exactly once. * Make `Commandline.argv` a `string array` instead of a `string array ref`. We no longer need to update it after initialization! * Improve reporting of errors during expansion of response files.
* Check for alignment of command-line switches.Bernhard Schommer2019-05-101-3/+7
| | | | | | Add a check for alignment on command-line switches `-falign-*`. The check is similar to the one for the alignment attribute and ensures that only powers of two can be specified.
* Define macros with CompCert's version number (#284)Xavier Leroy2019-03-271-2/+24
| | | | | | | | | | | | | | | | 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
* Fix passing of -u to linker.Bernhard Schommer2018-08-211-1/+1
| | | | | | Instead of just passing -u to the linker also pass the value of the option to the linker. Bug 24316
* Add sizeof_reg and new Machine configurations (#129)Bernhard Schommer2018-08-201-4/+6
| | | | | | | | | | | | | 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
* Various improvements in the wording of diagnostics.Michael Schmidt2018-08-026-12/+12
| | | | | | Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850
* Typo in -iquote preprocessing option (#239)Frédéric Besson2018-06-201-1/+1
| | | The `-iquote` option was passed to the GNU preprocessor as `-iquore`
* Simplify module Complements and add separate compilation (#121)Xavier Leroy2018-05-291-74/+172
| | | | | | | | | | | | | | | | | * Simplify the theorems about preservation of specifications (section 2) There were three theorems, transf_c_program_preserves_spec, _safety_spec, and _liveness_spec) with the first being needlessly general and the last being hard to understand. Plus, the "liveness" and "safety" terminology wasn't very good. Replaced by two theorems: - transf_c_program_preserves_spec, which is the theorem previously named _safety_spec and talks about specifications that exclude going-wrong behaviors; - transf_c_program_preserves_initial_trace, which is an instance of the theorem previously named _liveness_spec, and now talks about a single initial trace of interest rather than a set of such traces. Added named definitions for properties of interest. Added more explanations. * Added theorems that talk about separate compilation (section 3) These are the theorems from section 1 and 2 but reformulated in terms of multiple C source compilation units being separately compiled to Asm units then linked together.
* Define C11 conditional feature macros (#77)Bernhard Schommer2018-04-061-1/+10
| | | | | | | | 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
* Removed struct passing/return from ConfigurationsBernhard Schommer2018-02-162-49/+0
|
* Move struct passing/return style to Machine.Bernhard Schommer2018-02-161-1/+5
| | | | | | Since the used configuration for passing and returning values struct values is pretty much static it can be hardwired into the machine settings.
* Added error summary in case of fatal error.Bernhard Schommer2018-02-091-1/+1
|
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-088-70/+64
| | | | | | | | | | | | | | | | | * 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.
* Share code for common options.Bernhard Schommer2018-01-292-61/+105
| | | | | | In order to avoid more divergence between the command line options of clightgen and ccomp the code for the common options, the language support options, the version string and the general options.
* Move machine initialization to Frontend.init function. (#49)Bernhard Schommer2018-01-113-22/+29
| | | | | 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.
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-051-45/+3
|
* Added toolchain specific option for dcc. (#47)Bernhard Schommer2018-01-051-1/+16
| | | | | | CompCert now accepts the target configuration option of the diab data compiler and passes it on to the preprocessor, assembler and linker. Bug 20521
* Handle dcompcertc and dparsedc like all dump opts.Bernhard Schommer2018-01-042-13/+5
| | | | | This time with the correct place for setting the destination files. Bug 20521
* Remove duplicated code. Bug 20521Bernhard Schommer2018-01-041-46/+26
|
* Remove all temporary files at program exit (#46)Bernhard Schommer2018-01-033-18/+16
| | | | | | | | | Replaced calls to Filename.temp_file by own version Driveraux.tmp_file. The Driveraux.tmp_file function takes care that the temporary files are removed at exit. Consequently there is no need to explicitly remove temp files in Driver.
* Export configured architecture to JSON (#38)Michael Schmidt2017-12-131-0/+6
| | | The architecture which was configured is now exported in a new top-level json field.
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-072-1/+5
| | | | | | | | | New inlining heuristic for static functions. Static functions that are only called once can always be inlined, since they can be removed safely after inlining and no call prologue, epilogue, as well as register saving and needs to be generated.
* Remove temporary .o files after linking (#36)Xavier Leroy2017-11-271-2/+5
| | | | | | | When -c is not given, .o files are now generated in /tmp, but they are still not erased. This commit uses an "at_exit" action to erase those temporary .o files before CompCert exits. Using at_exit is easier to implement than explicit erasure (like we do for other temporary files), yet should not result in temporary files lingering in /tmp longer than strictly necessary, since the call to the linker is the last thing that CompCert does before exiting, hence temporary .o files are erased just after the linker returns.
* New support for inserting ais-annotations.Bernhard Schommer2017-10-192-0/+5
| | | | | | | | | | | | The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call.
* Do not generate object files for linking.Bernhard Schommer2017-10-161-7/+14
| | | | | | If CompCert is called to compile and link object files should not be created. Bug 22399
* Added dump-mnemonics option.Bernhard Schommer2017-09-251-2/+12
| | | | | | This option allows it to dump a list of all used mnemonics into a file. Bug 22239
generated by cgit (git 2.34.1) at 2024-06-28 21:38:40 +0000