src/java.base/share/classes/jdk/internal/math/FDBigInteger.java

*** 113,123 ****
  
      // Maximum size of cache of powers of 5 as FDBigIntegers.
      private static final int MAX_FIVE_POW = 340;
  
      // Cache of big powers of 5 as FDBigIntegers.
!     private static final FDBigInteger POW_5_CACHE[];
  
      // Initialize FDBigInteger cache of powers of 5.
      static {
          POW_5_CACHE = new FDBigInteger[MAX_FIVE_POW];
          int i = 0;
--- 113,123 ----
  
      // Maximum size of cache of powers of 5 as FDBigIntegers.
      private static final int MAX_FIVE_POW = 340;
  
      // Cache of big powers of 5 as FDBigIntegers.
!     private static final FDBigInteger[] POW_5_CACHE;
  
      // Initialize FDBigInteger cache of powers of 5.
      static {
          POW_5_CACHE = new FDBigInteger[MAX_FIVE_POW];
          int i = 0;
*** 145,155 ****
  
      // Constant for casting an int to a long via bitwise AND.
      private static final long LONG_MASK = 0xffffffffL;
  
      //@ spec_public non_null;
!     private int data[];  // value: data[0] is least significant
      //@ spec_public;
      private int offset;  // number of least significant zero padding ints
      //@ spec_public;
      private int nWords;  // data[nWords-1]!=0, all values above are zero
                   // if nWords==0 -> this FDBigInteger is zero
--- 145,155 ----
  
      // Constant for casting an int to a long via bitwise AND.
      private static final long LONG_MASK = 0xffffffffL;
  
      //@ spec_public non_null;
!     private int[] data;  // value: data[0] is least significant
      //@ spec_public;
      private int offset;  // number of least significant zero padding ints
      //@ spec_public;
      private int nWords;  // data[nWords-1]!=0, all values above are zero
                   // if nWords==0 -> this FDBigInteger is zero
*** 415,425 ****
       @ requires 0 < bitcount && bitcount < 32 && anticount == 32 - bitcount;
       @ requires src.length >= idx && result.length > idx;
       @ assignable result[*];
       @ ensures AP(result, \old(idx + 1)) == \old((AP(src, idx) + UNSIGNED(prev) << (idx*32)) << bitcount);
       @*/
!     private static void leftShift(int[] src, int idx, int result[], int bitcount, int anticount, int prev){
          for (; idx > 0; idx--) {
              int v = (prev << bitcount);
              prev = src[idx - 1];
              v |= (prev >>> anticount);
              result[idx] = v;
--- 415,425 ----
       @ requires 0 < bitcount && bitcount < 32 && anticount == 32 - bitcount;
       @ requires src.length >= idx && result.length > idx;
       @ assignable result[*];
       @ ensures AP(result, \old(idx + 1)) == \old((AP(src, idx) + UNSIGNED(prev) << (idx*32)) << bitcount);
       @*/
!     private static void leftShift(int[] src, int idx, int[] result, int bitcount, int anticount, int prev){
          for (; idx > 0; idx--) {
              int v = (prev << bitcount);
              prev = src[idx - 1];
              v |= (prev >>> anticount);
              result[idx] = v;