Handling k-safety property

[Nivous]

Hi.
I am looking to implement k-safety property using seahorn.
For that I am trying to think what is the best way to introduce the pre \ post conditions in my program.
I am not sure at all what I should use as even from a technical point of view, I am not sure how the compiler would handle those function calls and how should I implement them.
Have you considered implementing something like that and maybe have a suggestion on how to begin?

Any help would be appreciated,
Niv

[Nivous]

Still relevant. We could really use the help.

[agurfinkel]

Sorry, your email came when most of the team is on vacation / travel. The best way to communicate pre- and post-conditions is with special function calls. In the same way we communicate assumptions using verifier.assume call.

It would work best if you can break your desired solution into a series of examples. If we can see what you are doing, we might be able to help.

There was a project in the past that used self-composition to convert k-safety into safety and solve it with seahorn. I don't believe it was ever merged in and seahorn has changed substantially since that time.