Make contract inference work with simple functions

[xldenis]

We support inference for closures, but another useful situation is 'dumb' getters and setters where the contract repeats the (short) function body. We should be able to specify those.

I feel like we could start with using this only on small (pure?) functions, but in principle anything without loops is game I suppose.

[jhjourdan]

One problem we will have with that is that we need to generate the coma code for these simple functions as part of the caller Why3 module (otherwise the inference can't work), and therefore we will need to re-prove the callee at each use. We should somehow have two odes when generating the coma code: one mode would emit everythin, and the other would only emit whatever is not behind an abstraction barrier.

[xldenis]

and therefore we will need to re-prove the callee at each use.

That's fine for things like getters and setters though. their contract is their body so its not increasing the amount of work to be done.