code: @Requires({
      "kind != null",
      "kind.isPostcondition()",
      "oldLocals != null",
      "extraIndex >= -1"
    })
    protected void invokeCommonPostconditions(ContractKind kind,
        List<Integer> oldLocals, int extraIndex) {
      MethodContractHandle h =
          contracts.getMethodHandle(kind, methodName, methodDesc,
                                    getPostDescOffset(oldLocals, extraIndex));
      if (h == null) {
        return;
      }
  
      MethodNode contractMethod = injectContractMethod(h);
  
      if (!statik) {
        loadThis();
      }
      loadArgs();
  
      if (extraIndex != -1) {
        loadLocal(extraIndex);
      }
  
      for (Integer oldIndex : oldLocals) {
        loadLocal(oldIndex);
      }
  
      invokeContractMethod(contractMethod);
    }
docs: Injects calls to postcondition (or exceptional postcondition)
  contract methods. Postcondition contract methods get called with,
  in this order:
  
  <ul>
  <li>the {@code this} pointer, if any;
  <li>the original method's parameters;
  <li>the return value, if the original method is not void, or the
  exception object;
  <li>and old values if any.
  </ul>
  
  @param kind the kind of postcondition contract to invoke
  @param oldLocals a list of old value variables
  @param extraIndex the index of the local variable that holds the
  return value, or exception object, of the method, or -1 if none