docs: @Requires({
      "bytecode != null",
      "contractBytecode != null"
    })
    @Ensures("result != null")
    public byte[] transformWithContracts(byte[] bytecode, byte[] contractBytecode)
        throws IllegalClassFormatException {
      try {
        ContractAnalyzer contracts =
            extractContracts(new ClassReader(contractBytecode));
        return instrumentWithContracts(bytecode, contracts);
      } catch (Throwable t) {
        /* If the class file contains errors, ASM will just crash. */
        IllegalClassFormatException e = new IllegalClassFormatException();
        e.initCause(t);
        throw e;
      }
    }