Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2 | David Monniaux | 2020-02-03 | 1 | -18/+18 |
|\ | |||||
| * | another version of proof that allows Vundef in loaded values | David Monniaux | 2020-02-03 | 1 | -18/+18 |
* | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2 | David Monniaux | 2020-02-03 | 2 | -0/+14 |
|\| | |||||
| * | comments | David Monniaux | 2020-02-03 | 2 | -0/+14 |
* | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2 | David Monniaux | 2020-01-28 | 2 | -0/+1834 |
|\| | |||||
| * | with loads too ? | David Monniaux | 2020-01-28 | 2 | -8/+119 |
| * | load_sound | David Monniaux | 2020-01-28 | 1 | -0/+96 |
| * | find_load_sound | David Monniaux | 2020-01-28 | 1 | -4/+92 |
| * | begin adding loads | David Monniaux | 2020-01-28 | 1 | -2/+7 |
| * | much better - seems to eliminate CSE not containing loads | David Monniaux | 2020-01-28 | 2 | -2/+18 |
| * | still buggy | David Monniaux | 2020-01-28 | 2 | -56/+95 |
| * | connected (just a silly problem) | David Monniaux | 2020-01-28 | 1 | -2/+8 |
| * | CSE2 now works for expressions | David Monniaux | 2020-01-28 | 2 | -47/+69 |
| * | now going back to op | David Monniaux | 2020-01-28 | 1 | -45/+6 |
| * | rework | David Monniaux | 2020-01-28 | 1 | -20/+49 |
| * | sem_rel_b_ge | David Monniaux | 2020-01-28 | 1 | -61/+152 |
| * | sem_rel_b_ge | David Monniaux | 2020-01-28 | 1 | -18/+77 |
| * | CSE2 split in two files | David Monniaux | 2020-01-28 | 2 | -827/+837 |
| * | progress | David Monniaux | 2020-01-27 | 1 | -0/+467 |
| * | use in transformation | David Monniaux | 2020-01-27 | 1 | -3/+21 |
| * | find_op_sound | David Monniaux | 2020-01-27 | 1 | -1/+110 |
| * | goes to the end but does not find available ops | David Monniaux | 2020-01-27 | 1 | -13/+5 |
| * | simpler definitions | David Monniaux | 2020-01-27 | 1 | -41/+24 |
| * | static analysis done | David Monniaux | 2020-01-27 | 1 | -20/+7 |
| * | kill_mem_sound | David Monniaux | 2020-01-27 | 1 | -8/+59 |
| * | renamed kill_reg into kill_mem | David Monniaux | 2020-01-27 | 1 | -11/+11 |
| * | gen_oper_sound | David Monniaux | 2020-01-27 | 1 | -1/+37 |
| * | oper_sound | David Monniaux | 2020-01-27 | 1 | -0/+27 |
| * | oper1_sound | David Monniaux | 2020-01-27 | 1 | -1/+10 |
| * | arg replace | David Monniaux | 2020-01-27 | 1 | -1/+87 |
| * | move sound | David Monniaux | 2020-01-27 | 1 | -19/+85 |
| * | begin proving stuff | David Monniaux | 2020-01-27 | 1 | -0/+436 |
* | | FINISHED the forward-moves pass | David Monniaux | 2020-01-09 | 1 | -2/+6 |
* | | nearly done | David Monniaux | 2020-01-09 | 1 | -3/+5 |
* | | fix move | David Monniaux | 2020-01-09 | 1 | -1/+3 |
* | | fix move | David Monniaux | 2020-01-09 | 2 | -4/+120 |
* | | return is ok | David Monniaux | 2020-01-09 | 1 | -14/+53 |
* | | proof of return | David Monniaux | 2020-01-09 | 1 | -1/+59 |
* | | we still have issues with call stacks | David Monniaux | 2020-01-09 | 2 | -15/+51 |
* | | moving forward with proofs | David Monniaux | 2020-01-09 | 2 | -5/+20 |
* | | proof for jumptable | David Monniaux | 2020-01-09 | 1 | -1/+17 |
* | | more proofs | David Monniaux | 2020-01-09 | 1 | -1/+18 |
* | | fix bug and forward in proofs | David Monniaux | 2020-01-09 | 2 | -2/+18 |
* | | some more proof | David Monniaux | 2020-01-09 | 1 | -3/+53 |
* | | moving forward with proofs | David Monniaux | 2020-01-09 | 1 | -1/+59 |
* | | fix bug in xfer function | David Monniaux | 2020-01-09 | 1 | -1/+2 |
* | | progressing in proofs | David Monniaux | 2020-01-08 | 2 | -12/+101 |
* | | moving forward in proofs | David Monniaux | 2020-01-08 | 1 | -2/+19 |
* | | correct semantics for bottom | David Monniaux | 2020-01-08 | 2 | -14/+45 |
* | | progressing towards a proof | David Monniaux | 2020-01-08 | 2 | -47/+150 |