aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* reset PATHv3.8_aarch64_postpassDavid Monniaux2021-01-081-1/+1
* remove some useless "OK tt"Sylvain Boulmé2021-01-072-11/+11
* update index-kvx.htmlSylvain Boulmé2021-01-071-8/+8
* Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2021-01-0713-267/+280
|\
| * Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2021-01-0710-262/+256
| |\
| | * Removing Yarpgen test 89Cyril SIX2021-01-071-0/+14
| | * Making verify_mapping_mn_rec tail recursive (should fix arm CI) #231Cyril SIX2021-01-062-3/+2
| | * Solving a stack overflow issue (was failing in yarpgen ran000089 for armhf)Cyril SIX2021-01-061-9/+9
| | * Merge remote-tracking branch 'origin/kvx-work' into kvx-work-dirtyCyril SIX2020-12-179-79/+149
| | |\
| | * | Uniformizing a couple of debug print functionsCyril SIX2020-12-175-167/+148
| | * | Fixing too many loads being NOTRAPCyril SIX2020-12-171-3/+9
| | * | Flushing at each dprintfCyril SIX2020-12-161-1/+3
| | * | Partially fixing turning loads into non trapCyril SIX2020-12-161-22/+56
| | * | CleanupCyril SIX2020-12-161-83/+0
| | * | Turning loads into non-trapping when necessaryCyril SIX2020-12-153-2/+43
| * | | -fcse3-trivial-opsDavid Monniaux2021-01-072-3/+4
| | |/ | |/|
| * | add profiling entry-points in the htmldoc.Sylvain Boulmé2020-12-171-2/+20
| * | Merge branch 'master' of gricad-gitlab.univ-grenoble-alpes.fr:certicompil/com...Sylvain Boulmé2020-12-160-0/+0
| |\ \
| | * | fix installation problemsDavid Monniaux2020-12-111-1/+1
* | | | update kvxSylvain Boulmé2021-01-074-98/+45
* | | | 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
generated by cgit (git 2.34.1) at 2024-05-19 03:52:52 +0000