Replies: 6 comments 4 replies
-
Still relevant. We could really use the help. |
Beta Was this translation helpful? Give feedback.
-
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 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. |
Beta Was this translation helpful? Give feedback.
-
this is more appropriate as a discussion rather than an issue |
Beta Was this translation helpful? Give feedback.
-
I was about to suggest that you should talk to @yvizel , since he was the author of the previous code. Glad to see he joined the conversation :) |
Beta Was this translation helpful? Give feedback.
-
Hi.
Said function: #include "seahorn/seahorn.h" extern int nd(void); int main(void) {
} note: __hyper_post_gt(a) means that my post condition is a1>a2 |
Beta Was this translation helpful? Give feedback.
-
I'm not sure I understand the question. Can you be more specific what If this is a query for the CHC-solver, then, of course, CHC-solver needs a property to solve and query is needed. If your goal is only to generate the CHC system and not ask any questions of it, then the query is irrelevant. Otherwise, it depends on the property that you are encoding. The argument to the query is a nullary predicate that represent a basic block. The intended meaning is whether the basic block is reachable. You cannot use To debug interaction with z3, you can use For the second question, it is hard for me to answer it without seeing the CHCs that you generate. I cannot generate them myself either because I do not have access to your modifications. Hope this helps. I think, most likely reason, is that there is some misunderstanding and you are creating query (True) that is not supported and getting unknown as an error answer as a result. |
Beta Was this translation helpful? Give feedback.
-
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
Beta Was this translation helpful? Give feedback.
All reactions