Add support for spec annotations

[sonmarcho]

It would be good to add the possibility of annotating the definitions with pre/post-conditions and even proof annotations.
This issue should be done after #63

[Nadrieril]

After #105, an annotation like

#[postcondition(*x == y)]
fn foo(&mut x, y) { ... }

will show up as a string "postcondition(*x == y)" in the function attributes. Can we do more than that on the charon side?