| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001178 | Frama-C | Kernel | public | 2012-05-04 13:27 | 2012-09-19 17:16 | ||||
| Reporter | Anne | ||||||||
| Assigned To | virgile | ||||||||
| Priority | normal | Severity | major | Reproducibility | have not tried | ||||
| Status | closed | Resolution | duplicate | ||||||
| Product Version | Frama-C Nitrogen-20111001 | ||||||||
| Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
| Summary | 0001178: Several types for the same function | ||||||||
| 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 ??? | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
||||||
|
||||||
 Relationships |
| Notes |
|
|
yakobowski (manager) 2012-05-04 13:43 |
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) 2012-05-04 15:21 |
Yes: it looks similar... maybe it has been fixed already, then. |
|
virgile (developer) 2012-05-07 10:50 |
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 |