3 ms·
In the first test example, how does the framework know that `size` shouldn't return -1?
by brabel 6y ago
In the first test example, how does the framework know that `size` shouldn't return -1?
- the-smug-one 6y agoThere's a finite amount of valid linear execution histories for the example given. Run all of these in one thread, collect states (or return values, or whatever), and compare them when model checking. I don't know if that's what LinCheck does, but that's what I'd do if I wrote LinCheck :-).