aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | | | better patch for running the test suiteDavid Monniaux2019-03-221-0/+13
| * | | | Now we have division, simplify the patch.David Monniaux2019-03-221-50/+0
| |/ / /
| * | | rm Pdiv / PdivuDavid Monniaux2019-03-226-66/+1
| * | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-224-3/+36
| |\ \ \
| | * | | Risc-V works again (32/64).David Monniaux2019-03-224-3/+36
| * | | | seems like powerpc runs but the result segfaultsDavid Monniaux2019-03-224-3/+36
| |/ / /
| * | | ARM repasseDavid Monniaux2019-03-224-3/+36
| * | | restructuration pour compilation toute archiDavid Monniaux2019-03-223-1/+5
| * | | ça recompile sur x86David Monniaux2019-03-2215-110/+166
| * | | Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-2215-624/+43
| |\| |
| | * | I think it should now compile for all architectures.David Monniaux2019-03-221-613/+0
| | * | try to be portable across archsDavid Monniaux2019-03-2114-11/+43
* | | | rm tests inherited from Risc-VDavid Monniaux2019-03-201-30/+5
|/ / /
* | | csmith for testingDavid Monniaux2019-03-201-0/+23
* | | Makefile for ocamlrun testingDavid Monniaux2019-03-201-0/+7
* | | ocaml byterunner exampleDavid Monniaux2019-03-20119-0/+45174
* | | Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-202-9/+8
|\| |
| * | XLeroy's suggested fix for shared float/int register file.David Monniaux2019-03-202-5/+5
| * | Revert "Better fix for register allocation?"David Monniaux2019-03-201-4/+3
* | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-202-9/+24
|\ \ \
| * | | Proof of div32/mod32/divf32/divf64 lemmasCyril SIX2019-03-202-9/+24
* | | | rm need for gccDavid Monniaux2019-03-202-4/+2
|/ / /
* | | use the original source codesDavid Monniaux2019-03-2030-5528/+5235
* | | picomus compile aussiDavid Monniaux2019-03-201-1/+1
* | | picosat fonctionneDavid Monniaux2019-03-202-3/+7
* | | la division flottante fonctionneDavid Monniaux2019-03-208-14/+67
* | | begin float divisionDavid Monniaux2019-03-202-3/+7
* | | vire des scories INT_DIV et INT_MODDavid Monniaux2019-03-205-6/+6
* | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-203-8/+49
|\ \ \
| * | | Proving eval_divs_baseCyril SIX2019-03-203-8/+49
* | | | Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2019-03-200-0/+0
|\| | |
| * | | Fix for CompCert not recognizing the _i32 external callsCyril SIX2019-03-201-0/+2
* | | | les divisions entieres passentDavid Monniaux2019-03-205-9/+54
* | | | sdiv worksDavid Monniaux2019-03-202-1/+15
* | | | ça semble passerDavid Monniaux2019-03-201-2/+4
* | | | Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-2028-1645/+724
|\ \ \ \ | |/ / / |/| / / | |/ /
| * | Merge branch 'mppa-madd' into mppa_postpassDavid Monniaux2019-03-209-25/+86
| |\ \
| | * | maddl / maddlim are synthesized (but not for pointers it seems)David Monniaux2019-03-205-6/+34
| | * | maddl gets to assemblyDavid Monniaux2019-03-201-2/+0
| | * | maddl declaredDavid Monniaux2019-03-203-17/+52
| * | | Merge branch 'mppa-madd' into mppa_postpassDavid Monniaux2019-03-1916-1357/+327
| |\| |
| | * | mul+madd immediateDavid Monniaux2019-03-194-3/+28
| | * | mul immediateDavid Monniaux2019-03-196-3/+18
| | * | mul immediate beginDavid Monniaux2019-03-199-4/+32
| | * | fix classes for maddDavid Monniaux2019-03-191-4/+4
| | * | reverse maddDavid Monniaux2019-03-192-0/+4
| | * | seems to workDavid Monniaux2019-03-191-0/+7
| | * | Merge branch 'mppa-madd' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-03-192-17/+33
| | |\ \
| | | * | improve robustness of Asmblockdeps.arith_op_eq.Sylvain Boulmé2019-03-191-13/+29
| | | * | fix missing case in Asmblockdeps.arith_op_eqSylvain Boulmé2019-03-191-2/+2
generated by cgit (git 2.34.1) at 2024-07-11 22:30:40 +0000