Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | | transfer function | David Monniaux | 2020-01-08 | 1 | -1/+44 | |
* | | more on semilattices (ADD_BOTTOM) | David Monniaux | 2020-01-08 | 1 | -4/+114 | |
* | | continue implementing semilattice | David Monniaux | 2020-01-08 | 1 | -7/+65 | |
* | | begin lattice | David Monniaux | 2020-01-08 | 1 | -0/+57 | |
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge | David Monniaux | 2019-12-09 | 49 | -157/+1158 | |
|\ \ | ||||||
| * | | make it compile for ARM | David Monniaux | 2019-12-06 | 1 | -4/+4 | |
| * | | finish merge | David Monniaux | 2019-12-02 | 3 | -14/+32 | |
| * | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-12-02 | 4 | -1/+709 | |
| |\ \ | ||||||
| | * | | Duplicateproof: minor edit | Sylvain Boulmé | 2019-11-26 | 1 | -3/+4 | |
| * | | | Merge tag 'v3.6_mppa_2019-09-20' of gricad-gitlab.univ-grenoble-alpes.fr:sixc... | David Monniaux | 2019-09-20 | 10 | -54/+148 | |
| |\ \ \ | ||||||
| * | | | | missing file | David Monniaux | 2019-09-09 | 1 | -0/+26 | |
| * | | | | proof for Allnontrap | David Monniaux | 2019-09-09 | 1 | -0/+215 | |
| * | | | | finished the proofs for non-trapping loads | David Monniaux | 2019-09-08 | 1 | -10/+21 | |
| * | | | | fixes for compiling on other platforms | David Monniaux | 2019-09-07 | 4 | -8/+8 | |
| * | | | | fixes for ARM | David Monniaux | 2019-09-07 | 4 | -21/+12 | |
| * | | | | notrap works on x86 | David Monniaux | 2019-09-07 | 1 | -12/+3 | |
| * | | | | more for passing notrap through x86 | David Monniaux | 2019-09-07 | 1 | -2/+10 | |
| * | | | | ONE "admitted" and things compile | David Monniaux | 2019-09-06 | 11 | -46/+83 | |
| * | | | | progress in proof | David Monniaux | 2019-09-05 | 1 | -14/+27 | |
| * | | | | BSload notrap1 | David Monniaux | 2019-09-05 | 1 | -1/+19 | |
| * | | | | moving forward with proofs | David Monniaux | 2019-09-05 | 2 | -29/+29 | |
| * | | | | more proofs | David Monniaux | 2019-09-05 | 1 | -0/+39 | |
| * | | | | more on notrap | David Monniaux | 2019-09-05 | 2 | -5/+18 | |
| * | | | | more proof | David Monniaux | 2019-09-05 | 1 | -0/+16 | |
| * | | | | some more proofs on notrap | David Monniaux | 2019-09-05 | 1 | -0/+12 | |
| * | | | | more proofs going through | David Monniaux | 2019-09-05 | 9 | -26/+95 | |
| * | | | | LinearizeProof for non trapping loads | David Monniaux | 2019-09-05 | 1 | -16/+32 | |
| * | | | | CSEproof for non trapping loads | David Monniaux | 2019-09-05 | 3 | -19/+89 | |
| * | | | | going forward | David Monniaux | 2019-09-04 | 1 | -41/+50 | |
| * | | | | stuck in CSEproof | David Monniaux | 2019-09-04 | 1 | -1/+10 | |
| * | | | | ca avance | David Monniaux | 2019-09-04 | 1 | -2/+11 | |
| * | | | | begin CSE proof for notrap load | David Monniaux | 2019-09-04 | 1 | -3/+85 | |
| * | | | | begin CSE | David Monniaux | 2019-09-04 | 4 | -18/+23 | |
| * | | | | moved trapping_mode to a more appropriate place | David Monniaux | 2019-09-03 | 1 | -2/+0 | |
| * | | | | Dead code proof for non trapping loads | David Monniaux | 2019-09-03 | 1 | -0/+77 | |
| * | | | | finished Constopproof for non trapping loads | David Monniaux | 2019-09-03 | 1 | -1/+41 | |
| * | | | | advancing in constant propagation | David Monniaux | 2019-09-03 | 2 | -2/+22 | |
| * | | | | Value analysis for non trapping loads | David Monniaux | 2019-09-03 | 2 | -4/+38 | |
| * | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-09-03 | 19 | -134/+439 | |
| |\ \ \ \ | ||||||
| * | | | | | progress on non trapping loads | David Monniaux | 2019-09-03 | 1 | -0/+54 | |
| * | | | | | progress on non trapping loads | David Monniaux | 2019-09-02 | 1 | -8/+32 | |
| * | | | | | avancement (il faut utiliser Vundef visiblement) | David Monniaux | 2019-09-02 | 18 | -41/+114 | |
* | | | | | | merge merge merge | David Monniaux | 2019-11-14 | 1 | -1/+1 | |
* | | | | | | Merge branch 'mppa-work-upstream-merge' of gricad-gitlab.univ-grenoble-alpes.... | David Monniaux | 2019-11-14 | 1 | -3/+1 | |
|\ \ \ \ \ \ | ||||||
| * \ \ \ \ \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge | David Monniaux | 2019-11-14 | 4 | -0/+710 | |
| |\ \ \ \ \ \ | | |_|_|/ / / | |/| | | / / | | | |_|/ / | | |/| | | | ||||||
* | | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge | David Monniaux | 2019-11-14 | 2 | -187/+154 | |
|\ \ \ \ \ \ | | |/ / / / | |/| | | | | ||||||
| * | | | | | simplification of Duplicate: remove xfunction | Sylvain Boulmé | 2019-11-14 | 2 | -187/+154 | |
* | | | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2019-11-13 | 5 | -126/+11 | |
|\ \ \ \ \ \ | | |_|_|_|/ | |/| | | | | ||||||
| * | | | | | Remove no longer needed file PrintLTLin | Bernhard Schommer | 2019-11-12 | 1 | -115/+0 | |
| * | | | | | Make explicit the use of hints from OrderedType (#316) | Vincent Laporte | 2019-10-02 | 2 | -8/+8 |