<div><div>Our framework verifies individual modules independently on other modules</div><div>and the kernel. For each module it generates a model of its environment</div><div>on the base of specifications. For instance, these specifications</div><div>describe an order in which callbacks should be invoked and arguments to</div><div>be passed to these callbacks. The framework includes specifications for</div><div>most frequently used types of drivers like USB, PCI, TTY, I2C and so on,</div><div>but these specifications are not always precise. In the given case we</div><div>need to refine the TTY specification so that it will restrict those</div><div>values that can be passed to the install callback of tty_operations. At</div><div>the moment it assumes that tty->index may have any value of the integer</div><div>type.</div><div> </div><div>You can visit https://forge.ispras.ru/projects/klever for more details.</div></div><div> </div><div><div>-- </div><div>Evgeny Novikov<br />Linux Verification Center, ISP RAS<br />http://linuxtesting.org</div></div><div> </div><div> </div><div> </div><div>26.05.2021, 11:45, "Greg Kroah-Hartman" <gregkh@linuxfoundation.org>:</div><blockquote><p>On Wed, May 26, 2021 at 11:21:36AM +0300, Evgeny Novikov wrote:</p><blockquote> Now I see that we need to restrict in specifications those values that<br /> can be passed to the install callback of tty_operations according to<br /> a first actual argument of tty_alloc_driver(). Thank you for pointing<br /> this out.</blockquote><p><br />I do not understand what you mean here at all, sorry.<br /><br />What "specifications"?<br /><br />confused,<br /><br />greg k-h</p></blockquote>