docs: @Requires({
      "contextLocal >= 0",
      "checkInvariantsLocal >= 0"
    })
    @Ensures("result != null")
    protected Label enterBusySection() {
      Label skip = new Label();
      loadLocal(contextLocal);
      invokeVirtual(CONTRACT_CONTEXT_TYPE, TRY_ENTER_CONTRACT_METHOD);
      ifZCmp(EQ, skip);
      return skip;
    }