aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | | 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
| * | | | compiled with Lustre v4David Monniaux2019-05-154-0/+512
| * | | | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-05-157-6/+21
| |\ \ \ \
| | * | | | 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 gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-05-156-4/+47
| |\ \ \ \
| | * | | | CSV file generation for benches (only binary_search for now)Cyril SIX2019-05-156-4/+47
| * | | | | attempt at inlining; not many cycles removedDavid Monniaux2019-05-151-9/+11
| |/ / / /
* | | | | 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
|\| | | |
| * | | | Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-05-155-33/+120
| |\ \ \ \
| | * \ \ \ Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2019-05-154-32/+17
| | |\ \ \ \
| | | * | | | Added back bitslices-aesCyril SIX2019-05-154-32/+17
| | * | | | | detailDavid Monniaux2019-05-151-1/+1
| | * | | | | more lemmas on divisionDavid Monniaux2019-05-151-0/+48
| | * | | | | more lemmas on divisionDavid Monniaux2019-05-151-1/+55
| | |/ / / /
| * | | | | Heater example from Lustre v4David Monniaux2019-05-152-4/+18
| * | | | | Lustre v4 exampleDavid Monniaux2019-05-158-1/+568
| * | | | | example from Lustre v4 compiled with ONERA's lustrec compilerDavid Monniaux2019-05-155-0/+679
| |/ / / /
| * | | | Avancement sur la génération de Makefile des benchmarksCyril SIX2019-05-1434-409/+84
* | | | | abstractbb: support of removing useless computationsSylvain Boulmé2019-05-147-299/+481
|/ / / /
generated by cgit (git 2.34.1) at 2024-06-13 11:47:05 +0000