In my opinion SPLint (http://splint.org/) would be a nice approach. It is a way ...

In my opinion SPLint (http://splint.org/) would be a nice approach. It is a way to specify ownership semantics, inout parameters etc., but also allows to specify arbitrary pre- and postconditions. It works by annotating whole functions, their parameters, types and variables. These are then checked by calling splint on the codebase, you can also opt out of several checks by flags or using the preprocessor.

  - nullability: /*@null@*/
  - in/out parameter (default in): /*@inout@*/, /*@out@*/
  - ownership: /*@only@*/, /*@temp@*/, /*@shared@*/, /*@refcounted@*/
  - also supports partial defined parameters
  - allows to be introduced gradually in the codebase

Example from the documentation:

  void * /*@alt char * @*/
  strcpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2)
          /*@modifies *s1@*/
          /*@requires maxSet(s1) >= maxRead(s2) @*/
          /*@ensures maxRead(s1) == maxRead (s2) @*/;

My main problem was that it was annoying to add to a project, but that is only because you need to specify ownership semantic, not because of the syntax which is short and readable, and that the program is sometimes crashing and there doesn't seem to be active development.