aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Fix cutrewrite deprecatedCyril SIX2020-04-011-3/+4
* Removing 8.8.* versions of coq in configureCyril SIX2020-04-011-1/+1
* do not run check-admitted alwaysDavid Monniaux2020-03-311-0/+8
* move check-admitted elsewhereDavid Monniaux2020-03-311-2/+6
* forgot imageDavid Monniaux2020-03-311-0/+1
* add check-admittedDavid Monniaux2020-03-311-0/+6
* forgot an 'Admitted'David Monniaux2020-03-311-1/+1
* Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-03-3128-380/+1194
|\
| * fix typo in hfDavid Monniaux2020-03-291-1/+1
| * fix mismatch between hardware FP and software FP on ARMDavid Monniaux2020-03-293-3/+28
| * Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-283-5/+44
| |\
| | * fix MakefileDavid Monniaux2020-03-281-17/+0
| | * More YarpgenDavid Monniaux2020-03-282-5/+30
| | * Run Yarpgen in CIDavid Monniaux2020-03-283-47/+142
| | * disable leaf function removal of return address restoration due to memcpy ove...David Monniaux2020-03-273-7/+13
| | * Run tests on various targets in addition to compilingDavid Monniaux2020-03-277-13/+49
| | * Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-273-5/+38
| | |\
| | | * better epilogue proofDavid Monniaux2020-03-251-8/+18
| | | * removed RA restorationDavid Monniaux2020-03-253-4/+27
| * | | remove host .s generationDavid Monniaux2020-03-281-1/+1
| * | | use gcc -m32 on ia32David Monniaux2020-03-281-1/+1
| * | | remove tests wrt hostDavid Monniaux2020-03-282-2/+2
| * | | Debian is not like Ubuntu on multilib!David Monniaux2020-03-281-1/+1
| * | | yet another problem with 32-bit armDavid Monniaux2020-03-281-1/+1
| * | | fixup for armDavid Monniaux2020-03-281-1/+1
| * | | enlarge stack sizeDavid Monniaux2020-03-281-5/+5
| * | | Merge branch 'mppa-ci' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert...David Monniaux2020-03-280-0/+0
| |\ \ \
| | * | | rm yarpgen on armDavid Monniaux2020-03-281-1/+1
| * | | | run also on IA32David Monniaux2020-03-281-4/+4
| * | | | run yarpgen correctly on armDavid Monniaux2020-03-282-4/+12
| |/ / /
| * | | limit due to stack overflowsDavid Monniaux2020-03-281-1/+1
| * | | more fixes for CIDavid Monniaux2020-03-282-3/+3
| * | | run yarpgen on other architecturesDavid Monniaux2020-03-281-0/+4
| * | | fix inconsistencyDavid Monniaux2020-03-281-8/+7
| * | | better assemble with gccDavid Monniaux2020-03-281-2/+3
| * | | fix limitxyDavid Monniaux2020-03-281-1/+1
| * | | stdlib pathDavid Monniaux2020-03-281-3/+5
| * | | run yarpgen test on aarch64David Monniaux2020-03-281-1/+2
| * | | some more Makefile fixes (disable cse2 it's too slow)David Monniaux2020-03-281-1/+1
| * | | fix targets for proper generationDavid Monniaux2020-03-281-2/+5
| * | | fix Makefile (again)David Monniaux2020-03-281-9/+10
| * | | fix Makefile for not remaking the generatorDavid Monniaux2020-03-281-13/+13
| * | | set up for autogeneration of yarpgenDavid Monniaux2020-03-281-7/+22
| * | | cleaner make invocationDavid Monniaux2020-03-281-5/+5
| * | | Makefile for CIDavid Monniaux2020-03-282-24/+93
| * | | we still need a ppc64 compilerDavid Monniaux2020-03-271-0/+1
| * | | disable testing on ppc64David Monniaux2020-03-271-2/+0
| * | | +xDavid Monniaux2020-03-271-0/+0
| * | | temporarily disable raytracer test on ARMDavid Monniaux2020-03-271-1/+1
| * | | more configDavid Monniaux2020-03-272-2/+24