| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Merge remote-tracking branch 'origin/kvx-work-ssa' into kvx-test-prepass-ssa | David Monniaux | 2020-10-28 | 1 | -3/+46 |
| |\ | |||||
| | * | Merge remote-tracking branch 'origin/kvx-work' into kvx-work-ssa | David Monniaux | 2020-10-27 | 1 | -1/+2 |
| | |\ | |||||
| | * \ | Merge branch 'ssa' of https://gitlab.inria.fr/compcertssa/compcertssa into kv... | David Monniaux | 2020-07-17 | 1 | -3/+48 |
| | |\ \ | |||||
| | | * | | Global renaming of files in the middle-end | Delphine Demange | 2020-07-08 | 1 | -10/+10 |
| | | * | | Global cleanup of code base. | Delphine Demange | 2020-07-07 | 1 | -1/+1 |
| | | * | | Use CompCert's Maps interface. | Delphine Demange | 2020-07-05 | 1 | -1/+1 |
| | | * | | SCCP optimization support for all architectures, with reuse of | Delphine Demange | 2020-07-03 | 1 | -1/+1 |
| | | * | | Adding property about CSSA live-ranges to the Makefile | Delphine Demange | 2020-07-01 | 1 | -1/+1 |
| | | * | | Merge tag 'v3.7' into ssa | DEMANGE Delphine | 2020-06-17 | 1 | -1/+1 |
| | | |\ \ | |||||
| | | * \ \ | Merge tag 'v3.6' into ssa | DEMANGE Delphine | 2020-06-17 | 1 | -40/+45 |
| | | |\ \ \ | |||||
| | | * \ \ \ | Merge tag 'v3.5' into ssa | DEMANGE Delphine | 2020-06-17 | 1 | -5/+2 |
| | | |\ \ \ \ | |||||
| | | * | | | | | Adding benchs for ssa mode | DEMANGE Delphine | 2020-06-16 | 1 | -0/+3 |
| | | * | | | | | Merge tag 'v3.4' into ssa | DEMANGE Delphine | 2020-06-16 | 1 | -12/+7 |
| | | |\ \ \ \ \ | |||||
| | | * \ \ \ \ \ | Merge tag 'v3.3' into ssa | DEMANGE Delphine | 2020-06-16 | 1 | -4/+11 |
| | | |\ \ \ \ \ \ | |||||
| | | * | | | | | | | SSA middle-end for compcert v3.2 | DEMANGE Delphine | 2020-06-12 | 1 | -3/+38 |
| * | | | | | | | | | 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 |
| | |\ \ \ \ \ \ \ | | | |_|_|_|_|/ | | |/| | | | | | |||||
| | | * | | | | | | Support Coq 8.11.0 (#212) | Xavier Leroy | 2020-02-05 | 1 | -1/+1 |
| | | | |_|_|_|/ | | |/| | | | | |||||
| * | | | | | | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2 | David Monniaux | 2020-01-28 | 1 | -0/+1 |
| |\ \ \ \ \ \ \ | |/ / / / / / |/| | | | | | | |||||
| | * | | | | | | CSE2 split in two files | David Monniaux | 2020-01-28 | 1 | -0/+1 |
| | |/ / / / / | |||||
| * | | | | | | connect forward-moves to compiler | David Monniaux | 2020-01-08 | 1 | -0/+1 |
| * | | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-12-02 | 1 | -0/+1 |
| |\ \ \ \ \ \ | |||||
| | * | | | | | | Stubs for Duplicate pass | Cyril SIX | 2019-09-03 | 1 | -0/+1 |
| * | | | | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-non-tra... | David Monniaux | 2019-09-10 | 1 | -0/+1 |
| |\ \ \ \ \ \ \ | |/ / / / / / |/| / / / / / | |/ / / / / | |||||
| * | | | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2019-08-28 | 1 | -0/+1 |
| |\| | | | | | |||||
| | * | | | | | Coq 8.10 compatibility: (temporarily) silence new warning | Xavier Leroy | 2019-08-05 | 1 | -0/+1 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |