Frama-C Bug Tracking System - Frama-C
View Issue Details
0001367Frama-CDocumentation > ACSLpublic2013-02-14 14:122016-06-21 15:35
Frama-C Oxygen-20120901 
Frama-C Aluminium 
0001367: suggest to mention in acsl manual that \valid shouldn't be applied to function pointers
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.
No tags attached.
c ftest.c (137) 2013-02-14 14:12
Issue History
2013-02-14 14:12JochenNew Issue
2013-02-14 14:12JochenStatusnew => assigned
2013-02-14 14:12JochenAssigned To => signoles
2013-02-14 14:12JochenFile Added: ftest.c
2013-02-14 14:19signolesAssigned Tosignoles => virgile
2013-02-15 16:56yakobowskiNote Added: 0003700
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL
2016-06-21 14:25signolesAssigned Tovirgile => yakobowski
2016-06-21 15:34yakobowskiNote Added: 0006204
2016-06-21 15:34yakobowskiStatusassigned => closed
2016-06-21 15:34yakobowskiResolutionopen => fixed
2016-06-21 15:35signolesFixed in Version => Frama-C Aluminium

2013-02-15 16:56   
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 !=.
2016-06-21 15:34   
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).