diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-05 18:03:16 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-05 18:03:16 +0100 |
| commit | 1b5dec35abfaf0aec3cb6005c24f5c93b83e5f4c (patch) | |
| tree | 40b05d31d9cf1d368bef7cd345080ad1166ba0e7 /mppa_k1c/Asmblockdeps.v | |
| parent | e55222aa300b7187a6c0e6d7796165cc1ed2161d (diff) | |
| download | compcert-kvx-1b5dec35abfaf0aec3cb6005c24f5c93b83e5f4c.tar.gz compcert-kvx-1b5dec35abfaf0aec3cb6005c24f5c93b83e5f4c.zip | |
quick fix of equalities issues
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 6bcf9816..6743e198 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -477,7 +477,9 @@ Proof. Qed. -Definition op_eq (o1 o2: op): ?? bool := +Definition op_eq (o1 o2: op): ?? bool := struct_eq o1 o2. (* FIXME - quick hack: could be improved ? *) + +(* match o1, o2 with | Arith i1, Arith i2 => arith_op_eq i1 i2 | Load i1, Load i2 => load_op_eq i1 i2 @@ -490,11 +492,13 @@ Definition op_eq (o1 o2: op): ?? bool := | Fail, Fail => RET true | _, _ => RET false end. +*) Theorem op_eq_correct o1 o2: WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2. Proof. destruct o1, o2; wlp_simplify; try discriminate. +(* - simpl in Hexta. exploit arith_op_eq_correct. eassumption. eauto. congruence. - simpl in Hexta. exploit load_op_eq_correct. eassumption. eauto. congruence. - simpl in Hexta. exploit store_op_eq_correct. eassumption. eauto. congruence. @@ -503,6 +507,7 @@ Proof. - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. - congruence. +*) Qed. End IMPPARAM. |