diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-19 14:44:34 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-19 14:44:34 +0100 |
| commit | e44054e439adfc2128e93e652178c6df42ee9159 (patch) | |
| tree | 57f299f94f16ae698efaf2fedc965f5a069f0534 /src/hls/HTLgenspec.v | |
| parent | 56f442f41aba4efb3929b79f15e5a4cc87579acb (diff) | |
| download | vericert-e44054e439adfc2128e93e652178c6df42ee9159.tar.gz vericert-e44054e439adfc2128e93e652178c6df42ee9159.zip | |
Find called module in Icall proof
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 21de6bd..9c5804d 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -87,7 +87,7 @@ Inductive tr_code (ge : RTL.genv) (c : RTL.code) (pc : RTL.node) (stmnts : datap | tr_code_call : forall sig fn args dst n, c!pc = Some (RTL.Icall sig (inr fn) args dst n) -> - (exists fd, rtl_find_func ge fn = Some (AST.Internal fd)) -> + (exists fd, find_func ge fn = Some (AST.Internal fd)) -> Z.pos n <= Int.max_unsigned -> (exists pc2 fn_rst fn_return fn_finish fn_params, |