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/LTL.v | |
parent | 1fe28ba1ec3dd0657b121c4a911ee1cb046bab09 (diff) | |
download | compcert-4b119d6f9f0e846edccaf5c08788ca1615b22526.tar.gz compcert-4b119d6f9f0e846edccaf5c08788ca1615b22526.zip |
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/LTL.v')
-rw-r--r-- | backend/LTL.v | 31 |
1 files changed, 14 insertions, 17 deletions
diff --git a/backend/LTL.v b/backend/LTL.v index 3a61e6d0..2505566f 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -51,9 +51,7 @@ Record function: Type := mkfunction { fn_params: list loc; fn_stacksize: Z; fn_code: code; - fn_entrypoint: node; - fn_nextpc: node; - fn_code_wf: forall (pc: node), Plt pc fn_nextpc \/ fn_code!pc = None + fn_entrypoint: node }. Definition fundef := AST.fundef function. @@ -256,18 +254,17 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop := (** Computation of the possible successors of an instruction. This is used in particular for dataflow analyses. *) -Definition successors (f: function) (pc: node) : list node := - match f.(fn_code)!pc with - | None => nil - | Some i => - match i with - | Lnop s => s :: nil - | Lop op args res s => s :: nil - | Lload chunk addr args dst s => s :: nil - | Lstore chunk addr args src s => s :: nil - | Lcall sig ros args res s => s :: nil - | Ltailcall sig ros args => nil - | Lcond cond args ifso ifnot => ifso :: ifnot :: nil - | Lreturn optarg => nil - end +Definition successors_instr (i: instruction) : list node := + match i with + | Lnop s => s :: nil + | Lop op args res s => s :: nil + | Lload chunk addr args dst s => s :: nil + | Lstore chunk addr args src s => s :: nil + | Lcall sig ros args res s => s :: nil + | Ltailcall sig ros args => nil + | Lcond cond args ifso ifnot => ifso :: ifnot :: nil + | Lreturn optarg => nil end. + +Definition successors (f: function): PTree.t (list node) := + PTree.map (fun pc i => successors_instr i) f.(fn_code). |