diff options
Diffstat (limited to 'backend/CSE3.v')
-rw-r--r-- | backend/CSE3.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v index 5d05821a..f3a0af24 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -82,7 +82,7 @@ Definition find_cond_in_fmap fmap pc cond args := end else None. -Definition transf_instr (fmap : PMap.t RB.t) +Definition param_transf_instr (fmap : PMap.t RB.t) (pc: node) (instr: instruction) := match instr with | Iop op args dst s => @@ -118,7 +118,7 @@ Definition transf_instr (fmap : PMap.t RB.t) end. End REWRITE. -Definition transf_function (f: function) : res function := +Definition param_transf_function (f: function) : res function := do tenv <- type_function f; let (invariants, hints) := preanalysis tenv f in let ctx := context_from_hints hints in @@ -127,15 +127,15 @@ Definition transf_function (f: function) : res function := OK {| fn_sig := f.(fn_sig); fn_params := f.(fn_params); fn_stacksize := f.(fn_stacksize); - fn_code := PTree.map (transf_instr (ctx := ctx) invariants) + fn_code := PTree.map (param_transf_instr (ctx := ctx) invariants) f.(fn_code); fn_entrypoint := f.(fn_entrypoint) |} else Error (msg "cse3: not inductive"). -Definition transf_fundef (fd: fundef) : res fundef := - AST.transf_partial_fundef transf_function fd. +Definition param_transf_fundef (fd: fundef) : res fundef := + AST.transf_partial_fundef param_transf_function fd. -Definition transf_program (p: program) : res program := - transform_partial_program transf_fundef p. +Definition param_transf_program (p: program) : res program := + transform_partial_program param_transf_fundef p. End PARAMS. |