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 | |
| 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.)
| -rw-r--r-- | backend/RTLgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index b003eb10..b94ec22f 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -704,7 +704,7 @@ Proof. intros; red; intros. inv TE. exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RR1 [RO1 EXT1]]]]]]. exploit external_call_mem_extends; eauto. - intros [v' [tm2 [A [B [C [D E]]]]]]. + intros [v' [tm2 [A [B [C D]]]]]. exists (rs1#rd <- v'); exists tm2. (* Exec *) split. eapply star_right. eexact EX1. @@ -736,7 +736,7 @@ Proof. intros; red; intros. inv TE. exploit H3; eauto. intros [rs1 [tm1 [EX1 [ME1 [RR1 [RO1 EXT1]]]]]]. exploit external_call_mem_extends; eauto. - intros [v' [tm2 [A [B [C [D E]]]]]]. + intros [v' [tm2 [A [B [C D]]]]]. exploit function_ptr_translated; eauto. simpl. intros [tf [P Q]]. inv Q. exists (rs1#rd <- v'); exists tm2. (* Exec *) |