suggest to forbid unknown functions by default
ID0001213: This issue was created automatically from Mantis Issue 1213. Further discussion may take place here.
|Product Version||Frama-C Nitrogen-20111001||Target Version||-||Fixed in Version||Frama-C Fluorine-20130401|
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;".