diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-10-23 18:42:26 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-10-23 18:42:26 +0200 |
| commit | 70fed34d1b8600019c50f6ff897f22794020fb31 (patch) | |
| tree | 9bd25205e2dee5c9b03abf6558835b6ba6725241 /mppa_k1c/Asmblock.v | |
| parent | e71af11d385f4763ec92daa7df4a2326c0c6001a (diff) | |
| download | compcert-kvx-70fed34d1b8600019c50f6ff897f22794020fb31.tar.gz compcert-kvx-70fed34d1b8600019c50f6ff897f22794020fb31.zip | |
ajoute un axiom a virer plus tard
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 6afa6e56..db370d13 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -384,7 +384,11 @@ Coercion PCtlFlow: cf_instruction >-> control. (** * Definition of a bblock *) Definition non_empty_bblock (body: list basic) (exit: option control): Prop - := body <> nil \/ exit <> None. (* TODO: use booleans instead of Prop to enforce proof irrelevance in bblock type ? *) + := body <> nil \/ exit <> None. + +(* TODO: use booleans instead of Prop to enforce proof irrelevance in bblock type + in order to prove bblock_equality below +*) (* Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res, exit = Some (PExpand (Pbuiltin ef args res)) -> body = nil. @@ -405,6 +409,8 @@ Record bblock := mk_bblock { Ltac bblock_auto_correct := ((* split; *)try discriminate; try (left; discriminate); try (right; discriminate)). Local Obligation Tactic := bblock_auto_correct. +Axiom bblock_equality: forall bb1 bb2, header bb1=header bb2 -> body bb1 = body bb2 -> exit bb1 = exit bb2 -> bb1 = bb2. + (* FIXME: redundant with definition in Machblock *) Definition length_opt {A} (o: option A) : nat := match o with |