From f401437a97b09726d029e3a1b65143f34baaea70 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 24 Feb 2013 09:40:25 +0000 Subject: Updated ARM and PowerPC ports with new handling of __builtin_annot. ARM: add support for builtin_volatile_{read,write}_global, after all. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/ConstpropOpproof.v | 13 ------------- 1 file changed, 13 deletions(-) (limited to 'arm/ConstpropOpproof.v') diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index e7e6a419..c7de86d9 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -450,19 +450,6 @@ Proof. auto. Qed. -Lemma builtin_strength_reduction_correct: - forall ef args vl m t vres m', - vl = approx_regs app args -> - external_call ef ge rs##args m t vres m' -> - let (ef', args') := builtin_strength_reduction ef args vl in - external_call ef' ge rs##args' m t vres m'. -Proof. - (* force MATCH to be used *) - assert (val_match_approx (approx_reg app 1%positive) rs#(1%positive)) - by (apply MATCH). - unfold builtin_strength_reduction; intros; simpl; auto. -Qed. - End STRENGTH_REDUCTION. End ANALYSIS. -- cgit