aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
...
| * Preuve du internal_function (step_simulation)Cyril SIX2018-09-283-36/+90
| * storeind_ptr_correct un peu d'avancéeCyril SIX2018-09-273-22/+33
| * Avancement dans exec_straight_throughCyril SIX2018-09-271-9/+51
| * Enlèvement du "no_builtin" condition; exec_control sur les option control; e...Cyril SIX2018-09-264-55/+120
| * AB: removing bregsCyril SIX2018-09-265-97/+73
| * MB2AB - Adding Asmblockgenproof1.vCyril SIX2018-09-261-0/+1595
| * MB2AB - un peu d'avancement sur internal functionCyril SIX2018-09-253-14/+214
| * MB2AB - Proof of external function stepCyril SIX2018-09-253-13/+85
| * add an example on depfreeSylvain Boulmé2018-09-251-1/+19
| * relectureSylvain Boulmé2018-09-242-27/+148
| * Some definitions in AsmbundleCyril SIX2018-09-241-0/+98
| * a few stubs for bundlingSylvain Boulmé2018-09-244-194/+334
| * 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
generated by cgit (git 2.34.1) at 2024-07-06 16:23:39 +0000