|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0001213||Frama-C||Kernel||public||2012-06-18 16:22||2013-06-18 09:47|
|Product Version||Frama-C Nitrogen-20111001|
|Target Version||Fixed in Version||Frama-C Fluorine-20130401|
|Summary||0001213: suggest to forbid unknown functions by default|
|Description||Due 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;".
|Tags||No tags attached.|
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.
|This is a feature wish for the kernel, not a particular plug-in: all plug-ins should treat such functions the same way.|
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?
|@Julien: Yes, they are ok for me, and seemingly also for my colleagues here.|
|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|