Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | some more testing | David Monniaux | 2019-03-22 | 1 | -1/+1 |
* | uses yarpgen random generator | David Monniaux | 2019-03-22 | 1 | -0/+37 |
* | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | David Monniaux | 2019-03-22 | 85 | -17/+259 |
|\ | |||||
| * | Rajout de tests test/mppa pour division/modulo | Cyril SIX | 2019-03-22 | 6 | -0/+34 |
| * | Merge branch 'mppa_postpass' into mppa-mul | Cyril SIX | 2019-03-22 | 82 | -30/+238 |
| |\ | |||||
| | * | Reorganized the test/mppa/ tests to have fewer of them | Cyril SIX | 2019-03-22 | 82 | -30/+238 |
* | | | better patch for running the test suite | David Monniaux | 2019-03-22 | 1 | -0/+13 |
* | | | Now we have division, simplify the patch. | David Monniaux | 2019-03-22 | 1 | -50/+0 |
|/ / | |||||
* | | rm Pdiv / Pdivu | David Monniaux | 2019-03-22 | 6 | -66/+1 |
* | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | David Monniaux | 2019-03-22 | 4 | -3/+36 |
|\ \ | |||||
| * | | Risc-V works again (32/64). | David Monniaux | 2019-03-22 | 4 | -3/+36 |
* | | | seems like powerpc runs but the result segfaults | David Monniaux | 2019-03-22 | 4 | -3/+36 |
|/ / | |||||
* | | ARM repasse | David Monniaux | 2019-03-22 | 4 | -3/+36 |
* | | 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 |
|\| | |||||
| * | 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 |
* | | 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 |
|\| | |||||
| * | 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-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 |
|\ \ \ | |/ / |/| / | |/ | |||||
| * | 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 |