diff options
| -rw-r--r-- | kernel/byterun/coq_interp.c | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 0dd3b653a..a2ece57c4 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1238,10 +1238,21 @@ value coq_interprete /* higher level shift (does shifts and cycles and such) */ uint32 shiftby; shiftby = uint32_of_value(accu); + if (shiftby > 31) { + if (shiftby < 62) { + *sp++; + accu = (value)((((*sp++)^1) << (shiftby - 31)) | 1); + } + else { + accu = (value)(1); + } + } + else{ /* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */ accu = (value)(((*sp++)^1) << shiftby); /* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */ accu = (value)((accu | (((uint32)(*sp++)) >> (31-shiftby)))|1); + } Next; } |