diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2019-03-25 11:14:17 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2019-03-25 11:14:17 +0100 |
| commit | f7a4a67784b97013cd314fb4c50bd94abdb9c55e (patch) | |
| tree | f4fd8443d712aee18809cb569c8578a56cb08e98 /configure | |
| parent | 8c1735389e54d6ed4d8552a9e3f568d5edc5fa72 (diff) | |
| download | compcert-f7a4a67784b97013cd314fb4c50bd94abdb9c55e.tar.gz compcert-f7a4a67784b97013cd314fb4c50bd94abdb9c55e.zip | |
RTLgenproof: destruct too deep
`external_call_mem_extends` returns a conjunction of 4 properties,
but the destruct pattern was 5 level deep.
(Reported by Jeremie Koenig in pull request #278.)
Diffstat (limited to 'configure')
0 files changed, 0 insertions, 0 deletions