aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* | | | | | | | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-0711-254/+240
* | | | | | | | directory postpass_libSylvain Boulmé2021-01-076-3/+3
* | | | | | | | recreate abstractbb/Sylvain Boulmé2021-01-075-2/+2
* | | | | | | | cleaningSylvain Boulmé2021-01-0711-10296/+1
* | | | | | | | lia instead of omega in libLéo Gourdin2021-01-041-51/+51
* | | | | | | | CI test with 12.2Léo Gourdin2021-01-043-13/+22
* | | | | | | | Fix Asmblockgenproof after mergeLéo Gourdin2020-12-201-8/+20
* | | | | | | | Merge remote-tracking branch 'origin/aarch64-asmblockgenproof' into aarch64-p...Léo Gourdin2020-12-2010-1302/+4274
|\ \ \ \ \ \ \ \
| * | | | | | | | CleanupLéo Gourdin2020-12-195-1269/+919
| * | | | | | | | CI 11.2Léo Gourdin2020-12-191-12/+12
| * | | | | | | | Asmblockgenproof finished !Léo Gourdin2020-12-192-215/+132
| * | | | | | | | Some progress in AsmblockgenproofLéo Gourdin2020-12-174-1494/+566
| * | | | | | | | intermediatet commit before builtinsLéo Gourdin2020-12-166-99/+3292
| * | | | | | | | Generals lemmas for asmblockgenproofLéo Gourdin2020-12-144-13/+896
| * | | | | | | | Removing the PseudoAsm IRLéo Gourdin2020-12-137-46/+303
* | | | | | | | | Merge branch 'aarch64-peephole-tofix' into aarch64-peepholeLéo Gourdin2020-12-20169-2435/+4361
|\ \ \ \ \ \ \ \ \
| * | | | | | | | | Fix the Asmblock/Asm proofLéo Gourdin2020-12-203-34/+26
| * | | | | | | | | fix builtin_sqrtSylvain Boulmé2020-12-171-1/+1
| * | | | | | | | | fix extraction of non-aarch64 targetsSylvain Boulmé2020-12-174-6/+11
| * | | | | | | | | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-17167-2411/+4340
|/| | | | | | | | | | | |/ / / / / / / | |/| | | | | | |
| * | | | | | | | fix CI for x86_64Sylvain Boulmé2020-12-161-1/+1
| * | | | | | | | try coq.8.12.2 in the CISylvain Boulmé2020-12-161-12/+12
| * | | | | | | | add superblock-scheduling passes in the coqhtmlSylvain Boulmé2020-12-161-25/+62
| * | | | | | | | update the doc for CompCert 3.8Sylvain Boulmé2020-12-161-6/+12
| * | | | | | | | upgrade kvx backend to coq.8.12.2Sylvain Boulmé2020-12-167-34/+43
| | |_|/ / / / / | |/| | | | | |
| * | | | | | | fix installation problemsDavid Monniaux2020-12-111-1/+1
| * | | | | | | bad linkDavid Monniaux2020-12-111-1/+0
| | |/ / / / / | |/| | | | |
| * | | | | | Fixing wrong predictions on imbricated loopsCyril SIX2020-12-111-104/+114
| * | | | | | 8.11.2 partoutDavid Monniaux2020-12-111-10/+10
| * | | | | | try 8.11.2David Monniaux2020-12-111-1/+1
| * | | | | | bump Coq version in CIDavid Monniaux2020-12-111-11/+11
| * | | | | | Fixing exponential blowup on get_loop_info.mark_path.exploreCyril SIX2020-12-091-33/+44
| * | | | | | Flushing debug outputCyril SIX2020-12-091-1/+1
| * | | | | | The last fix for get_loop_info was giving false positives. Fixing that.Cyril SIX2020-12-081-2/+12
| * | | | | | Merge branch 'kvx-work' into kvx-work-dirtyCyril SIX2020-12-0820-670/+290
| |\ \ \ \ \ \ | | | |_|_|_|/ | | |/| | | |
| | * | | | | fix new register erasing scheme for AArch64David Monniaux2020-12-083-553/+241
| | * | | | | rm instructions now unusedDavid Monniaux2020-12-081-2/+1
| | | |_|_|/ | | |/| | |
| | * | | | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-0818-115/+48
| | |\ \ \ \
| | | * | | | Error when using -main without -interpXavier Leroy2020-12-061-0/+2
| | | * | | | PowerPC modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | | * | | | ARM modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | | * | | | AArch64 modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-8/+11
| | | * | | | Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-0612-99/+23
| * | | | | | Fixing get_loop_info : part 2Cyril SIX2020-12-081-8/+28
| * | | | | | Fixing loop detection in get_loop_info - part 1Cyril SIX2020-12-081-16/+8
| * | | | | | Moving codeCyril SIX2020-12-081-71/+72
| * | | | | | More debugCyril SIX2020-12-081-6/+21
| * | | | | | More debugCyril SIX2020-12-081-3/+3
| * | | | | | Do not duplicate nodes that don't need to when unrolling the bodyCyril SIX2020-12-081-4/+18
| * | | | | | Fix on find_last_node_before_loopCyril SIX2020-12-081-3/+7
| |/ / / / /
generated by cgit (git 2.34.1) at 2024-06-02 12:52:03 +0000