From e44054e439adfc2128e93e652178c6df42ee9159 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Thu, 19 Aug 2021 14:44:34 +0100 Subject: Find called module in Icall proof --- src/hls/HTLgen.v | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to 'src/hls/HTLgen.v') diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index c63847a..3b4b934 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -518,12 +518,6 @@ Fixpoint xmap_externctrl_params (n : nat) (fn : ident) (l : list reg) := Definition map_externctrl_params := xmap_externctrl_params 0. -Definition rtl_find_func (ge : RTL.genv) (symb : AST.ident) := - match Globalenvs.Genv.find_symbol ge symb with - | None => None - | Some b => Globalenvs.Genv.find_funct_ptr ge b - end. - Definition transf_instr (ge : RTL.genv) (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with (n, i) => @@ -552,7 +546,7 @@ Definition transf_instr (ge : RTL.genv) (fin rtrn stack: reg) (ni: node * instru | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.") | Icall sig (inr fn) args dst n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned - then match rtl_find_func ge fn with + then match find_func ge fn with | Some (AST.Internal _) => do params <- map_externctrl_params fn args; -- cgit