Note, LLMs are very good at finding suspect “security issues” in kernel code these days. But even with the best of the current and next generation tools, at least 1/3 of the results they generate are flat out wrong or harmful. So, if you think your LLM-found/fixed issue in a drivers/staging/ file is really valid, it’s fine to submit it BUT you must have first tested it on the actual hardware for the driver, and described how you have done so, in order for us to be willing to take the change.
We’re talking about different kind of proofs.
Proving a program is correct requires a formal specification and a formal verification with mathematics and/or formal methods. ie proving the behavior and result perfectly match specification for all possible inputs.
A test only proves that a program 1) returns the expected output for a specific input, or limited set of inputs, and 2) appears to behave correctly, ie there may be undefined behaviour but they don’t cause an immediate crash.
lol no. Absolutely no. In any way. Ever. A bug either works or it doesn’t. The fact you think I’m talking about something else means you are already cooked, utterly and completely. Sad.
So you prove you fixed the bug. How do you test to prove you didn’t introduce another?