Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001213Frama-CKernelpublic2012-06-18 16:222013-06-18 09:47
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001213: suggest to forbid unknown functions by default
DescriptionDue to FRAMA-C's current defaults, the attached program is considered correct by both Jessie and Wp. I suggest to change these defaults; an undeclared function should be treated as having an unsatisfiable contract ("requires \false"). Reasons are:
(1) The called function f() most likely has some effect, since its call would have been omitted otherwise. If f() doesn't take arguments and doesn't return a value, such an effect *must* be a change of some global variable. In other cases, it still *can* be such a change.
(2) FRAMA-C's warning about missing code for f() appears only on stdout, while most users inspect only the gui. The latter conveys the impression of everything being verified and ok. This way, a typo in the called function's names passes unnoticed. In fact, I just had such a problem.
(3) Applications that really need FRAMA-C's current defaults can specify the affected functions as "requires \true; assigns \nothing;".
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (64 bytes) 2012-06-18 16:22 [Show Content]

- Relationships

-  Notes
(0003161)
yakobowski (manager)
2012-06-18 17:02

The current development version complains already a bit more than Nitrogen:

ftest.c:5:[kernel] warning: Calling undeclared function f. Old style K&R code?
[kernel] warning: Neither code nor specification for function f, generating default assigns from the prototype

Both warnings are shown in the "Messages" panel of the GUI. we are also considering displaying a non-green status on the (inferred) assigns of f.
(0003167)
virgile (developer)
2012-06-19 10:08

This is a feature wish for the kernel, not a particular plug-in: all plug-ins should treat such functions the same way.
(0003915)
signoles (manager)
2013-05-28 09:58

In Fluorine, the status of the contract (including the inferred assigns) for such a function is not green anymore. It is "blue-green" which means "unproven but considered valid for proving the properties which depends on it; you should verify it by external way".

@Jochen: are this status and the additional warnings explained by Boris enough?
(0003956)
Jochen (reporter)
2013-06-13 15:13

@Julien: Yes, they are ok for me, and seemingly also for my colleagues here.

- Issue History
Date Modified Username Field Change
2012-06-18 16:22 Jochen New Issue
2012-06-18 16:22 Jochen Status new => assigned
2012-06-18 16:22 Jochen Assigned To => correnson
2012-06-18 16:22 Jochen File Added: ftest.c
2012-06-18 17:02 yakobowski Note Added: 0003161
2012-06-19 10:08 virgile Note Added: 0003167
2012-06-19 10:08 virgile Assigned To correnson => virgile
2012-06-19 10:08 virgile Category Plug-in > wp => Kernel
2013-05-28 09:58 signoles Note Added: 0003915
2013-05-28 09:58 signoles Status assigned => feedback
2013-06-13 15:13 Jochen Note Added: 0003956
2013-06-18 09:47 signoles Status feedback => closed
2013-06-18 09:47 signoles Resolution open => fixed
2013-06-18 09:47 signoles Fixed in Version => Frama-C Fluorine-20130401


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker