Missing or misleading warnings when merging two functions
ID0000999: This issue was created automatically from Mantis Issue 999. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000999 | Frama-C | Kernel | public | 2011-10-24 | 2014-02-12 |
| Reporter | yakobowski | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
frama-c does not complain in the right way when parsing the following code:
- there is no warning for the types, even though the return types are not compatible
- the warning "found two default behaviors, merging them" is not really intuitive for the user, as he has not written "behavior" anywhere.
//@ assigns \nothing; int foo(int* p);
//@ ensures 0 <= \result < 25; unsigned short foo() { return 0; }