2021-01-24 23:13 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001178Frama-CKernelpublic2012-09-19 17:16
ReporterAnne 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionduplicate 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001178: Several types for the same function
DescriptionOn the following program :

void f (void) { unsigned char c = 0xef; out (c); }
void out (unsigned x) {}
int main (void) { f(); return 0; }

Frama-C alone seems happy, but the value analysis gives:
toto.c:1:[value] warning: Pointed function type must match function pointer type when dereferenced: assert(Ook)
which leads to :
[value] Values for function f: NON TERMINATING FUNCTION.

The problem disappears when out is declared before f.

Frama-C should at least gives a warning (or fail ?)
Additional InformationThis is very strange since this warning occurs when processing the call to 'out' because [Kernel_function.get_return_type f]
is different from the return type of the TFun type [Cil.typeOf funcexp].
It seems to me than both evaluation should go though the same variable,
so there might be two different variables for the 'out' function ???
TagsNo tags attached.
Attached Files

-Relationships
duplicate of 0000728closedyakobowski Arguments are not checked when function call precedes function declaration 
+Relationships

-Notes

~0002989

yakobowski (manager)

I cannot check right now, but I suspect this is another instance of bug 0000728. The current development of Frama-C already fails on this kind of code.

~0002990

Anne (reporter)

Yes: it looks similar... maybe it has been fixed already, then.

~0002992

virgile (developer)

It's indeed already fixed in SVN.
+Notes

-Issue History
Date Modified Username Field Change
2012-05-04 13:27 Anne New Issue
2012-05-04 13:43 yakobowski Note Added: 0002989
2012-05-04 15:21 Anne Note Added: 0002990
2012-05-07 10:50 virgile Note Added: 0002992
2012-05-07 10:50 virgile Relationship added duplicate of 0000728
2012-05-07 10:50 virgile Duplicate ID 0 => 728
2012-05-07 10:50 virgile Status new => resolved
2012-05-07 10:50 virgile Fixed in Version => Frama-C GIT, precise the release id
2012-05-07 10:50 virgile Resolution open => duplicate
2012-05-07 10:50 virgile Assigned To => virgile
2012-09-19 17:15 signoles Fixed in Version Frama-C GIT, precise the release id => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
+Issue History