From bc24cf49659f91245d8f42ca06fbe7d21a5c06cd Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 May 2013 15:04:26 +0000 Subject: Extend CSE of loads following stores to chunks Mint64 and Mfloat64al32. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2231 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/CSEproof.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'backend/CSEproof.v') diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 1e269f84..65f67ad2 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -696,6 +696,8 @@ Proof. destruct chunk; auto; apply N3. simpl in H3. destruct (rs#src); auto || contradiction. simpl in H3. destruct (rs#src); auto || contradiction. + simpl in H3. destruct (rs#src); auto || contradiction. + simpl in H3. destruct (rs#src); auto || contradiction. Qed. (** Correctness of [reg_valnum]: if it returns a register [r], -- cgit