Add Linter Checks to Gobra

[herzamos]

TODO

[jcp19]

The conclusion of this work is that we should strengthen Gobra with stronger checks already to prevent common specification errors. That are things that we can easily do in the context of Gobra itself, like:

• reject non-heap dependent expressions occurring in old expressions
• reject permission amounts in places where they are not consequential, like specs and bodies of pure functions
• reject some form of redundant pre/postconditions
• reject preconditions that trivially evaluate to false but are not the expression false. in these cases, it is likely the dev meant sth else

[jcp19]

Other useful checks include rejecting abstract functions and methods without marking them as trusted (which makes it easy to textually enumerate all the places where assumptions are introduced) and to reject unused variables (especially in ghost code), which the go compiler does by default