-
Notifications
You must be signed in to change notification settings - Fork 277
Correctly truncate error traces #4162
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
Correctly truncate error traces #4162
Conversation
00dba5d
to
6ae7ad1
Compare
Though weirdly not in all build configurations, this is failing the "several-threads" test:
|
6ae7ad1
to
1a1ac2a
Compare
A condition was missing in identifying the assertion step. Fixed now. |
Produce message in a single place.
to be used in build_goto_trace to truncate traces.
to support - full trace for whole SSA - trace for a specific property - trace for the "first" failing property (behavior of stop-on-fail)
which is more readable.
The traces need to be correctly truncated so that the failing property comes last. The traces are printed in the same order as the properties are listed in the result report.
1a1ac2a
to
cbd61b2
Compare
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.
✔️
Passed Diffblue compatibility checks (cbmc commit: cbd61b2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100599878
Fixes a regression introduced in #3795:
If a single counterexample violates several properties then the traces need to be correctly truncated for each property and printed in the same order as the properties are reported.