diff options
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 5 | ||||
| -rw-r--r-- | kernel/byterun/dune | 4 |
2 files changed, 8 insertions, 1 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 2c0b580e24..40aaa5c021 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -21,6 +21,7 @@ #include <caml/alloc.h> #include <caml/memory.h> #include "coq_instruct.h" +#include "coq_arity.h" #include "coq_fix_code.h" #ifdef THREADED_CODE @@ -82,7 +83,9 @@ void init_arity () { /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ - arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0; + arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=-1; + for (int i = 0; i <= STOP; ++i) + if (arity[i] != arity2[i]) { printf("bad: %d\n", i); abort(); } } #endif /* THREADED_CODE */ diff --git a/kernel/byterun/dune b/kernel/byterun/dune index d3e2a2fa7f..a2484f79a7 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -14,3 +14,7 @@ (rule (targets coq_jumptbl.h) (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump)))) + +(rule + (targets coq_arity.h) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe arity)))) |