Correctness bug: division by 0 not detected
ID0000514: This issue was created automatically from Mantis Issue 514. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000514 | Frama-C | Plug-in > jessie | public | 2010-06-18 | 2010-09-29 |
| Reporter | pascal | Assigned To | cmarche | Resolution | no change required |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
Verifying the code in the attached file, I was boasting I had found an overflow, and someone pointed out to me a division by zero. This was very embarrassing.
Frama-C 20100401, Why 2.26, Alt-Ergo 0.91
frama-c -jessie interp_search.c
The safety of the function interpolationSearch is not proved yet with the invariants I wrote so far, but what worries me is that the VC for the division (number 37 in the list) is proved when this function clearly has division-by-zero problems, for instance when run on the input vector provided in the main() function in the file. Compiling and executing does not make the error manifest itself, but the value analysis guarantees that there is one (frama-c-gui -val interp_search.c).
I am not sure whether it is a good idea to report a bug when there are still unproved VCs, but the establishment/preservation of the invariants I wrote are proved, so hopefully they are not false. Also I had the hope that there no longer was any overflow with the casts to "long long" I have introduced, so that the division-by-zero bug would be first in the control flow (so that the proof of its absence may not be caused by assuming another, false, VC above it).
Aside: the original function appear to have all the mentioned problems and to be in Java. Maybe it is a good example to run Krakatoa on?