Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | adding builtins | David Monniaux | 2021-02-01 | 4 | -6/+27 |
* | Obits_of_single etc | David Monniaux | 2021-02-01 | 3 | -3/+46 |
* | define some semantics in Asm | David Monniaux | 2021-02-01 | 2 | -3/+24 |
* | select_long | David Monniaux | 2021-01-30 | 1 | -0/+38 |
* | select through bitwise operations | David Monniaux | 2021-01-30 | 1 | -0/+40 |
* | 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 |
| | |/ | |||||
| * | | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe... | David Monniaux | 2020-03-03 | 11 | -39/+189 |
| |\ \ | | |/ | |/| | |||||
| * | | Update the RISC-V calling conventions (#221) | Xavier Leroy | 2020-02-26 | 2 | -137/+149 |
| * | | Platform-independent implementation of Conventions.size_arguments (#222) | Xavier Leroy | 2020-02-24 | 1 | -64/+0 |
* | | | Merge branch 'mppa-work' into mppa-thread | Cyril SIX | 2020-02-25 | 3 | -13/+18 |
|\ \ \ | |||||
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2020-02-24 | 3 | -13/+18 |
| |\| | | | |/ | |/| | |||||
| | * | Cosmetic: in OCaml code, write "open! Module" instead of "open !Module" | Xavier Leroy | 2020-02-21 | 1 | -1/+1 |