Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002098Frama-CKernel > ACSL implementationpublic2015-03-31 15:442016-01-26 18:30
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFrama-C MagnesiumFixed in VersionFrama-C Magnesium 
Summary0002098: overloading of predicate fails
DescriptionOverloading of ACSL predicates does not work anymore.

Steps To Reproducethe 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 Informationthe problem does NOT occur under Neon.
TagsNo tags attached.
Attached Filesc file icon overloading.c [^] (141 bytes) 2015-03-31 15:44 [Show Content]
c file icon overloading2.c [^] (440 bytes) 2015-04-03 12:47 [Show Content]

- Relationships

-  Notes
(0005863)
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.
(0005886)
virgile (developer)
2015-04-14 18:13

Fix committed to master branch.
(0006140)
virgile (developer)
2016-01-26 18:30

Fait dans le commit da16395

- Issue History
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 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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker