aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* -fbranch-probabilitiesDavid Monniaux2020-04-081-1/+2
* reloading and exploiting seems to workDavid Monniaux2020-04-088-15/+72
* fixed a bug in support libraries; reload profiling infoDavid Monniaux2020-04-085-8/+42
* library support for writing profiling information to filesDavid Monniaux2020-04-083-4/+65
* print profiling idsDavid Monniaux2020-04-081-3/+23
* looks like it works?David Monniaux2020-04-082-4/+39
* print hashesDavid Monniaux2020-04-086-13/+28
* so that it gets printedDavid Monniaux2020-04-081-0/+3
* installed Profiling (not finished)David Monniaux2020-04-085-25/+273
* begin installing profilingDavid Monniaux2020-04-0810-54/+73
* begin profiling stuffDavid Monniaux2020-04-081-0/+57
* added EF_profilingDavid Monniaux2020-04-087-15/+77
* 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