2021-01-24 23:13 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001178Frama-CKernelpublic2012-09-19 17:16
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityhave not tried
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

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



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.


Anne (reporter)

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


virgile (developer)

It's indeed already fixed in SVN.

-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