aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight/Clightgen.ml
Commit message (Collapse)AuthorAgeFilesLines
* Fix tracing options for clightgen.Bernhard Schommer2019-07-151-10/+23
| | | | | | | | The clightgen tracing options did not result in printing of the intermediate files, but were ignored. Added also two new options, `-dprepro` to print the preprocessed file and `-dall` to dump all intermediate files.
* clightgen: add info on configuration and platform to generated .v files (#238)Xavier Leroy2018-06-201-1/+2
| | | | | Information about the run of clightgen is added to the generated .v file as definitions within a sub-module named Info. Closes: #226.
* Refactor the handling of errors and warnings (#44)Bernhard Schommer2018-02-081-15/+18
| | | | | | | | | | | | | | | | | * 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-291-70/+15
| | | | | | 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.
* Added missing help and common options.Bernhard Schommer2018-01-171-1/+15
| | | | | Clightgen also now has command line flags to control warnings as well as some other general options.
* Move machine initialization to Frontend.init function. (#49)Bernhard Schommer2018-01-111-20/+1
| | | | | 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.
* Added option -o to clightgen.Bernhard Schommer2018-01-111-5/+47
| | | Also allow preprocessed source files as input.
* Add riscv and attributes to ClightgenBernhard Schommer2018-01-101-0/+4
|
* Remove all temporary files at program exit (#46)Bernhard Schommer2018-01-031-1/+1
| | | | | | | | | 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.
* Use quoted strings in clightgen.Bernhard Schommer2018-01-021-22/+24
|
* clightgen: add option -normalize to ensure that memory loads never occur ↵Xavier Leroy2017-06-121-2/+11
| | | | | | | | | | | | | | | | | | | | | "deep" inside expressions For example, with this option, tmp = *(x + 0) + *(x + 1) in the original Clight is rewritten to tmp1 = *(x + 0) tmp2 = *(x + 1) tmp = tmp1 + tmp2 with two temporaries tmp1 and tmp2 introduced to name the intermediate results of memory loads. Squashed commit of the following: commit 3fb69dae567b1305383b74ce1707945f91369a46 commit 0071654b77a239c00bcbb92a5845447b2c4e9d2a commit c220ed303d9f3f36cc03c347a77b065a9362c0e7
* remove unused file, update tests for arch-field of configuration filesMichael Schmidt2016-11-031-1/+6
|
* Merge branch 'master' into advanced-diagnosticsBernhard Schommer2016-08-291-1/+3
|\
| * Implement support for big endian arm targets.Bernhard Schommer2016-08-051-1/+3
| | | | | | | | | | | | | | | | 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
* | Additional test for color output.Bernhard Schommer2016-08-051-10/+10
|/ | | | | | Color output is only enabled if stderr is a tty, and the environment variable TERM is not empty or dumb. Bug 18004
* Added version string to Clightgen.Bernhard Schommer2016-05-241-2/+14
| | | | | | 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-241-161/+28
| | | | | | | 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
* bug 18004, fix file extensions for dparse optionMichael Schmidt2016-04-251-1/+1
|
* Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-151-2/+2
| | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* Cleanup of Clightgen code.Bernhard Schommer2016-03-101-3/+2
| | | | | Removed unused code and code generating warnings. Bug 18394
* clightgen: update to recent change -fstruct-return/-fstruct-passingXavier Leroy2015-12-191-4/+7
|
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-2/+2
|
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-1/+1
| | | | | | | | | | 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.
* Update clightgen to the new annotations and the new inline asm.Xavier Leroy2015-04-231-1/+1
|
* Update clightgen with respect to new representation of composites.Xavier Leroy2015-02-201-97/+103
|
* Update clightgen for CompCert 2.2.v2.2xleroy2014-02-231-2/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2417 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* One more copyright header update.xleroy2013-06-171-1/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update LICENSE file and headers for dual-licensed files.xleroy2013-06-171-0/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2280 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updatedxleroy2013-04-301-3/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2219 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update clightgen to changes in Camlcoq and in AST.xleroy2013-03-201-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2156 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Put clighgen files in exportclight/xleroy2013-01-051-0/+282
Short doc in exportclight/README git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2089 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-29 14:12:02 +0000