The attribute language seems a little clunky in its current form (although apparently it's an upcoming C2X standard). The idea of separation logic applied to these problems is promising though.

If you want something you can use with C code today, that has had many applications and integrates a little better IMO, then see Frama-C, the open source platform for extensible C verification:

https://frama-c.com/