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 == 2*q + 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). ## Attachments - [modulo_testcase.c](/uploads/b725efd4758f124867c970e99d059011/modulo_testcase.c)