Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001367Frama-CDocumentation > ACSLpublic2013-02-14 14:122016-06-21 15:35
ReporterJochen 
Assigned Toyakobowski 
PrioritynormalSeveritytextReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0001367: suggest to mention in acsl manual that \valid shouldn't be applied to function pointers
DescriptionRunning "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.
TagsNo tags attached.
Relationships
Attached Filesc ftest.c (137) 2013-02-14 14:12
https://bts.frama-c.com/file_download.php?file_id=470&type=bug

Notes
(0003700)
yakobowski   
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 !=.
(0006204)
yakobowski   
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).

Issue History
Date ModifiedUsernameFieldChange
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