aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/mppa-work' into mppa-cosDavid Monniaux2019-05-291-2/+2
|\
| * error in the classification of SrswDavid Monniaux2019-05-291-2/+2
* | to be able to use DDR we need 8-byte pointers in jump tablesDavid Monniaux2019-05-291-5/+5
|/
* move Asmblockgenproof0 from lib to mppa_k1c/Sylvain Boulmé2019-05-211-0/+0
* move Machblock*.v into mppa_k1c/libSylvain Boulmé2019-05-213-0/+0
* 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
* | Desactivating the "one instruction per bundle" failsafeCyril SIX2019-05-171-0/+3
* | Merge branch 'mppa_k1c' into mppa-abstractbb-devCyril SIX2019-05-171-0/+2
|\ \
| * | directly call float and double division from gcc lib instead of a stubDavid Monniaux2019-05-151-0/+2
* | | improving the scheduling verifier and its frameworkSylvain Boulmé2019-05-162-36/+149
* | | Merge branch 'mppa-work' into mppa-abstractbb-devSylvain Boulmé2019-05-161-1/+103
|\| |
| * | detailDavid Monniaux2019-05-151-1/+1
| * | more lemmas on divisionDavid Monniaux2019-05-151-0/+48
| * | more lemmas on divisionDavid Monniaux2019-05-151-1/+55
* | | abstractbb: support of removing useless computationsSylvain Boulmé2019-05-147-299/+481
|/ /
* | some lemmas on division etc.David Monniaux2019-05-141-0/+258
* | 32-bit modulo now uses sign extend then call to the 64-bit functionDavid Monniaux2019-05-133-3/+59
* | we directly call 64-bit unsigned divisionDavid Monniaux2019-05-133-4/+24
* | begin proving that we can use 64-bit division for doing 32David Monniaux2019-05-131-0/+64
* | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-05-123-64/+72
|\ \
| * | Asmblockgen prologue is now 1 basicblock (instead of 3)Cyril SIX2019-05-103-64/+72
* | | directly branch to certain division functions from gccDavid Monniaux2019-05-121-3/+16
|/ /
generated by cgit (git 2.34.1) at 2024-07-04 01:40:11 +0000