Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000524Frama-CKernelpublic2010-06-29 11:222014-02-12 16:55
Reportervmoyalam 
Assigned Tomonate 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000524: Missing declared inline functions in Globals
DescriptionIf several inline functions have the same signature (parameter type and return type), only one (the first of them) is found in Globals.
Additional InformationThe 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
TagsNo tags attached.
Attached Filesgz file icon testInline.tar.gz [^] (1,699 bytes) 2010-06-29 11:22

- Relationships

-  Notes
(0000955)
monate (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
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.

- Issue History
Date Modified Username Field Change
2010-06-29 11:22 vmoyalam New Issue
2010-06-29 11:22 vmoyalam File Added: testInline.tar.gz
2010-06-30 00:50 monate Note Added: 0000955
2010-06-30 00:50 monate Assigned To => monate
2010-06-30 00:50 monate Status new => acknowledged
2010-06-30 00:51 monate Status acknowledged => feedback
2010-06-30 09:42 vmoyalam Note Added: 0000956
2010-06-30 11:12 monate Note Added: 0000957
2010-06-30 11:43 vmoyalam Note Added: 0000958
2010-06-30 14:34 monate Note Added: 0000959
2010-06-30 14:34 monate Status feedback => resolved
2010-06-30 14:34 monate Fixed in Version => Frama-C svn, precise the release id
2010-06-30 14:34 monate Resolution open => fixed
2010-06-30 21:23 svn Checkin
2010-12-10 15:40 signoles Fixed in Version Frama-C GIT, precise the release id => Frama-C Carbon-20101201-beta1
2010-12-17 19:38 signoles Status resolved => closed

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker