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 | ||||||
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 |
|
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2011-04-18 14:14 | patrick | New Issue | |
2011-04-18 14:14 | patrick | Status | new => assigned |
2011-04-18 14:14 | patrick | Assigned To | => pherrmann |
2011-04-18 17:26 | pherrmann | Note Added: 0001794 | |
2011-04-18 17:26 | pherrmann | Status | assigned => resolved |
2011-05-16 17:26 | signoles | Resolution | open => fixed |
2011-10-10 14:13 | signoles | Fixed in Version | => Frama-C Nitrogen-20111001 |
2011-10-10 14:14 | signoles | Status | resolved => closed |