diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-27 11:21:35 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-27 11:21:35 +0200 |
| commit | 62b0708ebfda01e377c4e6e229be4388a96cbecc (patch) | |
| tree | 33ce6dbcc9680ce79f0c77c7c4c1f9a5468555ae /kernel/byterun | |
| parent | 3cf7a09799982924453df29b3bb4d081a0e089b4 (diff) | |
Fix some ill-typed debugging code in the VM.
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 0ab9f89ff..ddbde9d38 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -77,9 +77,11 @@ sp is a local copy of the global variable extern_sp. */ #ifdef _COQ_DEBUG_ # define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s) # define print_int(i) /*if (drawinstr)*/ printf("%d\n",i) +# define print_lint(i) /*if (drawinstr)*/ printf("%ld\n",i) # else # define print_instr(s) # define print_int(i) +# define print_lint(i) #endif /* GC interface */ @@ -795,12 +797,12 @@ value coq_interprete if (Is_block(accu)) { long index = Tag_val(accu); print_instr("block"); - print_int(index); + print_lint(index); pc += pc[(sizes & 0xFFFFFF) + index]; } else { long index = Long_val(accu); print_instr("constant"); - print_int(index); + print_lint(index); pc += pc[index]; } Next; @@ -957,7 +959,7 @@ value coq_interprete sp -= nargs; for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); *--sp = accu; - print_int(nargs); + print_lint(nargs); coq_extra_args = nargs; pc = Code_val(coq_env); goto check_stacks; |