Project

General

Profile

Feature #10751

Updated by Evgeny Novikov over 3 years ago

Among these places and actions are the following ones: 
 * Functions returning non-deterministic values. 
 * __VERIFIER_assume(). 
 * Inline Assembler stubs. 
 * External allocated data. 

 Some trial 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.

Back