diff options
| -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. |