From a42119b0149f887fc109c607ea13c647f920022e Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Thu, 23 Jul 2020 08:07:52 +0200 Subject: Complete bblock_non_empty --- aarch64/Asmgenproof.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'aarch64') 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. -- cgit