aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'kvx-work' into mppa-RTLpathSECyril SIX2020-05-28511-3071/+13850
|\ | | | | | | | | Adapting the new mppa-RTLpathSE passes into the new Compiler.vexpand framework
| * fix markdownSylvain Boulmé2020-05-281-1/+3
| |
| * automatic date in the html indexSylvain Boulmé2020-05-283-4/+13
| |
| * source url in the docSylvain Boulmé2020-05-272-2/+7
| |
| * fix pages ?Sylvain Boulmé2020-05-271-1/+2
| |
| * add coq2html for pagesSylvain Boulmé2020-05-272-0/+7
| |
| * gitlab-ci.yml: inherit keyword does not work ?Sylvain Boulmé2020-05-271-2/+12
| |
| * pages: make documentationSylvain Boulmé2020-05-271-1/+5
| |
| * fix pages ?Sylvain Boulmé2020-05-271-0/+1
| |
| * basic pages configurationSylvain Boulmé2020-05-271-0/+9
| |
| * Merge remote-tracking branch 'certicompil/master' into kvx-workSylvain Boulmé2020-05-272-0/+26
| |\
| | * readmeDavid Monniaux2020-05-272-2/+17
| | |
| | * opam updateDavid Monniaux2020-05-271-0/+11
| | |
| * | link to the HAL preprintSylvain Boulmé2020-05-271-2/+6
| | |
| * | replace k1 -> kvxSylvain Boulmé2020-05-272-3/+3
| |/
| * install extra packagesDavid Monniaux2020-05-271-2/+2
| |
| * download/untar from KalrayDavid Monniaux2020-05-272-2/+3
| |
| * strict key checking offDavid Monniaux2020-05-271-1/+1
| |
| * CI for KVXDavid Monniaux2020-05-272-2/+17
| |
| * tests for kvxDavid Monniaux2020-05-26160-0/+0
| |
| * k1c -> kvx changesDavid Monniaux2020-05-26203-1057/+1057
| |
| * backport to coq 8.10.2Sylvain Boulmé2020-05-112-4/+9
| |
| * fix index-mppa_k1c.htmlSylvain Boulmé2020-05-111-1/+1
| |
| * updating the html index for mppa-k1cSylvain Boulmé2020-05-101-45/+27
| | | | | | | | NOTE: This file has been copied from the one of pldi-artefact branch.
| * -fcse3-glbDavid Monniaux2020-05-066-14/+36
| |
| * CSE3 across mergesDavid Monniaux2020-05-065-11/+33
| |
| * make Aarch64 muladd depend on the optionDavid Monniaux2020-05-062-4/+10
| |
| * README KalrayCyril SIX2020-05-041-0/+32
| |
| * Adding copyrightsCyril SIX2020-05-04108-460/+1392
| |
| * Update on testsuite and INSTALL.mdCyril SIX2020-05-043-9/+16
| |
| * add a renumber phaseDavid Monniaux2020-04-301-0/+1
| |
| * run a separate CSE3 for LICMDavid Monniaux2020-04-241-1/+3
| |
| * Merge branch 'mppa-work' of ↵David Monniaux2020-04-23139-589/+9973
| |\ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| | * Merge remote-tracking branch 'origin/mppa-features' into mppa-workDavid Monniaux2020-04-23139-589/+9973
| | |\
| | | * sync with licmDavid Monniaux2020-04-231-1/+1
| | | |
| | | * Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-237-35/+119
| | | |\
| | | | * CSE3 across callsDavid Monniaux2020-04-236-13/+44
| | | | |
| | | | * Merge remote-tracking branch 'origin/mppa-cse3' into mppa-licmDavid Monniaux2020-04-235-21/+75
| | | | |\
| | | | | * make tracing output optionalDavid Monniaux2020-04-233-6/+11
| | | | | |
| | | | | * fix in CSE3 move propagationDavid Monniaux2020-04-234-42/+82
| | | | | |
| | | | | * CSE3analysisaux: pp_rhsDavid Monniaux2020-04-231-0/+9
| | | | | |
| | | | * | use cbn not simplDavid Monniaux2020-04-221-21/+21
| | | | | |
| | | * | | cbn and copyrightDavid Monniaux2020-04-222-9/+19
| | | | | |
| | | * | | use cbn in T instead of simpl in TDavid Monniaux2020-04-222-2/+3
| | | | | |
| | | * | | automated writing Compiler.vDavid Monniaux2020-04-226-122/+90
| | | | | |
| | | * | | generate mkpassDavid Monniaux2020-04-212-19/+14
| | | | | |
| | | * | | Require autogenDavid Monniaux2020-04-212-42/+26
| | | | | |
| | | * | | begin scripting the Compiler.v fileDavid Monniaux2020-04-215-39/+71
| | | | | |
| | | * | | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-2115-165/+444
| | | |\| |
| | | | * | exampleDavid Monniaux2020-04-211-0/+6
| | | | | |
generated by cgit (git 2.34.1) at 2024-07-07 08:00:30 +0000