diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-10-07 18:23:59 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-10-07 18:23:59 +0100 |
| commit | aa3740d8ce01b813869609b4f971133c3d5d4bcd (patch) | |
| tree | 1fc0406d000749447766cc23fe5317f13e047ece /src/hls | |
| parent | 0c26ff7eb91d694824fd8450f56ae90a4e043923 (diff) | |
| download | vericert-aa3740d8ce01b813869609b4f971133c3d5d4bcd.tar.gz vericert-aa3740d8ce01b813869609b4f971133c3d5d4bcd.zip | |
Maintain that initial call does not have arguments
Diffstat (limited to 'src/hls')
| -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 |