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 /aarch64/Machregsaux.ml | |
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 'aarch64/Machregsaux.ml')
0 files changed, 0 insertions, 0 deletions