summaryrefslogtreecommitdiff
path: root/kernel/byterun/coq_fix_code.c
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
commita4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch)
tree26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /kernel/byterun/coq_fix_code.c
parent164c6861860e6b52818c031f901ffeff91fca16a (diff)
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'kernel/byterun/coq_fix_code.c')
-rw-r--r--kernel/byterun/coq_fix_code.c8
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 29e33d34..d5feafbf 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -57,7 +57,7 @@ void init_arity () {
arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]=
arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=
arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=
- arity[BRANCH]=arity[ISCONST]= 1;
+ arity[BRANCH]=arity[ISCONST]=arity[ENSURESTACKCAPACITY]=1;
/* instruction with two operands */
arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
arity[ARECONST]=arity[PROJ]=2;
@@ -79,7 +79,7 @@ void * coq_stat_alloc (asize_t sz)
value coq_makeaccu (value i) {
code_t q;
- code_t res = coq_stat_alloc(8);
+ code_t res = coq_stat_alloc(2 * sizeof(opcode_t));
q = res;
*q++ = VALINSTR(MAKEACCU);
*q = (opcode_t)Int_val(i);
@@ -91,13 +91,13 @@ value coq_pushpop (value i) {
int n;
n = Int_val(i);
if (n == 0) {
- res = coq_stat_alloc(4);
+ res = coq_stat_alloc(sizeof(opcode_t));
*res = VALINSTR(STOP);
return (value)res;
}
else {
code_t q;
- res = coq_stat_alloc(12);
+ res = coq_stat_alloc(3 * sizeof(opcode_t));
q = res;
*q++ = VALINSTR(POP);
*q++ = (opcode_t)n;