aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* Removed the bundle attemptCyril SIX2018-09-286-624/+9
* 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-254-15/+215
* 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-245-194/+335
* 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-184-10/+98
* Rebase avec le commit qui fixe les tests + librairiesCyril SIX2018-09-063-7/+15
* Asmblock & cie - ça compileCyril SIX2018-09-065-114/+102
* Extraction issueCyril SIX2018-09-065-11/+29
* 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-066-20/+51
* 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-069-3392/+754
* 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-064-20/+1146
* Asmblockgen.v finished (no proof yet)Cyril SIX2018-09-063-128/+200
* Changements mineurs Asmblock.v + draft de Asmblockgen.v à compléterCyril SIX2018-09-063-12/+900
* 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-063-236/+159
* Machblock: adaptation to the generalized ForwardSimulationBlockSylvain Boulmé2018-09-064-352/+395
* Generalization of ForwardSimulationBlockSylvain Boulmé2018-09-061-33/+24
* Machblock: some cleaningCyril SIX2018-09-064-203/+146
* Machblock: Mach language with basic blocksCyril SIX2018-09-066-1/+1986
* Fixed CompCert library inclusion. Indirect fix for udivd and umoddCyril SIX2018-06-262-3/+4
* MPPA - Forgot to initialize variables in the testsCyril SIX2018-06-062-2/+3
* WIP - Changed all the general tests to include PRNG (instead of small constants)Cyril SIX2018-06-0559-308/+394
* MPPA - Changed division to include the builtinCyril SIX2018-06-051-23/+2
generated by cgit (git 2.34.1) at 2024-07-12 08:25:03 +0000