aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* adaptation pour k1c-cosDavid Monniaux2019-05-2812-354/+35
|
* move Asmblockgenproof0 from lib to mppa_k1c/Sylvain Boulmé2019-05-211-0/+0
| | | | This file is specific to our backend.
* move Machblock*.v into mppa_k1c/libSylvain Boulmé2019-05-213-0/+0
| | | | Indeed, these files may not be specific to our backend.
* Better graphsCyril SIX2019-05-211-37/+41
|
* Added type annotations to gengraphs.pyCyril SIX2019-05-211-7/+8
|
* Added types annotations to genmake.pyCyril SIX2019-05-211-8/+9
|
* legere simplification de preuveSylvain Boulmé2019-05-201-29/+7
|
* Merge remote-tracking branch 'machblock/mppa_k1c' into mppa-workCyril SIX2019-05-205-934/+717
|\ | | | | | | | | Conflicts: mppa_k1c/lib/Asmblockgenproof0.v
| * 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-072-8/+29
| |
| * extract Machgen.trans_code stuff from AsmgenproofSylvain Boulmé2019-04-073-99/+65
| |
| * 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
| |
| * Machblockgen proofstvdd2019-03-071-4/+15
| |
| * add_to_code_is_trans_code proof 2tvdd2019-03-051-14/+6
| |
| * mSylvain Boulmé2019-03-051-4/+9
| |
| * add_to_code_is_trans_code prooftvdd2019-03-051-4/+15
| |
| * squelette de preuve pour Machblockgenproof.vSylvain Boulmé2019-02-223-21/+228
| |
| * machblockgen.v recursion terminaletvdd2019-02-211-535/+47
| |
* | Premier jet de graphes de mesures (à améliorer)Cyril SIX2019-05-174-4/+97
| |
* | Measures to CSV doneCyril SIX2019-05-1711-4/+11
| |
* | Desactivating the "one instruction per bundle" failsafeCyril SIX2019-05-171-0/+3
| |
* | Adding more measuresCyril SIX2019-05-1712-16/+26
| |
* | Merge branch 'mppa_k1c' into mppa-abstractbb-devCyril SIX2019-05-1743-64/+614
|\ \
| * | simpler code, works in 32 bitsDavid Monniaux2019-05-161-5/+18
| | |
| * | directly call float and double division from gcc lib instead of a stubDavid Monniaux2019-05-152-42/+2
| | |
| * | remet les trucs dans les bons répertoiresDavid Monniaux2019-05-1524-0/+0
| | |
| * | truly inline function as macro to trigger better instruction selectionDavid Monniaux2019-05-151-1/+6
| | | | | | | | | | | | (replace x/2 by x*0.5)
| * | compiled with Lustre v4David Monniaux2019-05-154-0/+512
| | |
| * | Merge branch 'mppa-work' of ↵David Monniaux2019-05-157-6/+21
| |\ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| | * | Measures for bitslices-aes, bitsliced-tea and complex_matCyril SIX2019-05-157-6/+21
| | | |
| * | | renamingDavid Monniaux2019-05-1524-0/+0
| |/ /
| * | Merge branch 'mppa-work' of ↵David Monniaux2019-05-156-4/+47
| |\ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| | * | CSV file generation for benches (only binary_search for now)Cyril SIX2019-05-156-4/+47
| | | |
generated by cgit (git 2.34.1) at 2024-07-12 03:04:09 +0000