Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | progressing on select/selectl | David Monniaux | 2019-03-25 | 2 | -0/+12 |
* | going forward with select/selectl | David Monniaux | 2019-03-25 | 1 | -12/+26 |
* | begin ternary | David Monniaux | 2019-03-24 | 2 | -1/+49 |
* | Merge branch 'mppa-mul' into mppa-ternary | David Monniaux | 2019-03-24 | 219 | -5819/+54280 |
|\ | |||||
| * | demo ternary op | David Monniaux | 2019-03-24 | 2 | -0/+49 |
| * | mysteriously slow code | David Monniaux | 2019-03-24 | 2 | -0/+70 |
| * | encore un essai de creduce | David Monniaux | 2019-03-23 | 3 | -0/+1561 |
| * | system for comparing speeds | David Monniaux | 2019-03-23 | 1 | -0/+12 |
| * | bitsliced AES in one file | David Monniaux | 2019-03-23 | 1 | -10/+85 |
| * | Test in one file only. | David Monniaux | 2019-03-23 | 1 | -0/+1467 |
| * | for testing with quest | David Monniaux | 2019-03-22 | 1 | -0/+24 |
| * | passage de structures en varargs (fonctionne avec une convention "passage par... | David Monniaux | 2019-03-22 | 1 | -0/+3 |
| * | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | David Monniaux | 2019-03-22 | 3 | -2/+54 |
| |\ | |||||
| | * | check that gcc and ccomp compiled k1c code return the same | David Monniaux | 2019-03-22 | 1 | -2/+6 |
| | * | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd) | David Monniaux | 2019-03-22 | 1 | -1/+1 |
| | * | improved testing | David Monniaux | 2019-03-22 | 1 | -5/+16 |
| | * | 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 | 136 | -877/+595 |
| |\| | |||||
| | * | 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 |
| | | |\ | |||||
| | * | | | 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 |
| | |\ \ | |||||
| * | | | | 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 |