How to set the boogie keep on verify all the asserts but not stop when it finds some asserts not holds #457
-
If boogie returns as "Boogie program verifier finished with 1 verified, 0 errors" I know that all the asserts points had been verified and I feel safe. But when it reports that some asserts might not be hold. It seems that it doesn't check all the asserts point. |
Beta Was this translation helpful? Give feedback.
Replies: 10 comments 37 replies
-
Please provide an example where you see this behavior.
|
Beta Was this translation helpful? Give feedback.
-
Could you try to run boogie with the option /errorLimit:0 and report back? |
Beta Was this translation helpful? Give feedback.
-
It is possible to just run the Boogie verifier. The Boogie equivalent of your first program is the following:
I have added your assert in the loop body and also added a loop invariant. I checked that |
Beta Was this translation helpful? Give feedback.
-
The installation instructions for Boogie are here: https://github.com/boogie-org/boogie. |
Beta Was this translation helpful? Give feedback.
-
I am going through some of your comments above. It seems like you have some static analysis on the side. This analysis is able to guarantee some facts. You want to provide those facts in the Boogie program in such a way that: (1) Boogie does not attempt to reverify those facts, and (2) Boogie uses those facts in its verification of other facts. Did I understand your intention correctly? |
Beta Was this translation helpful? Give feedback.
-
Is there a solution for the original question, i.e., "How to set the boogie to keep on verifying all the asserts but not stop when it finds some asserts not hold"? E.g.:
Running boogie on the above code returns
I would like it to report an error on line 3 as well |
Beta Was this translation helpful? Give feedback.
-
I see this option:
|
Beta Was this translation helpful? Give feedback.
-
I was looking into this myself just the other day. So let me explain my findings and my understanding of why you are seeing this behavior.
Now, even when you enable I think that is what is happening in your example as well. I guess the semantics you were looking for is that when an assertion fails, Boogie simply "deletes" it and tries to find more violations of other assertions. Coincidentally, that is the semantics I wanted as well. But it seems that such semantics when looking for multiple assertion failures is not. currently implemented in Boogie. |
Beta Was this translation helpful? Give feedback.
-
@Luweicai : you may have misunderstood the explanation by @zvonimir. He provided his explanation in terms of the SMT query but you interpreted it at the level of the Boogie program. Here is another explanation. Intuitively, Boogie proves each assertion, one at a time, in a variation of the program in which all previously considered asserts are converted into assumes. Consider the latest program you included:
First, a violation of
Boogie finds no error and finishes. Now, let us consider the other program you included:
Once
which does not have any assertion failures. |
Beta Was this translation helpful? Give feedback.
-
Hi, @shazqadeer .
This is different from my goal. I use boogie to automatically verify programs that contain several check points (these check point likes checking I add the loop invariants into the programs to help boogie. Because without the loop invariant boogie will get the wrong result of many satisfied check points which in loops. I have a algorithm to automatically add loop invariants that help verify the check points in loops. However, I can not switch these loop invaraints from form of |
Beta Was this translation helpful? Give feedback.
I am going through some of your comments above. It seems like you have some static analysis on the side. This analysis is able to guarantee some facts. You want to provide those facts in the Boogie program in such a way that: (1) Boogie does not attempt to reverify those facts, and (2) Boogie uses those facts in its verification of other facts. Did I understand your intention correctly?