aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytecodes.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-10-26 13:07:34 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-10-26 13:07:34 +0200
commit4a82de3b5b9d4a1a0830291b5b9a485bf2a16ded (patch)
tree15ff7464cc5a250fbb6ed2a10887d34cfb62a8a4 /kernel/cbytecodes.ml
parent95429d01a8f47f5f9d1ecee3b452d920e1e1af22 (diff)
parent2290dbb9c95b63e693ced647731623e64297f5c8 (diff)
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'kernel/cbytecodes.ml')
-rw-r--r--kernel/cbytecodes.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 8d4de523a..810c34699 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -43,7 +43,7 @@ type structured_constant =
type reloc_table = (tag * int) array
type annot_switch =
- {ci : case_info; rtbl : reloc_table; tailcall : bool}
+ {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
module Label =
struct
@@ -87,6 +87,7 @@ type instruction =
| Ksequence of bytecodes * bytecodes
| Kproj of int * Constant.t (* index of the projected argument,
name of projection *)
+ | Kensurestackcapacity of int
(* spiwack: instructions concerning integers *)
| Kbranch of Label.t (* jump to label *)
| Kaddint31 (* adds the int31 in the accu
@@ -264,6 +265,8 @@ let rec pp_instr i =
| Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p
+ | Kensurestackcapacity size -> str "growstack " ++ int size
+
| Kaddint31 -> str "addint31"
| Kaddcint31 -> str "addcint31"
| Kaddcarrycint31 -> str "addcarrycint31"