Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
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.
Attached Filesc file icon ftest.c [^] (137 bytes) 2013-02-14 14:12 [Show Content]

- Relationships

-  Notes
(0003700)
yakobowski (manager)
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 (manager)
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 Modified Username Field Change
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker