aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2020-04-201031-29150/+248508
|\
| * refine the rules for builtinsDavid Monniaux2020-04-162-5/+37
| * progress on CSE2 builtinsDavid Monniaux2020-04-162-31/+20
| * Coq error message update in configureCyril SIX2020-04-151-1/+1
| * Removed the assertion about prediction on ifsoCyril SIX2020-04-091-2/+3
| * Some cleaning on Linearize and DuplicateCyril SIX2020-04-082-95/+118
| * Duplicate: Common rtl_successors functionCyril SIX2020-04-081-61/+33
| * accept Coq 8.11.1David Monniaux2020-04-081-1/+1
| * Changing best_predecessor_of to not take None predictionsCyril SIX2020-04-031-4/+15
| * Fixing loop heuristicCyril SIX2020-04-021-15/+34
| * Stopping traces at join pointsCyril SIX2020-04-011-2/+25
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-branch-infoCyril SIX2020-04-0136-477/+2024
| |\
| | * 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
generated by cgit (git 2.34.1) at 2024-07-02 09:22:18 +0000