code: public FDBigInteger multBy10() {
          if (nWords == 0) {
              return this;
          }
          if (isImmutable) {
              int[] res = new int[nWords + 1];
              res[nWords] = multAndCarryBy10(data, nWords, res);
              return new FDBigInteger(res, offset);
          } else {
              int p = multAndCarryBy10(this.data, this.nWords, this.data);
              if (p != 0) {
                  if (nWords == data.length) {
                      if (data[0] == 0) {
                          System.arraycopy(data, 1, data, 0, --nWords);
                          offset++;
                      } else {
                          data = Arrays.copyOf(data, data.length + 1);
                      }
                  }
                  data[nWords++] = p;
              } else {
                  trimLeadingZeros();
              }
              return this;
          }
      }
docs: /*@
  @ requires this.value() == 0;
  @ assignable \nothing;
  @ ensures \result == this;
  @
  @  also
  @
  @ requires this.value() > 0 && this.isImmutable;
  @ assignable \nothing;
  @ ensures \result.value() == \old(this.value() * 10);
  @
  @  also
  @
  @ requires this.value() > 0 && !this.isImmutable;
  @ assignable this.nWords, this.data, this.data[*];
  @ ensures \result == this;
  @ ensures \result.value() == \old(this.value() * 10);
  @