diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-11 11:57:02 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-11 11:57:02 +0000 |
commit | bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc (patch) | |
tree | 3efa5cb51e9bb3edc935f42dbd630fce9a170804 /backend/InterfGraph.v | |
parent | cd2449aabe7b259b0fdb8aaa2af65c2b8957ab32 (diff) | |
download | compcert-bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc.tar.gz compcert-bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc.zip |
- 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
Diffstat (limited to 'backend/InterfGraph.v')
-rw-r--r-- | backend/InterfGraph.v | 16 |
1 files changed, 0 insertions, 16 deletions
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 -> |