Project

General

Profile

Feature #10751

Add comments of level 2 for rather important places and actions within environment models

Added by Evgeny Novikov 3 months ago. Updated 2 months ago.

Status:
Closed
Priority:
High
Category:
Environment models
Target version:
Start date:
03/13/2021
Due date:
% Done:

0%

Estimated time:
Published in build:

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 issues

Related to Klever - Feature #10753: Allow to show/hide comments of particular levelsNewVladimir Gratinskiy03/13/2021

Actions
Related to Klever - Feature #8131: Do not introduce notes when assertions are satisfiedClosedEvgeny Novikov04/21/2017

Actions
#1

Updated by Evgeny Novikov 3 months ago

  • Related to Feature #10753: Allow to show/hide comments of particular levels added
#2

Updated by Evgeny Novikov 3 months ago

  • Description updated (diff)
#3

Updated by Evgeny Novikov 3 months ago

  • 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.

#4

Updated by Evgeny Novikov 3 months ago

  • Status changed from Resolved to Open

CI demonstrated a tremendous number of regressions to be fixed.

#5

Updated by Evgeny Novikov 2 months ago

  • 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.

#6

Updated by Evgeny Novikov 2 months ago

  • 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();

#7

Updated by Evgeny Novikov 2 months ago

  • Related to Feature #8131: Do not introduce notes when assertions are satisfied added

Also available in: Atom PDF