3 ms·
That's right! There's no "traditional" loops as programs have to be proved to terminate at some point. That being said, very recently support for bounded loops
by javierhonduco 4y ago
That's right! There's no "traditional" loops as programs have to be proved to terminate at some point.
That being said, very recently support for bounded loops landed [0]. It's very exciting and useful, and I've seen it reduce verification times significantly, but we can't use this yet as it requires kernel 5.3 or greater, and we would like to support as many users as possible!
[0]: https://lwn.net/Articles/877062/ https://lwn.net/Articles/877062/
[1]: https://github.com/iovisor/bcc/commit/38304256c49a02aecbf78f2fdc4b86d95eb8df9f https://github.com/iovisor/bcc/commit/38304256c49a02aecbf78f...