Frama-C Bug Tracking System - Frama-C
View Issue Details
0000524Frama-CKernelpublic2010-06-29 11:222014-02-12 16:55
vmoyalam 
monate 
normalmajoralways
closedfixed 
Frama-C Boron-20100401 
Frama-C Carbon-20101201-beta1 
0000524: Missing declared inline functions in Globals
If several inline functions have the same signature (parameter type and return type), only one (the first of them) is found in Globals.
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
No tags attached.
gz testInline.tar.gz (1,699) 2010-06-29 11:22
https://bts.frama-c.com/file_download.php?file_id=101&type=bug
Issue History
2010-06-29 11:22vmoyalamNew Issue
2010-06-29 11:22vmoyalamFile Added: testInline.tar.gz
2010-06-30 00:50monateNote Added: 0000955
2010-06-30 00:50monateAssigned To => monate
2010-06-30 00:50monateStatusnew => acknowledged
2010-06-30 00:51monateStatusacknowledged => feedback
2010-06-30 09:42vmoyalamNote Added: 0000956
2010-06-30 11:12monateNote Added: 0000957
2010-06-30 11:43vmoyalamNote Added: 0000958
2010-06-30 14:34monateNote Added: 0000959
2010-06-30 14:34monateStatusfeedback => resolved
2010-06-30 14:34monateFixed in Version => Frama-C svn, precise the release id
2010-06-30 14:34monateResolutionopen => fixed
2010-06-30 21:23svnCheckin
2010-12-10 15:40signolesFixed in VersionFrama-C GIT, precise the release id => Frama-C Carbon-20101201-beta1
2010-12-17 19:38signolesStatusresolved => closed

Notes
(0000955)
monate   
2010-06-30 00:50   
This is a feature, but I'm not sure it is really a good one. first and second are isomorphic in some sense (the local declared variable a is not used and is therefore ignored). static inline function are emitted only once in the final source code: this prevents useless duplication when such functions are declared in multiply-included headers. Frama-C insists on minimizing the number of such functions. You may questions : * why a local variable declaration is'nt a source of non-isomorphism? * why different static inline names are collapsed if functions are isomorphic What would you expect in your specific settings?
(0000956)
vmoyalam   
2010-06-30 09:42   
We can have some of that kind of functions from an include header. Despite their isomorphism, their definition should be accessible by our plug-in (find_def_by_name) in place of raising a "Not_found" exception.
(0000957)
monate   
2010-06-30 11:12   
Do you need the function with its original name to be kept in the AST or only to be able to fetch its isomorphic brother with find_def_by_name?
(0000958)
vmoyalam   
2010-06-30 11:43   
We already have the function name in the Untyped AST from which (its visitor) we try to get the function definition with "find_def_by_name". In this use case, we get a "Not_found" exception as it is in the Untyped AST but not in Globals.
(0000959)
monate   
2010-06-30 14:34   
This will be fixed by svn > 9230 whenever I get access to the network. Isomorphy will no longer be modulo alpha conversion.