| 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 |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
| Issue History |
|||
| 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 |
| Issue History |