Does Verifast support multiple postconditions?

[Sophie Lathouwers]

Hi!

I am trying to verify some examples with Verifast and came across the problem that as soon as a I split a postcondition into two postconditions, Verifast raised a parse error (Parse error: The number, kind, or order of specification clauses is incorrect. Expected: nonghost_callers_only clause (optional), function type clause (optional), contract (optional), terminates clause (optional).).

Should I conclude from this that Verifast wants me to write all postconditions in a single ensures clause (i.e. it is not possible to write multiple ensures clauses for a single method)?

Kind regards,

Sophie Lathouwers