With CBMC it's even easier. You don't need magic comments in foreign languages to prove linked lists, arrays, graphs, trees, hashtables, ... If you need to formalize contracts you do it in C, but rarely need it

http://www.cprover.org/cbmc/