aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Machblockgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* move Machblock*.v into mppa_k1c/libSylvain Boulmé2019-05-211-806/+0
* legere simplification de preuveSylvain Boulmé2019-05-201-29/+7
* transf_program_correct prooftvdd2019-05-201-91/+7
* mSylvain Boulmé2019-05-201-4/+10
* is_trans_code_monotonic prooftvdd2019-05-171-56/+120
* step_simu_cfi_step ??tvdd2019-05-151-3/+32
* mtvdd2019-05-151-2/+16
* star_step_simu_body_step prooftvdd2019-05-131-26/+40
* petite simplif de preuveSylvain Boulmé2019-04-191-62/+26
* step_simu_header prooftvdd2019-04-181-9/+10
* trans_code_decompose prooftvdd2019-04-111-1/+86
* cleaner separation between Asmgenproof and MachblockgenproofSylvain Boulmé2019-04-071-1/+25
* extract Machgen.trans_code stuff from AsmgenproofSylvain Boulmé2019-04-071-5/+64
* relecture is_header, is_body, is_exit + pattern de preuve trans_code_decomposeSylvain Boulmé2019-04-041-16/+29
* is_header, is_body, is_exittvdd2019-04-041-4/+16
* dist_end_block_code_simu_mid_block prooftvdd2019-04-041-1/+12
* bien meilleure façon de s'inspirer de l'ancienne traductionSylvain Boulmé2019-04-031-71/+59
* adaptation de quelques vieux lemmes pour la nouvelle traductionSylvain Boulmé2019-04-031-61/+84
* introduce a small tactic.Sylvain Boulmé2019-04-031-4/+7
* legeres simplificationsSylvain Boulmé2019-04-021-239/+42
* find_label_transcode_preserved prooftvdd2019-03-281-4/+47
* un coup de pouceSylvain Boulmé2019-03-231-29/+28
* ctvdd2019-03-211-3/+73
* squelette de preuve pour Machblockgenproof.vSylvain Boulmé2019-02-221-11/+69
* Rajout d'un return_address_offset. Besoin de changer forward_simu de mach mac...Cyril SIX2018-09-061-10/+10
* Remplacement de match_prog par un plus classiqueCyril SIX2018-09-061-2/+2
* Asmblock -> Asm presque fini.. erreur sur driver/Compiler.vCyril SIX2018-09-061-4/+4
* Machblock: some renaming and proof simplificationsCyril SIX2018-09-061-36/+35
* Machblock: adaptation to the generalized ForwardSimulationBlockSylvain Boulmé2018-09-061-215/+201
* Machblock: some cleaningCyril SIX2018-09-061-22/+28
* Machblock: Mach language with basic blocksCyril SIX2018-09-061-0/+638
generated by cgit (git 2.34.1) at 2024-07-04 11:57:18 +0000