Frama-C Bug Tracking System - Frama-C
View Issue Details
0002428Frama-CPlug-in > wppublic2019-02-17 14:182019-02-25 09:09
evdenis 
correnson 
normalmajoralways
closedno change required 
Frama-C 18-Argon 
 
0002428: Division by zero doesn't increase the number of VC in console output
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)
No tags attached.
c test2.c (62) 2019-02-17 14:18
https://bts.frama-c.com/file_download.php?file_id=1303&type=bug
Issue History
2019-02-17 14:18evdenisNew Issue
2019-02-17 14:18evdenisStatusnew => assigned
2019-02-17 14:18evdenisAssigned To => correnson
2019-02-17 14:18evdenisFile Added: test2.c
2019-02-18 08:53virgileNote Added: 0006749
2019-02-18 08:54virgileStatusassigned => resolved
2019-02-18 08:54virgileResolutionopen => no change required
2019-02-25 09:09signolesStatusresolved => closed

Notes
(0006749)
virgile   
2019-02-18 08:53   
This is not a bug, but a feature 😁. By default, WP will only generate proof obligations for annotations that have not yet been verified (or falsified in this case) by other plugins (there's no need to do duplicate work) When RTE is saying "guaranteed RTE", it also puts a "invalid if reachable" status on the generated annotation, so that WP will ignore it. If you'd prefer WP to go on all annotations, option -wp-status-all will do that.

In addition, note that it is always possible to ask for a report to be emitted after the analyses, with `frama-c -wp -wp-rte foo.c -then -report`: the plug-in Report will report about all annotations, regardless of which plug-in did emit a status for it. Hence, you'll find the alarm there, with a status set by RTE:

--------------------------------------------------------------------------------
--- Properties of Function 'test2'
--------------------------------------------------------------------------------

[ Partial ] Assigns nothing
            By Wp.typed, with pending:
             - Unreachable instruction (file foo.c, line 5)
[ Alarm ] Assertion 'rte,division_by_zero' (file foo.c, line 5)
            By rte, with pending:
             - Unreachable instruction (file foo.c, line 5)
[ Partial ] Default behavior
            By Frama-C kernel, with pending:
             - Unreachable instruction (file foo.c, line 5)

--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
     2 Locally validated
     1 Alarm emitted
     3 Total
--------------------------------------------------------------------------------