diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-02 20:51:23 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-02 20:52:30 +0100 |
| commit | 710979db5857d58de4478c3e8a6d645ebab9d8c1 (patch) | |
| tree | e0c43496460e57024659a097dcae9d73861e57fe /src/hls/HTLgenspec.v | |
| parent | 87fba8b56e25130519f7b4bea4b9887bc14ec31f (diff) | |
| download | vericert-710979db5857d58de4478c3e8a6d645ebab9d8c1.tar.gz vericert-710979db5857d58de4478c3e8a6d645ebab9d8c1.zip | |
Check whether callee is internal for Icall
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 6 |
1 files changed, 0 insertions, 6 deletions
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 : |