aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-282-0/+1834
|\
| * with loads too ?David Monniaux2020-01-282-8/+119
| * load_soundDavid Monniaux2020-01-281-0/+96
| * find_load_soundDavid Monniaux2020-01-281-4/+92
| * begin adding loadsDavid Monniaux2020-01-281-2/+7
| * much better - seems to eliminate CSE not containing loadsDavid Monniaux2020-01-282-2/+18
| * still buggyDavid Monniaux2020-01-282-56/+95
| * connected (just a silly problem)David Monniaux2020-01-281-2/+8
| * CSE2 now works for expressionsDavid Monniaux2020-01-282-47/+69
| * now going back to opDavid Monniaux2020-01-281-45/+6
| * reworkDavid Monniaux2020-01-281-20/+49
| * sem_rel_b_geDavid Monniaux2020-01-281-61/+152
| * sem_rel_b_geDavid Monniaux2020-01-281-18/+77
| * CSE2 split in two filesDavid Monniaux2020-01-282-827/+837
| * progressDavid Monniaux2020-01-271-0/+467
| * use in transformationDavid Monniaux2020-01-271-3/+21
| * find_op_soundDavid Monniaux2020-01-271-1/+110
| * goes to the end but does not find available opsDavid Monniaux2020-01-271-13/+5
| * simpler definitionsDavid Monniaux2020-01-271-41/+24
| * static analysis doneDavid Monniaux2020-01-271-20/+7
| * kill_mem_soundDavid Monniaux2020-01-271-8/+59
| * renamed kill_reg into kill_memDavid Monniaux2020-01-271-11/+11
| * gen_oper_soundDavid Monniaux2020-01-271-1/+37
| * oper_soundDavid Monniaux2020-01-271-0/+27
| * oper1_soundDavid Monniaux2020-01-271-1/+10
| * arg replaceDavid Monniaux2020-01-271-1/+87
| * move soundDavid Monniaux2020-01-271-19/+85
| * begin proving stuffDavid Monniaux2020-01-271-0/+436
* | FINISHED the forward-moves passDavid Monniaux2020-01-091-2/+6
* | nearly doneDavid Monniaux2020-01-091-3/+5
* | fix moveDavid Monniaux2020-01-091-1/+3
* | fix moveDavid Monniaux2020-01-092-4/+120
* | return is okDavid Monniaux2020-01-091-14/+53
* | proof of returnDavid Monniaux2020-01-091-1/+59
* | we still have issues with call stacksDavid Monniaux2020-01-092-15/+51
* | moving forward with proofsDavid Monniaux2020-01-092-5/+20
* | proof for jumptableDavid Monniaux2020-01-091-1/+17
* | more proofsDavid Monniaux2020-01-091-1/+18
* | fix bug and forward in proofsDavid Monniaux2020-01-092-2/+18
* | some more proofDavid Monniaux2020-01-091-3/+53
* | moving forward with proofsDavid Monniaux2020-01-091-1/+59
* | fix bug in xfer functionDavid Monniaux2020-01-091-1/+2
* | progressing in proofsDavid Monniaux2020-01-082-12/+101
* | moving forward in proofsDavid Monniaux2020-01-081-2/+19
* | correct semantics for bottomDavid Monniaux2020-01-082-14/+45
* | progressing towards a proofDavid Monniaux2020-01-082-47/+150
* | bogus proofDavid Monniaux2020-01-081-0/+141
* | I *think* the transformation is now doneDavid Monniaux2020-01-081-2/+57
* | transfer functionDavid Monniaux2020-01-081-1/+44
* | more on semilattices (ADD_BOTTOM)David Monniaux2020-01-081-4/+114
generated by cgit (git 2.34.1) at 2024-06-13 06:06:53 +0000