docs: @Ensures({
      "contextLocal >= 0",
      "checkInvariantsLocal >= 0"
    })
    protected void enterContractedMethod() {
      contextLocal = newLocal(CONTRACT_CONTEXT_TYPE);
      checkInvariantsLocal = newLocal(Type.BOOLEAN_TYPE);
      invokeStatic(CONTRACT_RUNTIME_TYPE, GET_CONTEXT_METHOD);
      dup();
      storeLocal(contextLocal);
      if (statik) {
        loadThisClass();
      } else {
        loadThis();
      }
      invokeVirtual(CONTRACT_CONTEXT_TYPE, TRY_ENTER_METHOD);
      storeLocal(checkInvariantsLocal);
    }