Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 |
* | bogus proof | David Monniaux | 2020-01-08 | 1 | -0/+141 |
* | I *think* the transformation is now done | David Monniaux | 2020-01-08 | 1 | -2/+57 |
* | 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 |