aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* resoud pb du TransfLinkSylvain Boulmé2018-09-061-0/+2
* Remplacement de match_prog par un plus classiqueCyril SIX2018-09-063-42/+70
* Asmblock -> Asm presque fini.. erreur sur driver/Compiler.vCyril SIX2018-09-068-3391/+753
* Asmblockgen: Added Pnop and Program DefinitionsCyril SIX2018-09-062-56/+22
* Example of Program use...Sylvain Boulmé2018-09-061-0/+16
* Asmblock: Adding forward_simulation and determinism as axiomsCyril SIX2018-09-063-19/+1145
* Asmblockgen.v finished (no proof yet)Cyril SIX2018-09-062-127/+199
* Changements mineurs Asmblock.v + draft de Asmblockgen.v à compléterCyril SIX2018-09-062-12/+899
* deplacement allocframe/freeframe/loadsymbolSylvain Boulmé2018-09-061-41/+37
* Name changing + introducing Pbuiltin (alone in a block)Cyril SIX2018-09-061-91/+67
* Some renaming on asmblockCyril SIX2018-09-061-11/+11
* add comments (TODO/FIXME)Sylvain Boulmé2018-09-061-11/+28
* notation changeSylvain Boulmé2018-09-061-21/+21
* a version of Asmblock syntax and semanticsSylvain Boulmé2018-09-061-0/+1376
* Machblock: some renaming and proof simplificationsCyril SIX2018-09-062-221/+144
* Machblock: adaptation to the generalized ForwardSimulationBlockSylvain Boulmé2018-09-063-344/+292
* Machblock: some cleaningCyril SIX2018-09-063-196/+146
* Machblock: Mach language with basic blocksCyril SIX2018-09-063-0/+1741
* MPPA - Added Builtins support. Starting with clzll and stsudCyril SIX2018-06-052-61/+6
* WIP - Trying to add builtins support. They are not detected for now :(Cyril SIX2018-05-304-38/+34
* MPPA - Added modulo and division 64 bits. Non certifiedCyril SIX2018-05-215-30/+25
* MPPA - refactored instructionsCyril SIX2018-05-116-500/+549
* Code cleaningCyril SIX2018-05-093-153/+99
* MPPA - FIX GPR10 is now the Frame Pointer in Asmexpand.ml (instead of GPR32)Cyril SIX2018-04-261-3/+3
* MPPA - fixed some typos in the TargetPrinterCyril SIX2018-04-261-34/+5
* MPPA - Added coverage testCyril SIX2018-04-251-3/+3
* MPPA - Operands were inverted in SBFW and SBFD instructionsCyril SIX2018-04-241-2/+2
* MPPA - Added ops for comparison operatorsCyril SIX2018-04-245-262/+186
* MPPA - added remaining ops ; mult, div and floating point ops missingCyril SIX2018-04-204-15/+57
* MPPA - Added Ocast8signed and Ocast16signedCyril SIX2018-04-202-16/+16
* MPPA - Oshrximm + Mgetparam + FP is GPR10 + bugCyril SIX2018-04-206-42/+50
* MPPA - added Oaddrsymbol -> now able to run the matrix mult testCyril SIX2018-04-183-15/+17
* MPPA - Added Pmull -> now able to run the sort testCyril SIX2018-04-173-2/+7
* MPPA - added Oaddrstack - problem in TargetPrinter.ml Pbuiltin EF_annotCyril SIX2018-04-174-26/+23
* MPPA - More shiftsCyril SIX2018-04-173-4/+24
* MPPA - added all shiftsCyril SIX2018-04-173-3/+28
* MPPA - Added optim for long unsigned cmp to 0.Cyril SIX2018-04-135-23/+140
* Osub and OmulCyril SIX2018-04-113-2/+14
* MPPA - OshrCyril SIX2018-04-113-2/+7
* MPPA - Ocast32signedCyril SIX2018-04-116-8/+53
* MPPA - OnegfCyril SIX2018-04-115-14/+17
* MPPA - Added MloadCyril SIX2018-04-105-29/+57
* MPPA - bunch of ops added : lowlong, and, or, shr..Cyril SIX2018-04-105-21/+80
* MPPA - Oneg + PnegwCyril SIX2018-04-103-3/+8
* MPPA - Onegl + PneglCyril SIX2018-04-103-3/+8
* MPPA - optimized branch generation for signed long compare to 0Cyril SIX2018-04-095-23/+69
* MPPA - Optimized branch generation for word compare to 0Cyril SIX2018-04-095-30/+178
* MPPA - Desactivated Pbuiltin EF_annotCyril SIX2018-04-041-7/+6
* MPPA - Long comparisonsCyril SIX2018-04-045-30/+158
* MPPA - Added non immediate comparisonCyril SIX2018-04-043-5/+21
generated by cgit (git 2.34.1) at 2024-07-12 03:13:07 +0000