aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | 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 ↵David Monniaux2019-05-123-64/+72
|\ \ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | | 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
|/ /
* | Exploiting immediate comparisonsCyril SIX2019-05-092-36/+145
| |
* | Replacing tabs by spaces in TargetPrinterCyril SIX2019-05-091-20/+20
| |
* | smart memcpy for arbitrary sizesDavid Monniaux2019-05-092-12/+30
| |
* | copy 16 by 16David Monniaux2019-05-092-14/+15
| |
* | slightly improved memcpyDavid Monniaux2019-05-091-12/+23
| |
* | structure copy through 4 byte registers instead of 1David Monniaux2019-05-091-24/+47
| |
* | simplification d'un code moche pour les variables thread-localDavid Monniaux2019-05-081-1/+1
| |
* | generalize bblock_equiv into bblock_simu (abstract_bb)Sylvain Boulmé2019-05-076-73/+59
| |
* | fix linking bug (my fault)David Monniaux2019-05-071-1/+1
| |
* | put the get ra in same bundle as allocframeDavid Monniaux2019-05-071-1/+1
| |
* | gain d'un cycle au moment du freeframe (passer au ret dans le même bundle)David Monniaux2019-05-071-1/+6
| |
* | Merge branch 'mppa-work' of ↵David Monniaux2019-05-074-29/+28
|\ \ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | generalize bblock_equiv into bblock_simuSylvain Boulmé2019-05-074-29/+28
| | |
* | | Merge branch 'mppa-work' of ↵David Monniaux2019-05-064-267/+74
|\| | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | Merge remote-tracking branch 'origin/mppa-peephole' into mppa-workCyril SIX2019-05-064-267/+74
| |\ \
generated by cgit (git 2.34.1) at 2024-07-12 08:52:30 +0000