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