docs: @Override
    protected void onMethodEnter() {
      if (withPreconditions || withPostconditions || withInvariants) {
        enterContractedMethod();
  
        if (withPostconditions) {
          allocateOldValues(ContractKind.OLD, oldValueLocals);
          allocateOldValues(ContractKind.SIGNAL_OLD, signalOldValueLocals);
        }
  
        mark(methodStart);
  
        Label skip = enterBusySection();
  
        if (withInvariants && !statik && !isConstructor && !isStaticInit) {
          invokeInvariants();
        }
  
        if (withPreconditions) {
          invokePreconditions();
        }
  
        if (withPostconditions) {
          invokeOldValues(ContractKind.OLD, oldValueLocals);
          invokeOldValues(ContractKind.SIGNAL_OLD, signalOldValueLocals);
        }
  
        leaveBusySection(skip);
      }
    }