aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2019-05-217-949/+712
|\
| * 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
| |\
| | * 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
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2019-05-2025-23/+136
|\| |
| * | 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 remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2019-05-177-298/+593
|\| |
| * | Merge branch 'mppa_k1c' into mppa-abstractbb-devCyril SIX2019-05-1743-64/+614
| |\ \
| * | | improving the scheduling verifier and its frameworkSylvain Boulmé2019-05-162-36/+149
| * | | Merge branch 'mppa-work' into mppa-abstractbb-devSylvain Boulmé2019-05-1648-436/+1458
| |\ \ \
| * | | | abstractbb: support of removing useless computationsSylvain Boulmé2019-05-147-299/+481
* | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2019-05-161-5/+18
|\ \ \ \ \ | | |_|/ / | |/| | |
| * | | | simpler code, works in 32 bitsDavid Monniaux2019-05-161-5/+18
* | | | | sdiv, smod, udiv, umod through fast routinesDavid Monniaux2019-05-161-1/+32
* | | | | umodDavid Monniaux2019-05-161-1/+33
* | | | | udivDavid Monniaux2019-05-161-1/+28
* | | | | simplify sdivDavid Monniaux2019-05-161-5/+0
* | | | | simplify sdiv codeDavid Monniaux2019-05-161-4/+1
* | | | | simplify sdiv codeDavid Monniaux2019-05-161-8/+0
generated by cgit (git 2.34.1) at 2024-07-14 04:44:53 +0000