aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* 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-034-10/+7
|\
| * Renaming "dumb" scheduling into "greedy"Cyril SIX2019-05-033-9/+4
| * Fixing mppa_k1c/Chunks.v for Coq 8.9Cyril SIX2019-05-031-1/+3
* | -fcoalesce-memDavid Monniaux2019-05-031-7/+12
* | 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
|\|
| * rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)David 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
* | found peepholeDavid Monniaux2019-05-022-1/+24
* | seems to workDavid Monniaux2019-05-022-2/+19
|/
* allow disabling + xx global symbolsDavid Monniaux2019-05-022-4/+9
* Merge branch 'mppa-xsaddr' into mppa-workDavid Monniaux2019-05-0218-54/+396
|\
| * fix slow globals etc.David Monniaux2019-05-022-2/+2
| * command line options (still incomplete)David Monniaux2019-05-022-11/+24
| * forgot Chunks.vDavid Monniaux2019-05-021-0/+20
| * 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
* | Merge branch 'dumb-scheduling' into mppa-workCyril SIX2019-04-303-4/+71
|\ \ | |/ |/|
| * Setting fpostpass= optionCyril SIX2019-04-301-1/+1
| * The scheduler selection works, but the argument is not optional yet (-fpostpa...Cyril SIX2019-04-291-1/+7
| * [BROKEN] Fixed the dumb scheduler, not yet properly integratedCyril SIX2019-04-292-3/+6
| * [BUGGED] First attempt at a dumb scheduler ("accumulates" instructions)Cyril SIX2019-04-253-3/+61
* | rm unsupported int -> double signed/unsigned opsDavid Monniaux2019-04-294-17/+1
* | removed fake ops for int32 -> doubleDavid Monniaux2019-04-296-24/+0
* | float of int = float of long o long of intDavid Monniaux2019-04-292-4/+17
* | float of intu = float of longu o longu of intuDavid Monniaux2019-04-292-4/+18
* | srsdDavid Monniaux2019-04-292-16/+10
* | forgot in oracleDavid Monniaux2019-04-291-0/+2
* | begin using shrxDavid Monniaux2019-04-292-29/+10
* | Srsd / SrswDavid Monniaux2019-04-296-5/+55
* | insfl generationDavid Monniaux2019-04-292-0/+86
* | more insf detectionDavid Monniaux2019-04-282-0/+43
* | coq mode for emacsDavid Monniaux2019-04-281-0/+4
* | insf seems to workDavid Monniaux2019-04-281-1/+1
* | selection for insfDavid Monniaux2019-04-282-3/+21
generated by cgit (git 2.34.1) at 2024-07-04 13:53:55 +0000