From d0590cab5ee32df395c129ee3edfa2dc3aaa202d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 13:30:30 +0200 Subject: begin adapting for LICM phase --- backend/Inject.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/Inject.v') diff --git a/backend/Inject.v b/backend/Inject.v index 4bb25615..2350c149 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -81,7 +81,7 @@ Definition inject prog extra_pc injections : code := *) Section INJECTOR. - Variable gen_injections : function -> PTree.t (list inj_instr). + Variable gen_injections : function -> node -> reg -> PTree.t (list inj_instr). Definition valid_injection_instr (max_reg : reg) (i : inj_instr) := match i with @@ -102,9 +102,9 @@ Section INJECTOR. valid_injections1 (max_pc_function f) (max_reg_function f). Definition transf_function (f : function) : res function := - let injections := PTree.elements (gen_injections f) in let max_pc := max_pc_function f in let max_reg := max_reg_function f in + let injections := PTree.elements (gen_injections f max_pc max_reg) in if valid_injections1 max_pc max_reg injections then OK {| fn_sig := f.(fn_sig); -- cgit