ID0002428: **This issue was created automatically from Mantis Issue 2428. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002428 | Frama-C | Plug-in > wp | public | 2019-02-17 | 2019-02-25 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | evdenis | **Assigned To** | correnson | **Resolution** | no change required | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - | ### Description : Obvious division by zero doesn't increase the total number of proof obligations: Test2: <pre> /*@ assigns \nothing; */ int test2(int a) { return a / 0; } </pre> Frama-C: <pre> [kernel] Parsing test2.c (with preprocessing) [rte] annotating function test2 [rte] test2.c:5:8: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0; [wp] 1 goal scheduled [wp] Proved goals: 1 / 1 Qed: 1 </pre> Proved goals line is the same as in the case without division: Test1: <pre> /*@ assigns \nothing; */ int test1(int a) { return a; } </pre> Frama-C output: <pre> [kernel] Parsing test1.c (with preprocessing) [rte] annotating function test1 [wp] 1 goal scheduled [wp] Proved goals: 1 / 1 Qed: 1 </pre> From my point of view this is an incorrect behavior and the proved goals like should be 'Proved goals: 1 / 2' as in this case: Test3: <pre> /*@ assigns \nothing; */ int test3(int a) { //@ assert 0 != 0; return a / 0; } </pre> Frama-C: <pre> [kernel] Parsing test3.c (with preprocessing) [rte] annotating function test3 [rte] test3.c:6:8: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0; [wp] 2 goals scheduled [wp] [Alt-Ergo] Goal typed_test3_assert : Unknown (109ms) [wp] Proved goals: 1 / 2 Qed: 1 Alt-Ergo: 0 (unknown: 1) </pre> ## Attachments - [test2.c](/uploads/6a8a966174608d26a4e3aaca44d430f1/test2.c)