Several types for the same function
ID0001178: This issue was created automatically from Mantis Issue 1178. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001178 | Frama-C | Kernel | public | 2012-05-04 | 2012-09-19 |
| Reporter | Anne | Assigned To | virgile | Resolution | duplicate |
| Priority | normal | Severity | major | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
On 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 Information :
This 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 ???