Project

General

Profile

Actions

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.

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 2 (0 open2 closed)

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

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

Actions
Actions

Also available in: Atom PDF