diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-27 11:25:39 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-14 16:21:19 +0100 |
commit | 745696124240963616a38f41b1a20f199646c5dc (patch) | |
tree | 4ee26cc79bbc88fc0ec789981acb47a0e93722bb /kernel/cbytecodes.mli | |
parent | da659eeeb413c488f5efae0269c5d37837c62dc2 (diff) |
Factorize the relocations in the on-disk VM representation.
Instead of using a linear representation, we simply use a table that maps
every kind of relocation to the list of positions it needs to be applied to.
Diffstat (limited to 'kernel/cbytecodes.mli')
-rw-r--r-- | kernel/cbytecodes.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 5d37a5840..bf2e462e8 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -41,6 +41,12 @@ type reloc_table = (tag * int) array type annot_switch = {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} +val eq_structured_constant : structured_constant -> structured_constant -> bool +val hash_structured_constant : structured_constant -> int + +val eq_annot_switch : annot_switch -> annot_switch -> bool +val hash_annot_switch : annot_switch -> int + module Label : sig type t = int |