|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0001367||Frama-C||Documentation > ACSL||public||2013-02-14 14:12||2016-06-21 15:35|
|Product Version||Frama-C Oxygen-20120901|
|Target Version||Fixed in Version||Frama-C Aluminium|
|Summary||0001367: suggest to mention in acsl manual that \valid shouldn't be applied to function pointers|
|Description||Running "frama-c -val ftest.c" on the attached program reports an unsatisfied precondition in line 4, where \valid has been applied to a pointer to the function foo().|
From that behavior, I guess that \valid mustn't be applied to function pointers in general.
However, the acsl manual (acsl.pdf) says on p.54: "\valid applies to a set of terms (see Section 2.3.4) of some pointer type."
An apprioriate restriction to non-function-pointers could be added here.
|Tags||No tags attached.|
My interpretation of \valid is that it should only be applied to pointers to memory blocks, as it is meaningful only for pointers that reference memory. This is consistent with the use of "object" terminology in the section 2.7.1 of the ACSL manual.
However, the WP happily proves \valid(f) in your example. I must check with Loïc if this is the desired behavior.
Also, if we decide that \valid only applies to memory blocks, the kernel should statically reject your example at the typing phase.
Finally, to answer an implicit question: there is currently no way within Value to require a function pointer to be valid. You can only exclude abnormal values such as NULL using !=.
Indeed. On the original code, the kernel now prints
valid_function.c:3:[kernel] user error: expecting a pointer to an object, found void (*)(void)
With \valid_function, the code is accepted (and Value proves the precondition).
|2013-02-14 14:12||Jochen||New Issue|
|2013-02-14 14:12||Jochen||Status||new => assigned|
|2013-02-14 14:12||Jochen||Assigned To||=> signoles|
|2013-02-14 14:12||Jochen||File Added: ftest.c|
|2013-02-14 14:19||signoles||Assigned To||signoles => virgile|
|2013-02-15 16:56||yakobowski||Note Added: 0003700|
|2016-06-21 14:11||signoles||Category||Documentation => Documentation > ACSL|
|2016-06-21 14:25||signoles||Assigned To||virgile => yakobowski|
|2016-06-21 15:34||yakobowski||Note Added: 0006204|
|2016-06-21 15:34||yakobowski||Status||assigned => closed|
|2016-06-21 15:34||yakobowski||Resolution||open => fixed|
|2016-06-21 15:35||signoles||Fixed in Version||=> Frama-C Aluminium|