aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
...
* 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
* 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
generated by cgit (git 2.34.1) at 2024-07-06 17:24:09 +0000