Frama-C Bug Tracking System - Frama-C
View Issue Details
0002098Frama-CKernel > ACSL implementationpublic2015-03-31 15:442016-01-26 18:30
Frama-C Sodium 
Frama-C MagnesiumFrama-C Magnesium 
0002098: overloading of predicate fails
Overloading of ACSL predicates does not work anymore.
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.
the problem does NOT occur under Neon.
No tags attached.
c overloading.c (141) 2015-03-31 15:44
c overloading2.c (440) 2015-04-03 12:47
Issue History
2015-03-31 15:44jensNew Issue
2015-03-31 15:44jensFile Added: overloading.c
2015-03-31 16:56virgileAssigned To => virgile
2015-03-31 16:56virgileStatusnew => confirmed
2015-03-31 16:56virgileCategoryKernel => Kernel > ACSL implementation
2015-03-31 16:56virgileTarget Version => Frama-C Magnesium
2015-04-03 12:47jensFile Added: overloading2.c
2015-04-03 12:52jensNote Added: 0005863
2015-04-14 18:13virgileNote Added: 0005886
2015-04-14 18:13virgileStatusconfirmed => resolved
2015-04-14 18:13virgileResolutionopen => fixed
2016-01-26 08:51signolesFixed in Version => Frama-C Magnesium
2016-01-26 08:52signolesStatusresolved => closed
2016-01-26 18:30virgileNote Added: 0006140

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.
2015-04-14 18:13   
Fix committed to master branch.
2016-01-26 18:30   
Fait dans le commit da16395