diff options
author | tvdd <tvdd@debian.lan> | 2019-04-04 17:59:06 +0200 |
---|---|---|
committer | tvdd <tvdd@debian.lan> | 2019-04-04 17:59:06 +0200 |
commit | 8610699d59dab908ec5954733753008ecfb871ff (patch) | |
tree | 65794ad0803c33018ca681116f9f0744c164c24b | |
parent | b4ed42a385a4560c82d9ffa234fd00608f431583 (diff) | |
download | compcert-kvx-8610699d59dab908ec5954733753008ecfb871ff.tar.gz compcert-kvx-8610699d59dab908ec5954733753008ecfb871ff.zip |
is_header, is_body, is_exit
-rw-r--r-- | mppa_k1c/Machblockgenproof.v | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index 267cbebb..792fcc90 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -343,18 +343,30 @@ Lemma size_nonzero c b bl: is_trans_code c (b :: bl) -> size b <> 0. Proof. intros H; inversion H; subst. -Admitted. (* A FINIR *) + - rewrite size_add_to_newblock; omega. + - rewrite size_add_label; omega. + - rewrite size_add_basic; auto; omega. +Qed. (* TODO: définir les predicats inductifs suivants de façon à prouver le lemme [is_trans_code_decompose] ci-dessous *) + Inductive is_header: list label -> Mach.code -> Mach.code -> Prop := - . (* A FAIRE *) + | header_empty : is_header nil nil nil + | header_not_label i c: forall l, i <> Mlabel l -> is_header nil (i::c) c + | header_is_label l h c c0: is_header h c c0 -> is_header (l::h) ((Mlabel l)::c) c0 + . Inductive is_body: list basic_inst -> Mach.code -> Mach.code -> Prop := - . (* A FAIRE *) + | body_empty : is_body nil nil nil + | body_not_bi i c: forall bi, (trans_inst i) <> (MB_basic bi) -> is_body nil (i::c) c + | body_is_bi i lbi c0 c1: forall bi, (trans_inst i) = MB_basic bi -> is_body lbi c0 c1 -> is_body (bi::lbi) (i::c0) c1 + . Inductive is_exit: option control_flow_inst -> Mach.code -> Mach.code -> Prop := - . (* A FAIRE *) + | exit_not_cfi i c : forall cfi, (trans_inst i) <> MB_cfi cfi -> is_exit None (i::c) c + | exit_is_cfi i c : forall cfi, (trans_inst i) = MB_cfi cfi -> is_exit (Some cfi) (i::c) c + . Lemma trans_code_decompose c bc: is_trans_code c bc -> forall b blc, bc=(b::blc) -> |