aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)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
| | | | | | | | | | | | | | | | | | The "stof" and "utof" runtime functions contain a round-to-odd step that avoids double rounding. However, this step was incorrectly coded on PowerPC (stof and utof), PowerPC64 (utof), and ARM (stof), making round-to-odd ineffective and causing double rounding. Closes: #343
| * Add a test for int64 -> float32 conversionXavier Leroy2020-03-302-39/+838
| | | | | | | | | | This is a special value that causes double rounding with the naive conversion schema int64 -> float64 -> float32.
| * Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-293-12/+25
| | | | | | | | | | | | | | | | Introduce an error message for section attributes with non string arguments,and another for multiple, ambiguous section attributes. This is more consistent with the handling of other attributes, like packed, than the old behavior of silently ignoring them.
* | -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 ↵David Monniaux2020-03-283-5/+44
| |\ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-ci
| | * | 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 ↵David Monniaux2020-03-273-7/+13
| | | | | | | | | | | | | | | | overwriting the return address register
| | * | 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 ↵David Monniaux2020-03-280-0/+0
| |\ \ \ \ | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-ci
| | * | | | rm yarpgen on armDavid Monniaux2020-03-281-1/+1
| | | | | |
| * | | | | run also on IA32David Monniaux2020-03-281-4/+4
| | | | | | | | | | | | | | | | | | | | | | | | remove -k
| * | | | | 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
| | | | |
generated by cgit (git 2.34.1) at 2024-06-13 08:56:50 +0000