code: private static FDBigInteger valueOfPow2(int p2) {
          int wordcount = p2 >> 5;
          int bitcount = p2 & 0x1f;
          return new FDBigInteger(new int[]{1 << bitcount}, wordcount);
      }
docs: /*@
  @ requires p2 >= 0;
  @ assignable \nothing;
  @ ensures \result.value() == pow52(0, p2);
  @