Merge branch 'v8.5' into trunk

1 files changed, 4 insertions, 3 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0a121dc32e..399fa843f1 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1252,16 +1252,17 @@ value coq_interprete
         shiftby = uint32_of_value(accu);
         if (shiftby > 31) {
           if (shiftby < 62) {
-            *sp++;
-	    accu = (value)((((*sp++)^1) << (shiftby - 31)) | 1);
+            sp++;
+	    accu = (value)(((((uint32_t)*sp++)^1) << (shiftby - 31)) | 1);
           }
           else {
+            sp+=2;
             accu = (value)(1);
           }
 	}
         else{
         /* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */
-        accu = (value)(((*sp++)^1) << shiftby);
+	  accu = (value)((((uint32_t)*sp++)^1) << shiftby);
         /* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */
         accu = (value)((accu | (((uint32_t)(*sp++)) >> (31-shiftby)))|1);
 	}