From bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 11 Jan 2009 11:57:02 +0000 Subject: - Added alignment constraints to memory loads and stores. - In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/InterfGraph.v | 16 ---------------- 1 file changed, 16 deletions(-) (limited to 'backend/InterfGraph.v') diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v index c9891c27..433c074d 100644 --- a/backend/InterfGraph.v +++ b/backend/InterfGraph.v @@ -52,12 +52,6 @@ Module OrderedRegReg := OrderedPair(OrderedReg)(OrderedReg). Module OrderedMreg := OrderedIndexed(IndexedMreg). Module OrderedRegMreg := OrderedPair(OrderedReg)(OrderedMreg). -(* -Module SetDepRegReg := FSetAVL.Make(OrderedRegReg). -Module SetRegReg := NodepOfDep(SetDepRegReg). -Module SetDepRegMreg := FSetAVL.Make(OrderedRegMreg). -Module SetRegMreg := NodepOfDep(SetDepRegMreg). -*) Module SetRegReg := FSetAVL.Make(OrderedRegReg). Module SetRegMreg := FSetAVL.Make(OrderedRegMreg). @@ -226,16 +220,6 @@ Definition all_interf_regs (g: graph) : Regset.t := g.(interf_reg_mreg) Regset.empty). -(* -Lemma mem_add_tail: - forall r r' u, - Regset.mem r u = true -> Regset.mem r (Regset.add r' u) = true. -Proof. - intros. case (Reg.eq r r'); intro. - subst r'. apply Regset.mem_add_same. - rewrite Regset.mem_add_other; auto. -Qed. -*) Lemma in_setregreg_fold: forall g r1 r2 u, SetRegReg.In (r1, r2) g \/ Regset.In r1 u /\ Regset.In r2 u -> -- cgit