|
|
|
|
|
|
by guitarbill
3559 days ago
|
|
|
AFAIK, white-box testing is simply when you can look at the source code (as opposed to black-box testing) for example a unit test is a type of white-box test. What I was struggling to express is that in the mathematical notation, the operations are well defined (right?); in C that's not necessarily the case. So you could argue that if you were writing direct tests, you don't need to check all inputs, but testing edge-cases will do. And maybe that's true, but practically impossible for complex algos because how do you know which inputs cause edge case behaviour? So I was agreeing that this approach is probably better than having some fallible human write test cases :) (better = more thorough and reliable) And although you'd have to make sure the same fallible human hasn't put bugs in the mathematical spec, as you've said that's probably easier to check. EDIT: Nevermind, I found part three about undefined behaviour. I had written: You seem to know loads about this, maybe you could say how undefined C behaviour is handled when comparing against a spec? Is e.g. shift-past-bitwidth simply forbidden? The only alternative I can think of is looking at the disassembly on a certain platform and checking those instructions, which sounds less than ideal. |
|
|
Some comments:
* the operations in the mathematical spec are mostly well defined, but e.g. division by zero is not defined. However, the verification handles this by checking that all operations are well-defined on all possible inputs.
* yes, identifying the "edge cases" is not something you can do easily, and hard to make formal. In some sense, the fact the non-edge-case inputs are treated in a uniform way is probably what allows the verification to succeed at all.
* a short summary of the answer you already found in the third blog post: what we actually verify is the LLVM assembly that Clang produces when compiling the C program. Much of the potentially undefined behavior in a C program is translated away by the compiler on the way to LLVM assembly. For any potential undefined behavior that remains in the LLVM assembly, the verification checks that it cannot happen at runtime.