diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-02 17:19:15 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:07 +0200 |
| commit | a80a8b9ee92c9dd015d53d8de03b99c0d228d390 (patch) | |
| tree | 962123c4c33a38ae42ba3218f09329349ff3887b /backend | |
| parent | 917859721f6423b24788ec6219774b5196b02ec1 (diff) | |
| download | compcert-kvx-a80a8b9ee92c9dd015d53d8de03b99c0d228d390.tar.gz compcert-kvx-a80a8b9ee92c9dd015d53d8de03b99c0d228d390.zip | |
MPPA - Started Asm.v + Asmgen.v, commenting out some instructions
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Asmgenproof0.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index f6f03868..b1b7453a 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -39,12 +39,14 @@ Proof. unfold ireg_of; intros. destruct (preg_of r); inv H; auto. Qed. +(* FIXME - Replaced FR by IR for MPPA *) Lemma freg_of_eq: - forall r r', freg_of r = OK r' -> preg_of r = FR r'. + forall r r', freg_of r = OK r' -> preg_of r = IR r'. Proof. unfold freg_of; intros. destruct (preg_of r); inv H; auto. Qed. + Lemma preg_of_injective: forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2. Proof. |