Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Adding copyrights | Cyril SIX | 2020-05-04 | 1 | -0/+12 |
| | |||||
* | forward moves into store source | David Monniaux | 2020-04-20 | 1 | -1/+4 |
| | |||||
* | refine the rules for builtins | David Monniaux | 2020-04-16 | 1 | -4/+19 |
| | |||||
* | progress on CSE2 builtins | David Monniaux | 2020-04-16 | 1 | -5/+15 |
| | |||||
* | forgot an 'Admitted' | David Monniaux | 2020-03-31 | 1 | -1/+1 |
| | |||||
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-03-11 | 1 | -1/+4 |
|\ | |||||
| * | remet is_trivial_op dans CSE2 | David Monniaux | 2020-03-11 | 1 | -1/+4 |
| | | |||||
* | | same version as in dm-cse2 | David Monniaux | 2020-03-03 | 1 | -24/+24 |
|/ | |||||
* | fixed CSE2 for mppa_k1c | David Monniaux | 2020-03-03 | 1 | -668/+160 |
|\ | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2 | ||||
| * | CSE2 alias analysis for Risc-V | David Monniaux | 2020-03-03 | 1 | -1/+1 |
| | | |||||
| * | moved away x86-dependent parts | David Monniaux | 2020-03-03 | 1 | -38/+0 |
| | | |||||
| * | modularize proof | David Monniaux | 2020-03-03 | 1 | -29/+10 |
| | | |||||
| * | may_overlap_sound | David Monniaux | 2020-03-03 | 1 | -0/+38 |
| | | |||||
| * | starting to move x86 stuff to x86 | David Monniaux | 2020-03-03 | 1 | -201/+1 |
| | | |||||
| * | offsets in globals for x86 | David Monniaux | 2020-03-03 | 1 | -1/+78 |
| | | |||||
| * | globals alias analysis for x86 | David Monniaux | 2020-03-03 | 1 | -10/+57 |
| | | |||||
| * | with indexed/indexed alias analysis for x86 | David Monniaux | 2020-03-03 | 1 | -2/+2 |
| | | |||||
| * | kill_store_sound | David Monniaux | 2020-03-02 | 1 | -10/+25 |
| | | |||||
| * | kill_store1_sound | David Monniaux | 2020-03-02 | 1 | -3/+41 |
| | | |||||
| * | load_store_away | David Monniaux | 2020-03-02 | 1 | -1/+2 |
| | | |||||
| * | swap predicate | David Monniaux | 2020-03-02 | 1 | -13/+19 |
| | | |||||
| * | works on x86 x86_64 | David Monniaux | 2020-03-02 | 1 | -29/+47 |
| | | |||||
| * | playing with offsets | David Monniaux | 2020-03-02 | 1 | -1/+67 |
| | | |||||
* | | Merge branch 'mppa-cse2' of ↵ | David Monniaux | 2020-03-03 | 1 | -78/+430 |
|\ \ | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work | ||||
| * | | CSE2 with NOTRAP | David Monniaux | 2020-02-03 | 1 | -91/+184 |
| | | | |||||
| * | | NOTRAP in CSE2: progress | David Monniaux | 2020-02-03 | 1 | -31/+259 |
| | | | |||||
| * | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2 | 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 | 1 | -0/+8 |
| |\ \ | |||||
| * | | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2 | David Monniaux | 2020-01-28 | 1 | -65/+96 |
| | | | | |||||
* | | | | CSE2 now uses is_trivial_op | David Monniaux | 2020-02-27 | 1 | -2/+21 |
| | | | | |||||
* | | | | add hint | David Monniaux | 2020-02-05 | 1 | -0/+1 |
| | | | | |||||
* | | | | wellformed_reg_kill_mem | David Monniaux | 2020-02-05 | 1 | -1/+17 |
| | | | | |||||
* | | | | rm useless admitted lemma | David Monniaux | 2020-02-05 | 1 | -5/+0 |
| | | | | |||||
* | | | | wellformed_reg_kill_reg simpliied | David Monniaux | 2020-02-05 | 1 | -8/+3 |
| | | | | |||||
* | | | | wellformed_reg_kill_reg | David Monniaux | 2020-02-05 | 1 | -0/+129 |
| | | | | |||||
* | | | | progress on wellformed reg | David Monniaux | 2020-02-05 | 1 | -0/+32 |
| | | | | |||||
* | | | | wellformedness for reg begins; simplified | David Monniaux | 2020-02-04 | 1 | -12/+9 |
| | | | | |||||
* | | | | wellformedness for reg begins | David Monniaux | 2020-02-04 | 1 | -0/+53 |
| | | | | |||||
* | | | | kill memory focused | David Monniaux | 2020-02-04 | 1 | -19/+45 |
| | | | | |||||
* | | | | invariant guaranteed | David Monniaux | 2020-02-04 | 1 | -3/+53 |
| | | | | |||||
* | | | | wellformedness for memory | David Monniaux | 2020-02-04 | 1 | -13/+152 |
| | | | | |||||
* | | | | begin well formedness | David Monniaux | 2020-02-04 | 1 | -0/+98 |
| | | | | |||||
* | | | | stuff information into a record | David Monniaux | 2020-02-04 | 1 | -20/+30 |
| |_|/ |/| | | |||||
* | | | another version of proof that allows Vundef in loaded values | David Monniaux | 2020-02-03 | 1 | -18/+18 |
| |/ |/| | |||||
* | | comments | David Monniaux | 2020-02-03 | 1 | -0/+8 |
|/ | |||||
* | with loads too ? | David Monniaux | 2020-01-28 | 1 | -6/+67 |
| | |||||
* | load_sound | David Monniaux | 2020-01-28 | 1 | -0/+96 |
| | |||||
* | find_load_sound | David Monniaux | 2020-01-28 | 1 | -4/+92 |
| | |||||
* | much better - seems to eliminate CSE not containing loads | David Monniaux | 2020-01-28 | 1 | -1/+17 |
| | |||||
* | still buggy | David Monniaux | 2020-01-28 | 1 | -36/+67 |
| |