Incorrect assignments with generated behavior for declared-only function with unamed arguments
ID0000731: This issue was created automatically from Mantis Issue 731. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000731 | Frama-C | Kernel | public | 2011-02-18 | 2011-02-20 |
| Reporter | Jonathan-Christofer Demay | Assigned To | virgile | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | - |
Description :
I guess an example is enough to explain the problem:
/*@ behavior generated: assigns *b; assigns \at(\result,Post) \from *b, a; assigns *b \from *b, a;
*/ extern int func1(int a , int b ) ; /@ behavior generated: assigns \at(\result,Post) \from \nothing; */ extern int func2(int , int * ) ; void main(void) { func1(0,(int *)0); func2(0,(int *)0); return; }