2021-02-24 18:57 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001213Frama-CKernelpublic2013-06-18 09:47
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon ftest.c (64 bytes) 2012-06-18 16:22 -
    int g;
    //@ ensures g==0;
    void main(void) {
        g=0;
        f();
    }
    
    
    c file icon ftest.c (64 bytes) 2012-06-18 16:22 +

-Relationships
+Relationships

-Notes

~0003161

yakobowski (manager)

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)

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)

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)

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

-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
+Issue History