From 710979db5857d58de4478c3e8a6d645ebab9d8c1 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Mon, 2 Aug 2021 20:51:23 +0100 Subject: Check whether callee is internal for Icall --- src/hls/HTLgenspec.v | 6 ------ 1 file changed, 6 deletions(-) (limited to 'src/hls/HTLgenspec.v') diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 7480231..387def0 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -75,12 +75,6 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt - tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*) Hint Constructors tr_instr : htlspec. -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. - Inductive tr_code (ge : RTL.genv) (c : RTL.code) (pc : RTL.node) (stmnts : datapath) (trans : controllogic) (externctrl : AssocMap.t (ident * controlsignal)) (fin rtrn st stk : reg) : RTL.instruction -> Prop := | tr_code_single : -- cgit