aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
...
| * one step toward "bundle_step"Sylvain Boulmé2018-09-241-6/+55
| * relectureSylvain Boulmé2018-09-241-12/+1
| * MB2AB - changement du lock-step en star, cas du Returnstate faitCyril SIX2018-09-211-10/+27
| * MB2AB - Trois premières parties du lock-stepCyril SIX2018-09-212-17/+322
| * return_address_exists -> doneSylvain Boulmé2018-09-203-25/+92
| * avancement return_addressSylvain Boulmé2018-09-201-45/+64
| * return_address suiteSylvain Boulmé2018-09-194-17/+137
| * proof sketch for Asmgenproof.return_address_exists ?Sylvain Boulmé2018-09-192-3/+21
| * premier jet Asmblockgenproof.return_address_offsetSylvain Boulmé2018-09-183-9/+97
| * Rebase avec le commit qui fixe les tests + librairiesCyril SIX2018-09-063-7/+15
| * Asmblock & cie - ça compileCyril SIX2018-09-064-112/+101
| * Extraction issueCyril SIX2018-09-063-3/+18
| * 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-065-19/+50
| * 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
* | Added all the working builtins for ALU. Added BCU and LSU without testingCyril SIX2018-08-014-14/+372
|/
* 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
generated by cgit (git 2.34.1) at 2024-07-12 07:29:50 +0000