diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-23 08:07:52 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-23 08:07:52 +0200 |
| commit | a42119b0149f887fc109c607ea13c647f920022e (patch) | |
| tree | 97fd5cf96eadbbf42bb2be6cddc0a8b5a74257b5 /aarch64 | |
| parent | bdf9fe65ecb41bca4700eab3109da274a1b47d4b (diff) | |
| download | compcert-kvx-a42119b0149f887fc109c607ea13c647f920022e.tar.gz compcert-kvx-a42119b0149f887fc109c607ea13c647f920022e.zip | |
Complete bblock_non_empty
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/Asmgenproof.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index f0b45013..2f05355f 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -452,7 +452,16 @@ Proof. Admitted. Lemma bblock_non_empty bb: body bb <> nil \/ exit bb <> None. -Admitted. +Proof. + destruct bb. simpl. + unfold non_empty_bblockb in correct. + unfold non_empty_body, non_empty_exit, Is_true in correct. + destruct body, exit. + - right. discriminate. + - contradiction. + - right. discriminate. + - left. discriminate. +Qed. Lemma bblock_size_aux bb: size bb = list_length_z (header bb) + list_length_z (body bb) + Z.of_nat (length_opt (exit bb)). Admitted. |