[Fulminate] Generate functions for spec-checking

[rbanerjee20]

TODO: generate functions for each pre- and post-condition and loop invariant, and call these so that only a single line gets injected at function entry, exit and at loop conditions.

Requires the correct ghost state to be returned so it can be used later.