From bac2a0854ea51217690bc6f225da62053ed7ac06 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 11 Mar 2016 08:48:31 +0100 Subject: Removed unused parameter from is_small/rel_data. The ofs parameter is no longer used. Adopted the proofs and ml code using it. Bug 18394 --- powerpc/Asmgenproof1.v | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'powerpc/Asmgenproof1.v') diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index aa2645f3..70698736 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -844,7 +844,7 @@ Opaque Int.eq. exists rs'. auto with asmgen. (* Oaddrsymbol *) set (v' := Genv.symbol_address ge i i0). - destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ]. + destruct (symbol_is_small_data i) eqn:SD; [ | destruct (symbol_is_rel_data i) ]. (* small data *) Opaque Val.add. econstructor; split. apply exec_straight_one; simpl; reflexivity. @@ -867,7 +867,7 @@ Opaque Val.add. destruct (addimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen. exists rs'; auto with asmgen. (* Oaddsymbol *) - destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ]. + destruct (symbol_is_small_data i) eqn:SD; [ | destruct (symbol_is_rel_data i) ]. (* small data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. split. Simpl. rewrite (Val.add_commut (rs x)). f_equal. @@ -1020,7 +1020,7 @@ Transparent Val.add. (* Aindexed2 *) apply MK2; auto. (* Aglobal *) - destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR. + destruct (symbol_is_small_data i) eqn:SISD; [ | destruct (symbol_is_rel_data i) ]; inv TR. (* Aglobal from small data *) apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. @@ -1048,7 +1048,7 @@ Transparent Val.add. exists rs'; split. apply exec_straight_step with rs1 m; auto. eexact EX'. auto. (* Abased *) - destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]. + destruct (symbol_is_small_data i) eqn:SISD; [ | destruct (symbol_is_rel_data i) ]. (* Abased from small data *) set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))). exploit (MK2 x GPR0 rs1 k). @@ -1232,4 +1232,3 @@ Local Transparent destroyed_by_store. Qed. End CONSTRUCTORS. - -- cgit