Problems in error trace visualizer
1. Attribute tables takes only a half of screen, the rest is empty. It have to occupy all the space.
2. It is unclear which assertion in ldv_unregister_class(); is failed. There are three shown in green, while the first one is passed and the second is failed. If the second is red, it would be much more usable.
3. The third line with __VERIFIER_error(); is useless. and it has the same comment as the second one. Should we remove it completely?
Updated by Evgeny Novikov over 3 years ago
- The rest half of screen is intended for associated marks. But there is not any associated mark yet and you were not an expert for corresponding job to have a button to create them. Something (like my previous sentence) should be shown in such cases.
- Normally users shouldn't click on notes (blue text) and warnings (red text). They should click on corresponding rectangles like for the rest of error trace lines. But this is impossible due to #7103. Clicking on notes and warnings should be use to get more details about implementation of model functions that is hidden by default. As for your question warnings (red text) show assertions violated. They are automatically propagated from the __VERIFIER_error() to nearest model function calls and they correspond to notes that precede __VERIFIER_error(). I don't see much sense in the requested improvement since those people who do need such the details should understand what are they while other users will no experience such the problems at all.
- Ditto it is a detail that is normally hidden by default from the most of users.
BTW, implementation of ldv_assert() will be considerably changed when we will switch to so called multi-aspect verification. So it is better to postpone this issue anyway.