Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002428Frama-CPlug-in > wppublic2019-02-17 14:182019-02-25 09:09
Reporterevdenis 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionno change required 
PlatformOSOS Version
Product VersionFrama-C 18-Argon 
Target VersionFixed in Version 
Summary0002428: Division by zero doesn't increase the number of VC in console output
DescriptionObvious 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)
TagsNo tags attached.
Attached Filesc file icon test2.c [^] (62 bytes) 2019-02-17 14:18 [Show Content]

- Relationships

-  Notes
(0006749)
virgile (developer)
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 --------------------------------------------------------------------------------

- Issue History
Date Modified Username Field Change
2019-02-17 14:18 evdenis New Issue
2019-02-17 14:18 evdenis Status new => assigned
2019-02-17 14:18 evdenis Assigned To => correnson
2019-02-17 14:18 evdenis File Added: test2.c
2019-02-18 08:53 virgile Note Added: 0006749
2019-02-18 08:54 virgile Status assigned => resolved
2019-02-18 08:54 virgile Resolution open => no change required
2019-02-25 09:09 signoles Status resolved => closed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker