suggest to forbid unknown functions by default
ID0001213: This issue was created automatically from Mantis Issue 1213. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001213 | Frama-C | Kernel | public | 2012-06-18 | 2013-06-18 |
| Reporter | Jochen | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Fluorine-20130401 |
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;".