Feature #6781
closedMore user-friendly error traces
0%
Description
Sometimes we can enhance error traces representation a bit. I assume to collect all such cases within the given issue and then fix them. Note that corresponding enhancements shouldn't necessarily belong to any particular static verifier.
Updated by Evgeny Novikov over 8 years ago
Replace expressions like:
!(tmp == 0)
with:
tmp != 0
Strongly requested by Alexey.
Updated by Evgeny Novikov over 7 years ago
- Assignee set to Evgeny Novikov
- Priority changed from Normal to Urgent
No doubt that this should be done at last. Please, report more issues here (do not report issues related with environment models and rule specifications - there should be separate topics).
Updated by Evgeny Novikov over 7 years ago
- Priority changed from Urgent to Immediate
One more useful pattern that will fire in several places is the following:
... = aux_func([arg1, ...]);
T tmp;
tmp = func([arg1, ...]);
return tmp;
where the function aux_func() definition follows some specific comment. It can be simply and safely replaced with:
... = func([arg1, ...]);
Of course argument names for function func() should be translated to the ones for function aux_func(). Besides any extra white spaces and auxiliary braces shouldn't be treated.
Updated by Evgeny Novikov over 7 years ago
One more pattern that is very similar to the previous one is:
T tmp;
tmp = func([arg1, ...]);
return tmp;
that can be replaced with:
return func([arg1, ...]);
Updated by Evgeny Novikov over 7 years ago
- Status changed from New to Resolved
The witness format we are using for various tasks (simplifications, visualization, error traces comparison, etc.) as well as all requested in this issue were implemented in branch new_witness_format. It will be merged to master when all other related features will be implemented and tested.
Updated by Evgeny Novikov over 7 years ago
- Status changed from Resolved to Open
- Replace
"!(... </> ...)" with "... >/< ...".
- Replace "& ..." with "&...".
- Match the following pattern:
... tmp...; ... tmp... = func(...); ... tmp... ...;
and replace it with:... func(...) ...;
Updated by Evgeny Novikov over 7 years ago
- Status changed from Open to Resolved
Everything was eventually done in 4ea19c5.
Updated by Evgeny Novikov over 7 years ago
- Status changed from Resolved to Open
d6024ca - temporarily disable advanced simplifications since there are several open issues in them.
Updated by Evgeny Novikov over 7 years ago
In commit:9afbcbc to better-unsafes-and-marks there is a final version of the algorithms for removing temporary variables and auxiliary functions as well as some new and improved existing small simplifications.
The only thing to do is to think how to represent switches leading to large sequences of assumes (in particular this breaks a bit the latest version of the algorithm for removing temporary variables since it results in incorrect error trace with partially removed temporary variables in switches). How it is better to replace sequences like:
assume(x != A) assume(x != B) ... assume(x == Z)
I think that introducing huge boolean formula isn't a good idea.
Updated by Evgeny Novikov over 7 years ago
- Status changed from Open to Closed
- Priority changed from Immediate to Urgent
After comments were added to generated environment models, code without such the comments is considered auxiliary and completely removed from error traces. That is why the most of switches disappear and this doesn't hurt much. Any way I would like to have separate issues describing other useful improvements in error traces representation.