aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Select condition x < 0 with x unsigned leads to falsev3.9_kvx_fix1David Monniaux2021-09-173-14/+141
* test for many parametersDavid Monniaux2021-09-173-1/+2
* FIX CODEGEN BUG PallocframeDavid Monniaux2021-09-171-1/+1
* many parametersDavid Monniaux2021-09-171-0/+313
* reachableDavid Monniaux2021-09-161-1/+1
* bump OCaml version in CIDavid Monniaux2021-09-151-13/+13
* Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2021-09-152-4/+4
|\
| * fix bug from issue 239Léo Gourdin2021-09-151-0/+2
| * test opweights remLéo Gourdin2021-09-151-4/+2
* | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...David Monniaux2021-09-131-2/+2
|\|
| * Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...Léo Gourdin2021-09-131-2/+2
| |\
| * | update weights FU74...Léo Gourdin2021-09-131-2/+2
* | | coqchk -oDavid Monniaux2021-09-111-1/+1
| |/ |/|
* | rocket is default choiceDavid Monniaux2021-09-101-1/+1
* | option compatible avec gccDavid Monniaux2021-09-101-1/+1
|/
* new weights for FU74Léo Gourdin2021-09-101-1/+140
* test under coq 8.13.2David Monniaux2021-09-021-0/+23
* fix compil for coq 8.13.2Léo Gourdin2021-09-021-2/+1
* 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
generated by cgit (git 2.34.1) at 2024-05-19 07:32:09 +0000