From 4b119d6f9f0e846edccaf5c08788ca1615b22526 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 16 Aug 2009 15:35:09 +0000 Subject: Cil2Csyntax: added goto and labels; added assignment between structs Kildall: simplified the interface Constprop, CSE, Allocation, Linearize: updated for the new Kildall RTL, LTL: removed the well-formedness condition on the CFG, it is no longer necessary with the new Kildall and it is problematic for validated optimizations. Maps: more efficient implementation of PTree.fold. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenspec.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'backend/RTLgenspec.v') diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 8e61271..caf93c8 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -807,7 +807,7 @@ Inductive tr_stmt (c: code) (map: mapping): Inductive tr_function: CminorSel.function -> RTL.function -> Prop := | tr_function_intro: - forall f code rparams map1 s0 s1 i1 rvars map2 s2 i2 nentry ngoto nret rret orret nextnode wfcode, + forall f code rparams map1 s0 s1 i1 rvars map2 s2 i2 nentry ngoto nret rret orret, add_vars init_mapping f.(CminorSel.fn_params) s0 = OK (rparams, map1) s1 i1 -> add_vars map1 f.(CminorSel.fn_vars) s1 = OK (rvars, map2) s2 i2 -> orret = ret_reg f.(CminorSel.fn_sig) rret -> @@ -818,9 +818,7 @@ Inductive tr_function: CminorSel.function -> RTL.function -> Prop := rparams f.(CminorSel.fn_stackspace) code - nentry - nextnode - wfcode). + nentry). (** * Correctness proof of the translation functions *) -- cgit v1.2.3