Division by zero doesn't increase the number of VC in console output
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:
/*@ assigns \nothing; */ int test2(int a) { return a / 0; }
Frama-C:
[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
Proved goals line is the same as in the case without division: Test1:
/*@ assigns \nothing; */ int test1(int a) { return a; }
Frama-C output:
[kernel] Parsing test1.c (with preprocessing) [rte] annotating function test1 [wp] 1 goal scheduled [wp] Proved goals: 1 / 1 Qed: 1
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:
/*@ assigns \nothing; */ int test3(int a) { //@ assert 0 != 0; return a / 0; }
Frama-C:
[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)