Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge branch 'master' into merge_master_8.13.1 | Sylvain Boulmé | 2021-03-23 | 1 | -1/+18 |
|\ | |||||
| * | Silence some new warnings of Coq 8.13 | Xavier Leroy | 2021-01-21 | 1 | -1/+17 |
| * | Replace `omega` tactic with `lia` | Xavier Leroy | 2020-12-29 | 1 | -1/+1 |
| * | Update Flocq to 3.4.0 (#383) | Guillaume Melquiond | 2020-12-28 | 1 | -0/+1 |
* | | Separate target_op_simplify for riscV | Léo Gourdin | 2021-02-23 | 1 | -0/+1 |
* | | intro RTLpathWFcheck | Sylvain Boulmé | 2021-02-08 | 1 | -1/+1 |
* | | Fix "undefined lexer token" in extraction/extraction.v | Cyril SIX | 2021-01-26 | 1 | -1/+1 |
* | | Val_cmp* -> Val.mxcmp* | Sylvain Boulmé | 2021-01-07 | 1 | -3/+7 |
* | | fix extraction of non-aarch64 targets | Sylvain Boulmé | 2020-12-17 | 1 | -4/+9 |
* | | Merge branch 'kvx-work' into aarch64-peephole | Sylvain Boulmé | 2020-12-17 | 1 | -14/+75 |
|\ \ | |||||
| * \ | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 1 | -3/+22 |
| |\ \ | |/ / |/| | | |||||
| * | | Fixing compilation for KVX | Cyril SIX | 2020-12-04 | 1 | -1/+3 |
| * | | fix Makefile pour kvx | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| * | | un peu de progrès sur le Makefile | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| * | | Asmgenproof1 pas sur kvx | David Monniaux | 2020-11-19 | 1 | -1/+5 |
| * | | fix Makefile | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| * | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 1 | -15/+68 |
| |\| | |||||
| | * | Support the use of already-installed MenhirLib and Flocq libraries | Xavier Leroy | 2020-09-21 | 1 | -7/+23 |
| | * | Added missing semicolon. | Bernhard Schommer | 2020-07-15 | 1 | -1/+1 |
| | * | Bytecode-only build, continued | Xavier Leroy | 2020-07-15 | 1 | -0/+9 |
| | * | Introduce additional "branch" build information. | Bernhard Schommer | 2020-07-08 | 1 | -1/+4 |
| | * | Preliminary support for Coq 8.12 | Xavier Leroy | 2020-06-21 | 1 | -1/+1 |
| | * | Install "compcert.config" file along the Coq development | Xavier Leroy | 2020-04-29 | 1 | -1/+18 |
| | * | Simplify the generation of driver/Version.ml | Bernhard Schommer | 2020-04-27 | 1 | -3/+8 |
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 1 | -1/+1 |
|\| | | |||||
| * | | Adding Duplicatepasses.v to Makefile | Cyril SIX | 2020-10-27 | 1 | -1/+1 |
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 1 | -0/+1 |
|\| | | |||||
| * | | reorder phases | David Monniaux | 2020-10-16 | 1 | -0/+1 |
* | | | fixing the move of the verified prepass scheduler into scheduling/ directory | Sylvain Boulmé | 2020-10-17 | 1 | -1/+1 |
* | | | ccomp.force target for forcing compilation without Coq processing | David Monniaux | 2020-10-01 | 1 | -0/+4 |
* | | | just missing OpWeights for AARCH64 | David Monniaux | 2020-09-16 | 1 | -4/+13 |
* | | | starting to move common files | David Monniaux | 2020-09-16 | 1 | -1/+1 |
|/ / | |||||
* | | automated writing Compiler.v | David Monniaux | 2020-04-22 | 1 | -1/+1 |
* | | begin scripting the Compiler.v file | David Monniaux | 2020-04-21 | 1 | -0/+5 |
* | | Merge remote-tracking branch 'origin/mppa-licm' into mppa-features | David Monniaux | 2020-04-20 | 1 | -1/+3 |
|\ \ | |||||
| * | | attempt at compiling | David Monniaux | 2020-04-01 | 1 | -0/+1 |
| * | | use inject_l | David Monniaux | 2020-03-30 | 1 | -1/+1 |
| * | | more on injection | David Monniaux | 2020-03-30 | 1 | -0/+1 |
| * | | nop insertion at entrypoint | David Monniaux | 2020-03-29 | 1 | -1/+1 |
* | | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-features | David Monniaux | 2020-04-12 | 1 | -0/+2 |
|\ \ \ | |/ / |/| | | |||||
| * | | reloading and exploiting seems to work | David Monniaux | 2020-04-08 | 1 | -0/+1 |
| * | | begin installing profiling | David Monniaux | 2020-04-08 | 1 | -0/+1 |
* | | | pass to insert a nop at start position in functions | David Monniaux | 2020-03-27 | 1 | -0/+1 |
* | | | starts compiling but still fake | David Monniaux | 2020-03-10 | 1 | -1/+1 |
* | | | just the analysis | David Monniaux | 2020-03-05 | 1 | -1/+1 |
* | | | fix Makefile | David Monniaux | 2020-03-05 | 1 | -0/+1 |
* | | | more about extraction and linking | David Monniaux | 2020-03-05 | 1 | -0/+1 |
|/ / | |||||
* | | try to get it to compile | David Monniaux | 2020-03-03 | 1 | -0/+1 |
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-14 | 1 | -1/+1 |
|\ \ | |||||
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2020-02-08 | 1 | -1/+1 |
| |\| |