aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
* 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
|
* continue implementing semilatticeDavid Monniaux2020-01-081-7/+65
|
* begin latticeDavid Monniaux2020-01-081-0/+57
|
* Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-mergeDavid Monniaux2019-12-0949-157/+1158
|\
| * make it compile for ARMDavid Monniaux2019-12-061-4/+4
| |
| * finish mergeDavid Monniaux2019-12-023-14/+32
| |
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-024-1/+709
| |\
| | * Duplicateproof: minor editSylvain Boulmé2019-11-261-3/+4
| | |
| * | Merge tag 'v3.6_mppa_2019-09-20' of ↵David Monniaux2019-09-2010-54/+148
| |\ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
| * | | missing fileDavid Monniaux2019-09-091-0/+26
| | | |
| * | | proof for AllnontrapDavid Monniaux2019-09-091-0/+215
| | | |
| * | | finished the proofs for non-trapping loadsDavid Monniaux2019-09-081-10/+21
| | | |
| * | | fixes for compiling on other platformsDavid Monniaux2019-09-074-8/+8
| | | |
| * | | fixes for ARMDavid Monniaux2019-09-074-21/+12
| | | |
| * | | notrap works on x86David Monniaux2019-09-071-12/+3
| | | |
| * | | more for passing notrap through x86David Monniaux2019-09-071-2/+10
| | | |
| * | | ONE "admitted" and things compileDavid Monniaux2019-09-0611-46/+83
| | | |
| * | | progress in proofDavid Monniaux2019-09-051-14/+27
| | | |
| * | | BSload notrap1David Monniaux2019-09-051-1/+19
| | | |
| * | | moving forward with proofsDavid Monniaux2019-09-052-29/+29
| | | |
| * | | more proofsDavid Monniaux2019-09-051-0/+39
| | | |
| * | | more on notrapDavid Monniaux2019-09-052-5/+18
| | | |
| * | | more proofDavid Monniaux2019-09-051-0/+16
| | | |
| * | | some more proofs on notrapDavid Monniaux2019-09-051-0/+12
| | | |
| * | | more proofs going throughDavid Monniaux2019-09-059-26/+95
| | | |
| * | | LinearizeProof for non trapping loadsDavid Monniaux2019-09-051-16/+32
| | | |
| * | | CSEproof for non trapping loadsDavid Monniaux2019-09-053-19/+89
| | | |
| * | | going forwardDavid Monniaux2019-09-041-41/+50
| | | |
| * | | stuck in CSEproofDavid Monniaux2019-09-041-1/+10
| | | |
generated by cgit (git 2.34.1) at 2024-07-06 15:55:11 +0000