Missing declared inline functions in Globals
ID0000524: This issue was created automatically from Mantis Issue 524. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0000524 | Frama-C | Kernel | public | 2010-06-29 | 2014-02-12 |
Reporter | vmoyalam | Assigned To | monate | Resolution | fixed |
Priority | normal | Severity | major | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | Frama-C Carbon-20101201-beta1 |
Description :
If several inline functions have the same signature (parameter type and return type), only one (the first of them) is found in Globals.
Additional Information :
The attached file contains :
- A plug-in which recovers all declared functions from Globals and recovers information for each function from source file (from the untyped_AST visitor) is attached (DEV folder)
- A test source file (VAL folder) with several inline functions.
After building and installing the plug-in (make - make install), try the following command : frama-c -test_inline testInline.c