aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* fix kvxv3.8+ssa_aarch64_postpassssaDavid Monniaux2021-01-101-4/+5
* Merge gitlab.inria.fr:compcertssa/compcertssa into kvx-work-ssaDavid Monniaux2021-01-100-0/+0
|\
| * Merge branch 'issue1' into 'ssa'Delphine Demange2020-11-0924-43/+11929
| |\
* | | one problem in this file (admitted)David Monniaux2021-01-102-3/+3
* | | fix for SSADavid Monniaux2021-01-101-3/+3
* | | fix for KVXDavid Monniaux2021-01-101-307/+19
* | | fix for PPCDavid Monniaux2021-01-091-3/+0
* | | fix mergeDavid Monniaux2021-01-081-6/+0
* | | fix for rv64David Monniaux2021-01-081-16/+16
* | | fix MakefileDavid Monniaux2021-01-081-1/+1
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-work-ssaDavid Monniaux2021-01-08317-7959/+31764
|\ \ \
| * | | 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
generated by cgit (git 2.34.1) at 2024-05-06 11:17:53 +0000