Feature #10751
closed
Add comments of level 2 for rather important places and actions within environment models
Added by Evgeny Novikov over 3 years ago.
Updated over 3 years ago.
Category:
Environment models
Description
Among these places and actions are the following ones:
- Functions returning non-deterministic values.
- __VERIFIER_assume().
- Inline Assembler stubs.
- External allocated data.
Some support of comments of level 2 in VRP will be necessary since now it supports just level 0 and level 1.
BTW, comments of level 2 will not be shown by Bridge by default. Moreover, they will not influence error trace patterns in marks.
- Related to Feature #10753: Allow to show/hide comments of particular levels added
- Description updated (diff)
- Status changed from New to Resolved
I did this in branch notes-level-2. Also, I had to get rid of a very old workaround that was used because of "ASSERT" comments were used on normal paths.
- Status changed from Resolved to Open
CI demonstrated a tremendous number of regressions to be fixed.
- Status changed from Open to Resolved
After fixes CI passed tests. Unfortunately, invocation of __VERIFIER_assume() through the intermediate function adding a note resulted in too considerable changes in verification results (Pavel investigated that this is likely due to the solver considers the corresponding formulas rather differently). That's why I had to revert this change and to add the note in a cheating way.
- Status changed from Resolved to Closed
Tests passed, so, I merged the branch to master in fd6a483c8. Please, note, that all out-of-tree requirement specifications using ldv_assert() should be adjusted so that they should not pass any value/expression to this function while they should invoke it just when the corresponding value/expression is not true. Besides, there should be comment ASSERT like in the following example:
if (ldv_iomem != 0)
/* ASSERT io-memory should be released at exit */
ldv_assert();
- Related to Feature #8131: Do not introduce notes when assertions are satisfied added
Also available in: Atom
PDF