diff options
| author | Guillaume Melquiond | 2021-02-17 12:09:00 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-02-19 11:17:26 +0100 |
| commit | c7bbe4729dc53ddf3a02a7ae3816ec3c146d452e (patch) | |
| tree | 18f2e1a463ae9c4106fbfe4703c2098ff740cf20 /kernel/byterun/coq_fix_code.c | |
| parent | bbb9876da3093658c9eca206a585b045ed258220 (diff) | |
Add a file coq_arity.h generated by genOpcodeFiles.ml.
This avoids forgetting to add opcodes to coq_fix_code.c, and thus prevents
arities being mistakenly set to zero.
Diffstat (limited to 'kernel/byterun/coq_fix_code.c')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 5 |
1 files changed, 4 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 */ |