From 10f3467291b5a1e7ed195906eb23ef1ac57a0bd7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 16 Jul 2021 21:19:32 +0200 Subject: rename parameterized versions --- backend/CSE3.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'backend/CSE3.v') 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. -- cgit