| Commit message (Expand) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| | | * | | restructuration pour compilation toute archi | David Monniaux | 2019-03-22 | 3 | -1/+5 | |
| | | * | | ça recompile sur x86 | David Monniaux | 2019-03-22 | 15 | -110/+166 | |
| | | * | | Merge branch 'mppa_postpass' into mppa-mul | David Monniaux | 2019-03-22 | 15 | -624/+43 | |
| | | |\ \ | ||||||
| | * | | | | rm tests inherited from Risc-V | David Monniaux | 2019-03-20 | 1 | -30/+5 | |
| | |/ / / | ||||||
| | * | | | csmith for testing | David Monniaux | 2019-03-20 | 1 | -0/+23 | |
| | * | | | Makefile for ocamlrun testing | David Monniaux | 2019-03-20 | 1 | -0/+7 | |
| | * | | | ocaml byterunner example | David Monniaux | 2019-03-20 | 119 | -0/+45174 | |
| | * | | | Merge branch 'mppa_postpass' into mppa-mul | David Monniaux | 2019-03-20 | 2 | -9/+8 | |
| | |\ \ \ | ||||||
| | * \ \ \ | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | David Monniaux | 2019-03-20 | 2 | -9/+24 | |
| | |\ \ \ \ | ||||||
| | | * | | | | Proof of div32/mod32/divf32/divf64 lemmas | Cyril SIX | 2019-03-20 | 2 | -9/+24 | |
| | * | | | | | rm need for gcc | David Monniaux | 2019-03-20 | 2 | -4/+2 | |
| | |/ / / / | ||||||
| | * | | | | use the original source codes | David Monniaux | 2019-03-20 | 30 | -5528/+5235 | |
| | * | | | | picomus compile aussi | David Monniaux | 2019-03-20 | 1 | -1/+1 | |
| | * | | | | picosat fonctionne | David Monniaux | 2019-03-20 | 2 | -3/+7 | |
| | * | | | | la division flottante fonctionne | David Monniaux | 2019-03-20 | 8 | -14/+67 | |
| | * | | | | begin float division | David Monniaux | 2019-03-20 | 2 | -3/+7 | |
| | * | | | | vire des scories INT_DIV et INT_MOD | David Monniaux | 2019-03-20 | 5 | -6/+6 | |
| | * | | | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | David Monniaux | 2019-03-20 | 3 | -8/+49 | |
| | |\ \ \ \ | ||||||
| | | * | | | | Proving eval_divs_base | Cyril SIX | 2019-03-20 | 3 | -8/+49 | |
| | * | | | | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | David Monniaux | 2019-03-20 | 0 | -0/+0 | |
| | |\| | | | | ||||||
| | | * | | | | Fix for CompCert not recognizing the _i32 external calls | Cyril SIX | 2019-03-20 | 1 | -0/+2 | |
| | * | | | | | les divisions entieres passent | David Monniaux | 2019-03-20 | 5 | -9/+54 | |
| | * | | | | | sdiv works | David Monniaux | 2019-03-20 | 2 | -1/+15 | |
| | * | | | | | ça semble passer | David Monniaux | 2019-03-20 | 1 | -2/+4 | |
| | * | | | | | Merge branch 'mppa_postpass' into mppa-mul | David Monniaux | 2019-03-20 | 28 | -1645/+724 | |
| | |\ \ \ \ \ | | |/ / / / | |/| | | | | ||||||
| | * | | | | | added helper functions but strange | David Monniaux | 2019-03-19 | 8 | -95/+189 | |
| * | | | | | | check that gcc and ccomp compiled k1c code return the same | David Monniaux | 2019-03-22 | 1 | -2/+6 | |
| * | | | | | | improved testing | David Monniaux | 2019-03-22 | 1 | -5/+16 | |
| * | | | | | | uses yarpgen random generator | David Monniaux | 2019-03-22 | 1 | -0/+37 | |
| * | | | | | | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd) | David Monniaux | 2019-03-22 | 1 | -1/+1 | |
| | |_|_|_|/ |/| | | | | ||||||
| * | | | | | Reorganized the test/mppa/ tests to have fewer of them | Cyril SIX | 2019-03-22 | 82 | -30/+238 | |
| | |_|_|/ |/| | | | ||||||
| * | | | | I think it should now compile for all architectures. | David Monniaux | 2019-03-22 | 1 | -613/+0 | |
| * | | | | try to be portable across archs | David Monniaux | 2019-03-21 | 14 | -11/+43 | |
| | |_|/ |/| | | ||||||
| * | | | XLeroy's suggested fix for shared float/int register file. | David Monniaux | 2019-03-20 | 2 | -5/+5 | |
| * | | | Revert "Better fix for register allocation?" | David Monniaux | 2019-03-20 | 1 | -4/+3 | |
| | |/ |/| | ||||||
| * | | Merge branch 'mppa-madd' into mppa_postpass | David Monniaux | 2019-03-20 | 9 | -25/+86 | |
| |\ \ | ||||||
| | * | | maddl / maddlim are synthesized (but not for pointers it seems) | David Monniaux | 2019-03-20 | 5 | -6/+34 | |
| | * | | maddl gets to assembly | David Monniaux | 2019-03-20 | 1 | -2/+0 | |
| | * | | maddl declared | David Monniaux | 2019-03-20 | 3 | -17/+52 | |
| * | | | Merge branch 'mppa-madd' into mppa_postpass | David Monniaux | 2019-03-19 | 16 | -1357/+327 | |
| |\| | | ||||||
| | * | | mul+madd immediate | David Monniaux | 2019-03-19 | 4 | -3/+28 | |
| | * | | mul immediate | David Monniaux | 2019-03-19 | 6 | -3/+18 | |
| | * | | mul immediate begin | David Monniaux | 2019-03-19 | 9 | -4/+32 | |
| | * | | fix classes for madd | David Monniaux | 2019-03-19 | 1 | -4/+4 | |
| | * | | reverse madd | David Monniaux | 2019-03-19 | 2 | -0/+4 | |
| | * | | seems to work | David Monniaux | 2019-03-19 | 1 | -0/+7 | |
| | * | | Merge branch 'mppa-madd' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe... | David Monniaux | 2019-03-19 | 2 | -17/+33 | |
| | |\ \ | ||||||
| | | * | | improve robustness of Asmblockdeps.arith_op_eq. | Sylvain Boulmé | 2019-03-19 | 1 | -13/+29 | |
| | | * | | fix missing case in Asmblockdeps.arith_op_eq | Sylvain Boulmé | 2019-03-19 | 1 | -2/+2 | |
| | | * | | remove a FAILWITH that forbids some debugging information to be printed | Sylvain Boulmé | 2019-03-19 | 1 | -3/+3 | |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |