View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002098 | Frama-C | Kernel > ACSL implementation | public | 2015-03-31 15:44 | 2016-01-26 18:30 | ||||
Reporter | jens | ||||||||
Assigned To | virgile | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Sodium | ||||||||
Target Version | Frama-C Magnesium | Fixed in Version | Frama-C Magnesium | ||||||
Summary | 0002098: overloading of predicate fails | ||||||||
Description | Overloading of ACSL predicates does not work anymore. | ||||||||
Steps To Reproduce | the attached program reports the following error when called with 'frama-c overloading.c' [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing overloading.c (with preprocessing) overloading.c:10:[kernel] user error: invalid implicit conversion from 'int' to 'short' in annotation. [kernel] user error: stopping on file "overloading.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command. [kernel] Frama-C aborted: invalid user input. | ||||||||
Additional Information | the problem does NOT occur under Neon. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
jens (reporter) 2015-04-03 12:52 |
I added another example file overloading2.c and I experimented a bit with reordering the various overloaded versions. I am not sure this is relevant but the error message overloading.c:22:[kernel] user error: invalid implicit conversion from 'long long' to 'int' in annotation. refers to the 'int' version which is declared immediately before the 'long long' version. Seems to be a pattern. |
virgile (developer) 2015-04-14 18:13 |
Fix committed to master branch. |
virgile (developer) 2016-01-26 18:30 |
Fait dans le commit da16395 |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2015-03-31 15:44 | jens | New Issue | |
2015-03-31 15:44 | jens | File Added: overloading.c | |
2015-03-31 16:56 | virgile | Assigned To | => virgile |
2015-03-31 16:56 | virgile | Status | new => confirmed |
2015-03-31 16:56 | virgile | Category | Kernel => Kernel > ACSL implementation |
2015-03-31 16:56 | virgile | Target Version | => Frama-C Magnesium |
2015-04-03 12:47 | jens | File Added: overloading2.c | |
2015-04-03 12:52 | jens | Note Added: 0005863 | |
2015-04-14 18:13 | virgile | Source_changeset_attached | => framac master 5e67952e |
2015-04-14 18:13 | virgile | Note Added: 0005886 | |
2015-04-14 18:13 | virgile | Status | confirmed => resolved |
2015-04-14 18:13 | virgile | Resolution | open => fixed |
2016-01-26 08:51 | signoles | Fixed in Version | => Frama-C Magnesium |
2016-01-26 08:52 | signoles | Status | resolved => closed |
2016-01-26 18:30 | virgile | Note Added: 0006140 |