diff options
| -rw-r--r-- | src/hls/HTLgenproof.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 46d70c2..4405a93 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -203,6 +203,7 @@ Inductive match_states (ge : RTL.genv) : RTL.state -> HTL.state -> Prop := (TF : tr_module ge f m) (MF : match_frames ge mid mem rtl_stk htl_stk) (SP_BASE : nil_stack_base_sp rtl_stk sp blk \/ stack_base_sp rtl_stk blk) + (INIT_CALL_NO_ARGS : rtl_stk = nil -> rtl_args = nil) (ARGS_BASED : Forall (fun a => stack_based a blk) rtl_args) (MARGS : list_forall2 val_value_lessdef rtl_args htl_args), match_states ge |