diff options
Diffstat (limited to 'powerpc/Asmgenretaddr.v')
| -rw-r--r-- | powerpc/Asmgenretaddr.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v index adc15297..081336ca 100644 --- a/powerpc/Asmgenretaddr.v +++ b/powerpc/Asmgenretaddr.v @@ -112,6 +112,11 @@ Lemma addimm_tail: Proof. unfold addimm; intros; IsTail. Qed. Hint Resolve addimm_tail: ppcretaddr. +Lemma andimm_base_tail: + forall r1 r2 n k, is_tail k (andimm_base r1 r2 n k). +Proof. unfold andimm_base; intros; IsTail. Qed. +Hint Resolve andimm_base_tail: ppcretaddr. + Lemma andimm_tail: forall r1 r2 n k, is_tail k (andimm r1 r2 n k). Proof. unfold andimm; intros; IsTail. Qed. @@ -127,6 +132,11 @@ Lemma xorimm_tail: Proof. unfold xorimm; intros; IsTail. Qed. Hint Resolve xorimm_tail: ppcretaddr. +Lemma rolm_tail: + forall r1 r2 amount mask k, is_tail k (rolm r1 r2 amount mask k). +Proof. unfold rolm; intros; IsTail. Qed. +Hint Resolve rolm_tail: ppcretaddr. + Lemma loadind_tail: forall base ofs ty dst k, is_tail k (loadind base ofs ty dst k). Proof. unfold loadind; intros. destruct ty; IsTail. Qed. |