aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGuillaume Melquiond2021-02-17 12:13:32 +0100
committerGuillaume Melquiond2021-02-19 11:17:27 +0100
commitd39a01caf4cbbc22cddbaa23234622b21412f058 (patch)
tree63a253ac874feba89dfad3415795f7dd42460f9a
parentab94a2a5dbe142d972d65a33d977e8e9f8d52f01 (diff)
Be less permissive with respect to nonsensical bytecode.
-rw-r--r--kernel/byterun/coq_fix_code.c7
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index f986095f59..20890a28dc 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -108,9 +108,7 @@ value coq_tcode_of_code (value code) {
opcode_t instr;
COPY32(&instr,p);
p++;
- if (instr < 0 || instr > STOP){
- instr = STOP;
- };
+ if (instr < 0 || instr > STOP) abort();
*q++ = VALINSTR(instr);
if (instr == SWITCH) {
uint32_t i, sizes, const_size, block_size;
@@ -127,8 +125,9 @@ value coq_tcode_of_code (value code) {
q++;
for(i=1; i<n; i++) { COPY32(q,p); p++; q++; };
} else {
- uint32_t i, ar;
+ int i, ar;
ar = arity[instr];
+ if (ar < 0) abort();
for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
}
}