-
Notifications
You must be signed in to change notification settings - Fork 76
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add termination analysis success messages for loop bounds #1580
Conversation
Although this doesn't really explain the case from #1577: ./goblint --conf conf/svcomp.json --set ana.specification ../sv-benchmarks/c/properties/termination.prp ../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c --html --enable dbg.termination-bounds outputs (among other things)
The maximum bound 2147483896 is one lower, but that's just because we activate congruence analysis we can rule out 2147483897 (which is is excluded because it is odd). |
Regarding our discussion at today's Gobcon, whether it suffices to exclude that the abstract value for the artificially introduced loop counter variable is top: As for an artificial loop counter As a side note, the artificial loop counter should have an |
… but it should never wrap around, though :-) HelmutAm 29.10.2024 um 14:59 schrieb Julian Erhard ***@***.***>:
Regarding our discussion at today's Gobcon, whether it suffices to exclude that the abstract value for the artificially introduced loop counter variable is top: As for an artificial loop counter i it is ensured that i is incremented by one in each iteration, if the loop is ounbounded, i will receive every possible value (even if any finite number of unrollings is performed).
As a side note, the artificial loop counter should have an unsigned integer type, and thus should not be affected by the analyzer assuming that signed overflows do not happen.
—Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That will hopefully make debugging easier in the future. Nice addition!
Closes #1577.
These are disabled by default, but can be enabled with
dbg.termination-bounds
.Also cleans up the implementation of
LoopTermination.special
in general (pointlesselse ()
, too widetry
scope, annoying half-indentation).