diff options
| author | Guillaume Melquiond | 2021-03-25 12:03:40 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-03-26 15:18:28 +0100 |
| commit | ae819deb38c3a962e3badf020705c3d0c6c84e67 (patch) | |
| tree | f269e1968fd1f6420b4dc459a5d6e30e6a1726d9 /kernel/vmbytecodes.mli | |
| parent | 6d7fdaf8484da81993958d339e411d8e3b1a38c1 (diff) | |
Make it more obvious when the calling convention of APPLY changes.
Despite their names, APPLY1 to APPLY4 are completely different from
APPLY(n) with n = 1 to 4. Indeed, the latter assumes that the return
address was already pushed on the stack, before the arguments were. On the
other hand, APPLY1 to APPLY4 insert the return address in the middle of
the already pushed arguments.
Diffstat (limited to 'kernel/vmbytecodes.mli')
| -rw-r--r-- | kernel/vmbytecodes.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli index eeca0d2ad1..d9e2d91177 100644 --- a/kernel/vmbytecodes.mli +++ b/kernel/vmbytecodes.mli @@ -30,6 +30,7 @@ type instruction = | Kpush (** sp = accu :: sp *) | Kpop of int (** sp = skipn n sp *) | Kpush_retaddr of Label.t (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *) + | Kshort_apply of int (** number of arguments (arguments on top of stack) *) | Kapply of int (** number of arguments (arguments on top of stack) *) | Kappterm of int * int (** number of arguments, slot size *) | Kreturn of int (** slot size *) |