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 ++++- kernel/byterun/dune | 4 ++++ 2 files changed, 8 insertions(+), 1 deletion(-) (limited to 'kernel/byterun') 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 */ 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)))) -- cgit v1.2.3