aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
Commit message (Collapse)AuthorAgeFilesLines
* Correct typo in Clightnorm.ml (#285)Alix Trieu2019-03-271-1/+1
| | | | In the `Sswitch` case, the original expression was used instead of the result of `norm_expr`.
* clightgen: add info on configuration and platform to generated .v files (#238)Xavier Leroy2018-06-202-4/+21
| | | | | Information about the run of clightgen is added to the generated .v file as definitions within a sub-module named Info. Closes: #226.
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-131-1/+1
| | | | | Init_space has an argument of type Z and it can exceed the range of a 32-bit integer. Reported by Frédéric Besson.
* 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.
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2018-01-171-3/+9
|\
| * Added type annotations for exported program. (#50)v3.2Bernhard Schommer2018-01-151-2/+2
| | | | | | | | Added types for global_definitions in order to avoid problems with implicit parameters. This should fix issue 215
| * Use Ptrofs.repr instead of Int.repr for Init_addrof. (#51)Bernhard Schommer2018-01-151-1/+7
| | | | | | | | This should fix issue 216 and also allows it to print 64 bit offsets.
* | 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
|
* Minor improvements.Bernhard Schommer2018-01-101-2/+2
|
* Change README to markdown.Bernhard Schommer2018-01-101-15/+14
|
* 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
|
* New support for inserting ais-annotations.Bernhard Schommer2017-10-191-2/+2
| | | | | | | | | | | | 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.
* Issue #199: improve namespace management for clightgen-produced filesXavier Leroy2017-08-282-16/+6
| | | | | Qualify imports in clightgen-produced files and in Clightdefs so that they can be used with coq -Q /path/to/compcert compcert. Remove 'Require Export' from Clightdefs as suggested in issue #199.
* Issue #196: excessive proof-checking times in .v files generated by clightgenXavier Leroy2017-08-152-13/+33
| | | | | | The check that "build_composite_env composites = OK (make_composite_env composites)" is taking time exponential on the number of struct/union definitions, at least on the example provided in #196. The solution implemented in this commit is to use computational reflection more efficiently, just to check that "build_composite_env composites" is of the form "OK _". From there, a new function Clightdefs.mkprogram produces the appropriate Clight.program without additional computation.
* clightgen: add option -normalize to ensure that memory loads never occur ↵Xavier Leroy2017-06-122-2/+177
| | | | | | | | | | | | | | | | | | | | | "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
* Issue #179: clightgen produces wrong abstract syntax for "switch" statementsXavier Leroy2017-04-281-3/+8
|
* Removed shadowing open.Bernhard Schommer2017-02-061-11/+11
|
* 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
* Fixed warning 45 for ExportClight.ml.Bernhard Schommer2016-05-281-1/+1
|
* 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.
* Escape all newlines.Bernhard Schommer2016-05-241-5/+5
| | | | 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
|
* Also refactor clightgen to work with new warnings. Bug 18394Bernhard Schommer2016-03-231-6/+6
|
* Merge branch 'master' into cleanupBernhard Schommer2016-03-211-0/+2
|\
| * Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-061-0/+2
| |
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-152-27/+27
| | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* | Cleanup of Clightgen code.Bernhard Schommer2016-03-102-45/+41
|/ | | | | Removed unused code and code generating warnings. Bug 18394
* Naming of compiler-generated temporariesXavier Leroy2016-02-051-32/+76
| | | | clightgen now gives semi-readable and relatively stable names of the form _t'1, _t'2, _t'3, etc, to compiler-generated temporaries, instead of the unreadable and unstable NNN%positive notation generated previously.
* clightgen: update to recent change -fstruct-return/-fstruct-passingXavier Leroy2015-12-191-4/+7
|
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-202-8/+8
|
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-113-14/+15
| | | | | | | | | | 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.
* Upgrade to reflect changes in type external_function.Xavier Leroy2015-10-111-4/+2
|
* Update clightgen w.r.t. teh calling_conventions record (new field cc_unproto).Xavier Leroy2015-08-171-1/+2
|
* Update clightgen w.r.t. EF_inline_asm (type of the clobber list).Xavier Leroy2015-08-171-1/+6
|
* Update clightgen to the new annotations and the new inline asm.Xavier Leroy2015-04-232-25/+10
|
* Update clightgen with respect to new representation of composites.Xavier Leroy2015-02-203-232/+151
|
* Refactoring in the printing of FP numbers.Xavier Leroy2014-09-241-8/+2
|
* Upgrade clightgen with the new features of CompCert 2.4 (single floats, etc).Xavier Leroy2014-09-241-7/+20
|
* Merge of "newspilling" branch:xleroy2014-07-231-3/+3
| | | | | | | | | | | | | | | - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update clightgen for CompCert 2.2.v2.2xleroy2014-02-233-17/+33
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2417 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-1/+0
| | | | | | | - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-26 18:55:45 +0000