Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1 | Cyril SIX | 2021-06-01 | 1 | -0/+1 |
|\ | |||||
| * | Adding distinction between kvx-cos and kvx-mbr (for trapping loads) | Cyril SIX | 2021-04-13 | 1 | -0/+1 |
| | | |||||
* | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵ | Cyril SIX | 2021-06-01 | 1 | -4/+5 |
| | | | | | | | | cfrontend/C2C.ml | ||||
* | | Merge branch 'master' into merge_master_8.13.1 | Sylvain Boulmé | 2021-03-23 | 1 | -1/+18 |
|\ \ | |/ |/| | | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed | ||||
| * | Silence some new warnings of Coq 8.13 | Xavier Leroy | 2021-01-21 | 1 | -1/+17 |
| | | | | | | | | | | | | | | | | Either because the code change that would silence the warning is not desirable, or because it would break compatibility with earlier versions of Coq. Explain the silenced warnings as comments in the Makefile. | ||||
| * | Replace `omega` tactic with `lia` | Xavier Leroy | 2020-12-29 | 1 | -1/+1 |
| | | | | | | | | | | | | | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. | ||||
| * | 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 |
| |\ \ | |/ / |/| | | | | | | | | | | | Conflicts: Makefile configure | ||||
| * | | 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 |
| | | | | | | | | | | | | configure flags -use-external-Flocq and -use external-MenhirLib. | ||||
| | * | Added missing semicolon. | Bernhard Schommer | 2020-07-15 | 1 | -1/+1 |
| | | | |||||
| | * | Bytecode-only build, continued | Xavier Leroy | 2020-07-15 | 1 | -0/+9 |
| | | | | | | | | | | | | | | | | | | | | | If ocamlopt is not available, use ocamlc instead of ocamlopt to build auxiliary tools (tools/modorder, tools/ndfun). This is a follow-up to commit 9af28924. | ||||
| | * | 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 |
| | | | | | | | | | | | | | | | | | | | | | Based on testing with beta-1 release. The deprecation warning about the "omega" tactic is ignored while we decide when to switch to "lia" instead. | ||||
| | * | Install "compcert.config" file along the Coq development | Xavier Leroy | 2020-04-29 | 1 | -1/+18 |
| | | | | | | | | | | | | | | | | | | | | | | | | The file contains various parameters about the target processor and ABI, useful for VST and possibly other users of CompCert as a Coq library. It is in "var=val" syntax so that it can be included directly from a Makefile or a shell script. | ||||
| | * | Simplify the generation of driver/Version.ml | Bernhard Schommer | 2020-04-27 | 1 | -3/+8 |
| | | | | | | | | | | | | Don't use sed, just echo the contents of the file. | ||||
* | | | 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 |
|/ / |