aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2021-09-0171-12690/+11725
|\
| * cleanupLéo Gourdin2021-09-0121-10547/+1
| * fix stub for no-prepass archs...Léo Gourdin2021-09-011-2/+3
| * Merge remote-tracking branch 'origin/kvx-work' into kvx-workLéo Gourdin2021-09-016-95/+36
| |\
| * \ [MERGE] BTL into kvx-work (replacing RTLpath)Léo Gourdin2021-09-0155-2160/+11740
| |\ \
| | * | CI fix on armLéo Gourdin2021-08-021-2/+2
| | * | non-trapping loads fixLeo Gourdin2021-08-021-3/+11
| | * | ci fix?Léo Gourdin2021-07-283-25/+17
| | * | CI test activate non-trap on kvx-cosLéo Gourdin2021-07-281-1/+1
| | * | remove todos, cleanLéo Gourdin2021-07-2812-185/+91
| | * | test ci2Léo Gourdin2021-07-271-3/+3
| | * | Merge branch 'BTL-SEimpl' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompC...Léo Gourdin2021-07-271-12/+14
| | |\ \
| | | * \ Merge branch 'BTL-SEimpl' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompC...Léo Gourdin2021-07-279-64/+103
| | | |\ \
| | | * | | prepass actLéo Gourdin2021-07-271-12/+14
| | * | | | test non-trapping loads using CI...Léo Gourdin2021-07-271-2/+93
| | | |/ / | | |/| |
| | * | | non trapping loadsLéo Gourdin2021-07-239-64/+103
| | |/ /
| | * | nothing admitted !!Léo Gourdin2021-07-222-17/+25
| | * | branches expansions supportLéo Gourdin2021-07-224-29/+404
| | * | Merge branch 'BTL-SEimpl' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompC...Léo Gourdin2021-07-222-16/+14
| | |\ \
| | | * | fix ciLéo Gourdin2021-07-212-16/+14
| | * | | renamingLéo Gourdin2021-07-221-51/+51
| | |/ /
| | * | new expansionsLéo Gourdin2021-07-212-15/+935
| | * | expansions btl proofsLéo Gourdin2021-07-215-9/+1008
| | * | bug fix in oracleLéo Gourdin2021-07-201-33/+360
| | * | new expansion oracle for BTLLéo Gourdin2021-07-204-6/+336
| | * | fix depsLéo Gourdin2021-07-201-1/+2
| | * | Fix compile on ARM/x86 backendsLéo Gourdin2021-07-208-1714/+181
| | * | op simplify BTL introLéo Gourdin2021-07-208-10/+56
| | * | proof for symbolic simu, need to finish equiv_inputsLéo Gourdin2021-07-203-23/+31
| | * | Finish implem proof, need to adapt scheduler proofLéo Gourdin2021-07-194-114/+373
| | * | hrexec_correct1Léo Gourdin2021-07-081-25/+48
| | * | some progress in canonbuildingLéo Gourdin2021-07-071-14/+106
| | * | symbolic_simu impl definitionsLéo Gourdin2021-07-071-47/+9
| | * | hrexec1Léo Gourdin2021-07-071-27/+81
| | * | progress in simulation testLéo Gourdin2021-07-071-57/+250
| | * | Some advance, need to finish canonbuilding proofsLéo Gourdin2021-07-061-13/+270
| | * | lemma on HC_set_regLéo Gourdin2021-07-052-52/+165
| | * | red_PTree lemmasLéo Gourdin2021-07-012-10/+77
| | * | cbranch expanseLéo Gourdin2021-06-301-0/+25
| | * | coercions and simplifyLéo Gourdin2021-06-302-3/+91
| | * | some advanceLéo Gourdin2021-06-301-14/+154
| | * | Starting symbolic execution implementationLéo Gourdin2021-06-301-0/+314
| | * | BTLroadmap: combinaison liveness et invariants ?Sylvain Boulmé2021-06-251-9/+47
| | * | update BTLroadmapSylvain Boulmé2021-06-241-5/+6
| | * | transf fct correct in BTL scheduler proofLéo Gourdin2021-06-201-5/+5
| | * | finish main proofLéo Gourdin2021-06-191-18/+128
| | * | lemma on eqregs?Léo Gourdin2021-06-182-14/+7
| | * | finish RTLtoBTL proofLéo Gourdin2021-06-181-2/+18
| | * | End of main scheduling proofLéo Gourdin2021-06-183-59/+90
| | * | some advance, new section to simplify context from symbolic execLéo Gourdin2021-06-173-66/+151
generated by cgit (git 2.34.1) at 2024-06-28 01:33:58 +0000