| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof | Léo Gourdin | 2021-02-11 | 8 | -61/+248 |
| * | [Admitted checker] Adding cbranch expansions (without scratch) to the checker | Léo Gourdin | 2021-02-10 | 2 | -5/+7 |
| * | [Admitted checker] Checker expansion for reg Ocmp (without scratch) | Léo Gourdin | 2021-02-10 | 4 | -36/+36 |
| * | Adding pathmap psize modification during expansion oracle | Léo Gourdin | 2021-02-08 | 1 | -9/+20 |
| * | Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-work | Léo Gourdin | 2021-02-08 | 1 | -1/+1 |
| |\ | |||||
| | * | fix OpWeights | David Monniaux | 2021-01-30 | 1 | -1/+1 |
| * | | cond and branches expanded | Léo Gourdin | 2021-02-06 | 8 | -293/+691 |
| * | | All Ocmp expanded in RTL | Léo Gourdin | 2021-02-03 | 7 | -202/+417 |
| * | | Ccomp for long | Léo Gourdin | 2021-02-03 | 8 | -52/+408 |
| * | | Ccompu expansion | Léo Gourdin | 2021-02-02 | 8 | -178/+223 |
| * | | Expansion of Ccompimm in RTL [Admitted checker] | Léo Gourdin | 2021-02-02 | 8 | -4/+383 |
| |/ | |||||
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-08 | 5 | -26/+136 |
| |\ | |||||
| | * | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 11 | -242/+577 |
| | |\ | |||||
| | * \ | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 5 | -26/+136 |
| | |\ \ | |||||
| | | * | | Support the use of already-installed MenhirLib and Flocq libraries | Xavier Leroy | 2020-09-21 | 1 | -2/+1 |
| | | * | | Add __builtin_sqrt as synonymous for __builtin_fsqrt | Xavier Leroy | 2020-07-27 | 1 | -1/+1 |
| | | * | | RISC-V implementation of __builtin_clz* and __builtin_ctz* | Xavier Leroy | 2020-07-27 | 2 | -0/+134 |
| | | * | | No need to process __builtin_fabs in $ARCH/Asmexpand.ml | Xavier Leroy | 2020-07-27 | 1 | -2/+0 |
| | | * | | Move shared code in new file. | Bernhard Schommer | 2020-06-28 | 2 | -18/+0 |
| | | * | | Remove the `can_reserve_register` function. | Bernhard Schommer | 2020-06-28 | 2 | -3/+0 |
| | | * | | Use Hashtbl.find_opt. | Bernhard Schommer | 2020-06-28 | 1 | -1/+1 |
| * | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-02 | 9 | -239/+553 |
| |\ \ \ \ | | |_|/ | |/| | | |||||
| | * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-24 | 2 | -3/+14 |
| | |\ \ \ | |||||
| | * | | | | allow changing the target core | David Monniaux | 2020-10-22 | 2 | -120/+160 |
| | * | | | | attempt at modeling Rocket | David Monniaux | 2020-10-22 | 1 | -0/+83 |
| | * | | | | proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass sched... | Sylvain Boulmé | 2020-10-17 | 1 | -0/+10 |
| | * | | | | so that all architectures compile | David Monniaux | 2020-10-02 | 2 | -8/+16 |
| | * | | | | Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepass | David Monniaux | 2020-09-21 | 6 | -239/+390 |
| | |\ \ \ \ | |||||
| | | * | | | | risc-V now without trapping instructions | David Monniaux | 2020-09-21 | 4 | -74/+90 |
| | | * | | | | moved Risc-V div ValueAOp to central location | David Monniaux | 2020-09-21 | 1 | -293/+0 |
| | | * | | | | maketotal mod & div | David Monniaux | 2020-09-21 | 6 | -165/+593 |
| | | | |/ / | | |/| | | |||||
| | * | | | | wrong resources | David Monniaux | 2020-09-18 | 1 | -1/+1 |
| | * | | | | EH1 scheduling | David Monniaux | 2020-09-18 | 1 | -5/+18 |
| | * | | | | bogus OpWeights for Risc-V | David Monniaux | 2020-09-18 | 1 | -0/+19 |
| | |/ / / | |||||
| * | | | | op_depends_on_memory_correct | David Monniaux | 2020-11-25 | 1 | -6/+24 |
| * | | | | cond_valid_pointer_eq | David Monniaux | 2020-11-25 | 1 | -0/+10 |
| * | | | | pointer_eq copied | David Monniaux | 2020-11-25 | 1 | -0/+10 |
| | |/ / |/| | | |||||
| * | | | fix bug #223 on Risc-V | David Monniaux | 2020-11-23 | 2 | -3/+14 |
| |/ / | |||||
| * | | Adding copyrights | Cyril SIX | 2020-05-04 | 3 | -0/+38 |
| * | | Merge remote-tracking branch 'origin/mppa-licm' into mppa-features | David Monniaux | 2020-04-20 | 2 | -3/+11 |
| |\ \ | |||||
| | * | | test whether the instructions are allowed | David Monniaux | 2020-04-19 | 1 | -0/+2 |
| | * | | porting to ppc riscV x86 | David Monniaux | 2020-04-01 | 1 | -3/+9 |
| * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-thread | David Monniaux | 2020-04-08 | 5 | -207/+329 |
| |\| | | |||||
| | * | | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-work | David Monniaux | 2020-03-26 | 1 | -7/+10 |
| | |\| | |||||
| | | * | Update the RISC-V calling conventions, continued (#227) | Xavier Leroy | 2020-03-02 | 1 | -7/+10 |
| | * | | riscV/DuplicateOpcodeHeuristic.ml | David Monniaux | 2020-03-17 | 1 | -3/+27 |
| | * | | fixes for risc-V | David Monniaux | 2020-03-03 | 1 | -1/+1 |
| | * | | fix for risc-V | David Monniaux | 2020-03-03 | 1 | -9/+7 |
| | * | | fixed CSE2 for mppa_k1c | David Monniaux | 2020-03-03 | 2 | -0/+149 |
| | |\ \ | |||||
| | | * | | CSE2 alias analysis for Risc-V | David Monniaux | 2020-03-03 | 2 | -0/+149 |
| | | |/ | |||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |