aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * mergedDavid Monniaux2019-05-041-4/+3
| * Merge branch 'mppa-peephole' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...David Monniaux2019-05-041-5/+2
| |\
| | * legere simplification de preuveSylvain Boulmé2019-05-041-70/+26
| | * Merge branch 'mppa-work' into mppa-peepholeSylvain Boulmé2019-05-0429-326/+477
| | |\
| * | | store oDavid Monniaux2019-05-043-17/+22
| * | | store octupleDavid Monniaux2019-05-041-1/+38
| * | | it compiles!David Monniaux2019-05-044-7/+87
| * | | big proofs for so / loDavid Monniaux2019-05-044-6/+306
| * | | Merge remote-tracking branch 'origin/mppa-work' into mppa-peepholeDavid Monniaux2019-05-0329-326/+477
| |\ \ \ | | |/ / | |/| / | | |/
* | | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-05-0427-316/+461
|\ \ \ | | |/ | |/|
| * | [#120] - Makefile generator + replaced binary_search/Makefile : it worksCyril SIX2019-05-034-30/+81
| * | Merge branch 'mppa-work' into mppa_k1cCyril SIX2019-05-0342-379/+1684
| |\ \
| * | | Changes to include a -O1 -fschedule-insns2 gcc run as wellCyril SIX2019-04-2624-290/+384
* | | | Merge remote-tracking branch 'origin/mppa-peephole' into mppa-workDavid Monniaux2019-05-039-30/+148
|\ \ \ \ | |_|/ / |/| | / | | |/ | |/|
| * | Lq finished ?David Monniaux2019-05-033-18/+31
| * | begin add PlqDavid Monniaux2019-05-038-12/+117
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-peepholeDavid Monniaux2019-05-035-11/+8
| |\ \
* | | | Fixing Coq dependenciesCyril SIX2019-05-031-1/+1
* | | | [FIX #101] PostpassSchedulingOracle:separate_opaque was not computing correctlyCyril SIX2019-05-031-9/+15
* | | | Merge remote-tracking branch 'origin/mppa-peephole' into mppa-workDavid Monniaux2019-05-0316-21/+308
|\| | | | |/ / |/| |
| * | -fcoalesce-memDavid Monniaux2019-05-035-7/+19
| * | use sq to save pairs of registersDavid Monniaux2019-05-035-11/+27
| * | it compilesDavid Monniaux2019-05-035-5/+65
| * | ça avanceDavid Monniaux2019-05-031-0/+27
| * | rm OfslowDavid Monniaux2019-05-031-1/+1
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-peepholeDavid Monniaux2019-05-0310-93/+61
| |\ \
| * | | getting stuck need to move offsetsDavid Monniaux2019-05-034-10/+40
| * | | find consecutive writesDavid Monniaux2019-05-022-6/+83
| * | | detect consecutive onesDavid Monniaux2019-05-021-2/+6
| * | | example of spill peepholeDavid Monniaux2019-05-021-0/+21
| * | | found peepholeDavid Monniaux2019-05-022-1/+24
| * | | seems to workDavid Monniaux2019-05-022-2/+19
* | | | Renaming "dumb" scheduling into "greedy"Cyril SIX2019-05-034-10/+5
* | | | Fixing mppa_k1c/Chunks.v for Coq 8.9Cyril SIX2019-05-031-1/+3
| |/ / |/| |
* | | rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)David Monniaux2019-05-0310-93/+61
|/ /
* | allow disabling + xx global symbolsDavid Monniaux2019-05-022-4/+9
* | Merge branch 'mppa-xsaddr' into mppa-workDavid Monniaux2019-05-0223-55/+419
|\ \
| * | fix slow globals etc.David Monniaux2019-05-022-2/+2
| * | command line options (still incomplete)David Monniaux2019-05-026-11/+46
| * | forgot Chunks.vDavid Monniaux2019-05-022-1/+21
| * | fix targetprinter bug for .xsDavid Monniaux2019-05-011-4/+4
| * | load xs / store xs seem to workDavid Monniaux2019-05-011-1/+2
| * | does not yet work, arity mismatchDavid Monniaux2019-05-016-15/+15
| * | it compilesDavid Monniaux2019-05-0110-33/+164
| * | ça avanceDavid Monniaux2019-05-012-12/+85
| * | pass one proofDavid Monniaux2019-05-011-7/+2
| * | advancing (but broken)David Monniaux2019-05-012-0/+5
| * | translate load.xsDavid Monniaux2019-05-014-7/+30
| * | indexed2XS beginDavid Monniaux2019-05-013-3/+10
| * | begin load.xsDavid Monniaux2019-05-018-11/+85
generated by cgit (git 2.34.1) at 2024-07-12 03:19:15 +0000