| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000524 | Frama-C | Kernel | public | 2010-06-29 11:22 | 2014-02-12 16:55 | ||||
| Reporter | vmoyalam | ||||||||
| Assigned To | monate | ||||||||
| Priority | normal | Severity | major | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Boron-20100401 | ||||||||
| Target Version | Fixed in Version | Frama-C Carbon-20101201-beta1 | |||||||
| Summary | 0000524: Missing declared inline functions in Globals | ||||||||
| 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 | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
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? |
|
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. |
|
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? |
|
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. |
|
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. |
| Notes |
| 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 | ||
| 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 |
| 2013-12-19 01:13 | svn | Source_changeset_attached | => framac master 32e38788 |
| 2014-02-12 16:55 | monate | Source_changeset_attached | => framac stable/neon 32e38788 |
| Issue History |