diff options
| author | Léo Gourdin <leo.gourdin@lilo.org> | 2020-10-11 12:00:58 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@lilo.org> | 2020-10-11 12:00:58 +0200 |
| commit | 545bd78efd711ebb69cac6e5ff12429362002074 (patch) | |
| tree | 7ffd7364fb76a3a58c1d321890da75177cc7e589 /x86_64 | |
| parent | 4529cd8f17c53eae5b9a0f78cefb642a06f150eb (diff) | |
| download | compcert-kvx-545bd78efd711ebb69cac6e5ff12429362002074.tar.gz compcert-kvx-545bd78efd711ebb69cac6e5ff12429362002074.zip | |
Adding a lemma for exec load propagation.
The commit also contains an incomplete proof for assert (BDYLENPOS: ((length li) < length (body bb))%nat).
Diffstat (limited to 'x86_64')
0 files changed, 0 insertions, 0 deletions