aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | | * Double rounding error in int64->float32 conversions on PowerPC and ARMXavier Leroy2020-03-304-24/+22
| | | * Add a test for int64 -> float32 conversionXavier Leroy2020-03-302-39/+838
| | | * Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-293-12/+25
| | * | -fduplicate -1 really desactivates the pass in Coq nowCyril SIX2020-04-013-7/+8
| | * | 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
generated by cgit (git 2.34.1) at 2024-07-11 22:49:43 +0000