aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* return_address_exists -> doneSylvain Boulmé2018-09-201-7/+79
* return_address suiteSylvain Boulmé2018-09-191-6/+6
* proof sketch for Asmgenproof.return_address_exists ?Sylvain Boulmé2018-09-191-3/+17
* premier jet Asmblockgenproof.return_address_offsetSylvain Boulmé2018-09-181-7/+0
* une solution pour le rao -> on fait remonter dans AsmblockgenproofSylvain Boulmé2018-09-061-5/+5
* Rajout d'un return_address_offset. Besoin de changer forward_simu de mach mac...Cyril SIX2018-09-061-2/+22
* resoud pb du TransfLinkSylvain Boulmé2018-09-061-0/+2
* Remplacement de match_prog par un plus classiqueCyril SIX2018-09-061-14/+9
* Asmblock -> Asm presque fini.. erreur sur driver/Compiler.vCyril SIX2018-09-061-1071/+31
* MPPA - refactored instructionsCyril SIX2018-05-111-5/+5
* MPPA - Added ops for comparison operatorsCyril SIX2018-04-241-52/+12
* MPPA - added remaining ops ; mult, div and floating point ops missingCyril SIX2018-04-201-0/+6
* MPPA - Oshrximm + Mgetparam + FP is GPR10 + bugCyril SIX2018-04-201-15/+17
* MPPA - added Oaddrsymbol -> now able to run the matrix mult testCyril SIX2018-04-181-0/+2
* MPPA - added Oaddrstack - problem in TargetPrinter.ml Pbuiltin EF_annotCyril SIX2018-04-171-3/+3
* MPPA - Added optim for long unsigned cmp to 0.Cyril SIX2018-04-131-1/+6
* MPPA - Ocast32signedCyril SIX2018-04-111-0/+7
* MPPA - OnegfCyril SIX2018-04-111-2/+4
* MPPA - Added MloadCyril SIX2018-04-101-2/+5
* MPPA - bunch of ops added : lowlong, and, or, shr..Cyril SIX2018-04-101-0/+6
* MPPA - optimized branch generation for signed long compare to 0Cyril SIX2018-04-091-1/+2
* MPPA - Optimized branch generation for word compare to 0Cyril SIX2018-04-091-2/+8
* MPPA - Long comparisonsCyril SIX2018-04-041-0/+8
* MPPA - Added non immediate comparisonCyril SIX2018-04-041-1/+5
* MPPA - Added signed immediate comparisonCyril SIX2018-04-041-0/+3
* MPPA - 32-bits immediate eq/neq branchesCyril SIX2018-04-041-9/+9
* MPPA - Added Mgoto + Pj_lCyril SIX2018-04-041-2/+0
* MPPA - mppa_call branch cleaningCyril SIX2018-04-041-7/+3
* MPPA - Added Msetstack + bunch of store --> on a des call !Cyril SIX2018-04-041-5/+8
* MPPA - Reactivated OmoveCyril SIX2018-04-041-0/+4
* MPPA - Added Mcall + Pgoto + modified PcallCyril SIX2018-04-041-3/+9
* MPPA - Added Mgetstack, loadind, a bunch of loadsCyril SIX2018-04-041-6/+6
* MPPA - Activated Mtailcall + PcallCyril SIX2018-04-041-2/+4
* MPPA - Activated Paddw and Paddiw + opsCyril SIX2018-04-041-3/+4
* MPPA - code cleaningCyril SIX2018-04-041-7/+9
* MPPA - Created Pmakel instruction + re-activated Oloadimm64/32Cyril SIX2018-04-041-6/+4
* MPPA - Removed Plui, replaced with Pmake, and modified make_immed64Cyril SIX2018-04-041-2/+3
* MPPA - ABI proof complete (Asmgenproof.v:step_simulation)Cyril SIX2018-04-041-40/+92
* Hook for MPPA_K1c (generates Risc-V code for now)Cyril SIX2018-04-041-0/+1028
generated by cgit (git 2.34.1) at 2024-07-06 18:10:17 +0000