From 2ff53c2361773f28027ccc8332e1830686d5bbc6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 16 Jun 2017 11:53:28 +0200 Subject: Extend builtin arguments with a pointer addition operator, continued - Add support for PowerPC, with all addressing modes. - Add support for ARM, with "reg + ofs" addressing mode. - Add support for RISC-V, with the one addressing mode. - Constprop.v: forgot to recurse in BA_addptr - volatile4 test: more tests --- powerpc/SelectOpproof.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'powerpc/SelectOpproof.v') diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 31ddf304..5f87d9b9 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -1038,6 +1038,9 @@ Proof. - subst v. constructor; auto. - inv H. InvEval. simpl in H6; inv H6. constructor; auto. - inv H. InvEval. simpl in H6. inv H6. constructor; auto. +- inv H. repeat constructor; auto. +- inv H. repeat constructor; auto. +- inv H. repeat constructor; auto. - constructor; auto. Qed. -- cgit