aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* Removing the Admitted warning when running "make check-admitted"Cyril SIX2019-06-121-1/+1
* abstract_bb: few improvements while writing the paperSylvain Boulmé2019-06-086-251/+294
* Merge branch 'mppa-work' into mppa-abstractbb-devSylvain Boulmé2019-06-0818-1065/+1539
|\
| * Fix for #134 Pjumptable not recognizedCyril SIX2019-06-051-1/+1
| * fixed reservation table for cmoveDavid Monniaux2019-06-051-1/+5
| * move with immediatesDavid Monniaux2019-06-042-1/+31
| * osel immDavid Monniaux2019-06-048-23/+117
| * begin osel immDavid Monniaux2019-06-043-3/+57
| * added immediate cmoveDavid Monniaux2019-06-046-38/+80
| * shortcuts for cmoveDavid Monniaux2019-06-042-20/+40
| * shortcut cmove worksDavid Monniaux2019-06-042-89/+7
| * why doesn't it work?David Monniaux2019-06-042-7/+265
| * little restructuringDavid Monniaux2019-06-041-3/+4
| * start to have whole path if-conversion?David Monniaux2019-06-042-2/+17
| * Osel -> assembleurDavid Monniaux2019-06-043-104/+112
| * Osel is output = 1st inputDavid Monniaux2019-06-041-0/+1
| * Osel operation (not yet compiled)David Monniaux2019-06-043-31/+39
| * rm old select/selectl/selectf/selectfsDavid Monniaux2019-06-0312-850/+44
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-cosDavid Monniaux2019-05-3016-44/+871
| |\
| | * Merge remote-tracking branch 'origin/mppa-msub' into mppa-workDavid Monniaux2019-05-3016-44/+871
| | |\
| | | * standardization of expressionsDavid Monniaux2019-05-122-10/+8
| | | * standardize semantics, 1David Monniaux2019-05-122-7/+12
| | | * Merge remote-tracking branch 'origin/mppa-work' into mppa-msubDavid Monniaux2019-05-124-67/+88
| | | |\
| | | * | correct -faddx option and propagate addim over addximDavid Monniaux2019-05-114-10/+21
| | | * | option -faddx (off by default until questions cleared)David Monniaux2019-05-114-20/+81
| | | * | apply .xs onto addx4 etcDavid Monniaux2019-05-1110-27/+180
| | | * | more maddxDavid Monniaux2019-05-112-0/+74
| | | * | maddx ordre opposéDavid Monniaux2019-05-112-0/+6
| | | * | add with shift, beginningDavid Monniaux2019-05-117-13/+86
| | | * | generate multiply-sub longDavid Monniaux2019-05-113-4/+56
| | | * | Pmsub compiledDavid Monniaux2019-05-119-40/+48
| | | * | more gen O -> PDavid Monniaux2019-05-111-0/+9
| | | * | more gen O -> PDavid Monniaux2019-05-111-0/+6
| | | * | Oaddx -> PDavid Monniaux2019-05-115-21/+48
| | | * | begin generating Prevsub etc. from Oxxx to PxxxDavid Monniaux2019-05-117-43/+46
| | | * | use shift 1-4 in backendDavid Monniaux2019-05-105-97/+62
| | | * | more integer OpDavid Monniaux2019-05-104-17/+245
| | | * | new instructions at asm levelDavid Monniaux2019-05-105-9/+157
| * | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cosDavid Monniaux2019-05-291-2/+2
| |\| | |
| | * | | error in the classification of SrswDavid Monniaux2019-05-291-2/+2
| * | | | to be able to use DDR we need 8-byte pointers in jump tablesDavid Monniaux2019-05-291-5/+5
| |/ / /
* | | | minor change in auxiliary lemmaSylvain Boulmé2019-05-281-11/+21
* | | | simpler definition of reduceSylvain Boulmé2019-05-283-48/+133
* | | | slightly more efficient versionSylvain Boulmé2019-05-263-40/+85
* | | | extending bblock_simu_test with rewritingSylvain Boulmé2019-05-2613-1531/+1825
|/ / /
* | | move Asmblockgenproof0 from lib to mppa_k1c/Sylvain Boulmé2019-05-211-0/+0
* | | move Machblock*.v into mppa_k1c/libSylvain Boulmé2019-05-213-0/+0
* | | legere simplification de preuveSylvain Boulmé2019-05-201-29/+7
* | | Merge remote-tracking branch 'machblock/mppa_k1c' into mppa-workCyril SIX2019-05-205-934/+717
|\ \ \
| * | | transf_program_correct prooftvdd2019-05-201-91/+7
generated by cgit (git 2.34.1) at 2024-06-12 07:34:03 +0000