aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
* 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
| |\ | | | | | | | | | | | | Conflicts: mppa_k1c/ExtValues.v
| | * 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
|/ / /
* | | move Asmblockgenproof0 from lib to mppa_k1c/Sylvain Boulmé2019-05-211-0/+0
| | | | | | | | | | | | This file is specific to our backend.
* | | move Machblock*.v into mppa_k1c/libSylvain Boulmé2019-05-213-0/+0
| | | | | | | | | | | | Indeed, these files may not be specific to our backend.
* | | 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
|\ \ \ | | | | | | | | | | | | | | | | Conflicts: mppa_k1c/lib/Asmblockgenproof0.v
| * | | transf_program_correct prooftvdd2019-05-201-91/+7
| | | |
| * | | mSylvain Boulmé2019-05-201-4/+10
| | | |
| * | | is_trans_code_monotonic prooftvdd2019-05-171-56/+120
| | | |
| * | | step_simu_cfi_step ??tvdd2019-05-151-3/+32
| | | |
| * | | mtvdd2019-05-151-2/+16
| | | |
| * | | star_step_simu_body_step prooftvdd2019-05-131-26/+40
| | | |
| * | | petite simplif de preuveSylvain Boulmé2019-04-191-62/+26
| | | |
| * | | step_simu_header prooftvdd2019-04-181-9/+10
| | | |
generated by cgit (git 2.34.1) at 2024-07-06 17:50:44 +0000