Range of remainder of two positive integers, wrong and missing assertions.
ID0002129: This issue was created automatically from Mantis Issue 2129. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002129 | Frama-C | Plug-in > wp | public | 2015-06-04 | 2015-06-29 |
| Reporter | loic | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | Linux | OS | Ubuntu | OS Version | 12.04.5 LTS |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
Nitrogen-20111001 alt-ergo 0.94
False negative and false positive int the following code.
/@ requires 0 <= n; / void modulo_testcase_0(unsigned n) { /@ ghost unsigned q = n / 2; / /@ ghost unsigned r = n % 2; / /@ assert 0 <= n; / / OK / /@ assert n == 2q + r; / / OK / /@ assert 0 <= q; / / OK / /@ assert 0 <= r < 1; / / NOK, cannot be proven */ }
/*@ requires 0 <= n && 0 < d; / void modulo_testcase_1(int n, int d) { /@ assert n <= d * (n / d); / / NOK, cannot be proven / /@ ghost int q = n / d; / / OK / /@ ghost int r = n % d; / / OK / /@ assert 0 <= r < 1; / / NOK, r < d is true / /@ assert n <= d * (n / d); / / OK */ }
Steps To Reproduce :
frama-c -wp -wp-rte on the code above (also as attachment).