aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Fixing packedstruct issuev3.7_mppa_2020-04-01Cyril SIX2020-04-012-15/+15
* Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-0112-80/+926
|\
| * Updates for release 3.7v3.7Xavier Leroy2020-03-311-1/+1
| * Updates for release 3.7Xavier Leroy2020-03-312-1/+6
| * Update ChangelogXavier Leroy2020-03-311-3/+34
| * 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