Skip to content

suggest to mention in acsl manual that \valid shouldn't be applied to function pointers

ID0001367: This issue was created automatically from Mantis Issue 1367. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0001367 Frama-C Documentation > ACSL public 2013-02-14 2016-06-21
Reporter Jochen Assigned To yakobowski Resolution fixed
Priority normal Severity text Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Oxygen-20120901 Target Version - Fixed in Version Frama-C Aluminium

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.

Attachments

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information