| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0000800 | Frama-C | Plug-in > RTE | public | 2011-04-18 14:14 | 2011-10-10 14:14 |
|
| Reporter | patrick | |
| Assigned To | pherrmann | |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | | |
| Target Version | | Fixed in Version | Frama-C Nitrogen-20111001 | |
|
| Summary | 0000800: wrong generation of assigns \nothing at function call |
| Description | RTE should not generate assigns \nothing; at the statement calling function f |
| Additional Information | > cat file.c:
int X, Y ;
//@ assigns \union(X, Y) ;
void f () ;
void g() {
f () ;
}
> frama-c -print -rte file.c
int X ;
int Y ;
/*@ assigns \union(X, Y); */
extern void f() ;
void g(void)
{
/*@ behavior pre_f_0:
assigns \nothing; */
f();
return;
}
|
| Tags | No tags attached. |
|
| Attached Files | |
|
Relationships 
Relationships