docs: @Override
    protected void onMethodExit(int opcode) {
      if ((withPreconditions || withPostconditions || withInvariants)
          && opcode != ATHROW) {
        if (withPostconditions || withInvariants) {
          Label skip = enterBusySection();
  
          if (withPostconditions) {
            Type returnType = Type.getReturnType(methodDesc);
            int returnIndex = -1;
            if (returnType.getSort() != Type.VOID) {
              if (returnType.getSize() == 2) {
                dup2();
              } else {
                dup();
              }
              returnIndex = newLocal(returnType);
              storeLocal(returnIndex);
            }
            invokeCommonPostconditions(ContractKind.POST, oldValueLocals,
                                       returnIndex);
          }
  
          if (withInvariants && !statik) {
            invokeInvariants();
          }
  
          leaveBusySection(skip);
        }
        leaveContractedMethod();
      }
    }