From c7bbe4729dc53ddf3a02a7ae3816ec3c146d452e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 17 Feb 2021 12:09:00 +0100 Subject: 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. --- kernel/byterun/coq_fix_code.c | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kernel/byterun/coq_fix_code.c') 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 #include #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 */ -- cgit v1.2.3