diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-16 15:35:09 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-16 15:35:09 +0000 |
| commit | 4b119d6f9f0e846edccaf5c08788ca1615b22526 (patch) | |
| tree | 66cf55decd8d950d0bdc1050448aa3ee448ca13a /backend/RTLgenspec.v | |
| parent | 1fe28ba1ec3dd0657b121c4a911ee1cb046bab09 (diff) | |
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
Diffstat (limited to 'backend/RTLgenspec.v')
| -rw-r--r-- | backend/RTLgenspec.v | 6 |
1 files changed, 2 insertions, 4 deletions
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 *) |