Linux Driver Verification

Any sample driver that yields a false positive because of this?

That's funny. A nice example of underestimation.

First, I added a test for model 32 with this function.

Then, I have implemented a model. Test was failing.

Then, I noticed that I missed a file in test Makefile, so I wrote a script to automatically generate it. Test was still failing.

Then, I noticed that model 32_1 and model 32_7 actually, have different files. I copied the model function to that of 32_7. Test was still failing.

Then, I noticed that atomic_dec_and_mutex_lock has, actually, two arguments, and only the second one should be rerouted. This functionality was missing from the rerouter. So, I fixed the rerouter in BLAST, adding a new option -reroute-map2. Tests kept failing.

Then, I noticed that I should also add this to RCV backend. Now the tests is passed, and the fix is being tested on LDV-git...

Fixed in 7aca71a. Small and model tests are passed, but watch out for nightly tests today!

The driver you supplied yields Memory limit for me, so couldn't check it properly.

Ok, I increased the memory limit, and found out that BLAST crashes without any useful error! Investigating...

Alias analysis (which was partly on!) was failing on some anonymous fields or something. Didn't want to dig up, just made it a warning instead of an error, and turned alias analysis off completely (this should save several hours, or, perhaps, even days, for a typical ldv-git run!)

The driver still yields memory limit on my machine. However, the previous version of the rule thought that there's a potential error on iteration 7431, while the new version gets as far as to iteration 8654! Definitely, something happens here. Marking as resolved.

UNSAFE -> Out of memory in my run as well.