| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000791 | Frama-C | Plug-in > Eva | public | 2011-04-13 08:55 | 2014-02-12 16:54 | ||||
| Reporter | patrick | ||||||||
| Assigned To | pascal | ||||||||
| Priority | normal | Severity | crash | Reproducibility | have not tried | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C GIT, precise the release id | ||||||||
| Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
| Summary | 0000791: Cash in value analysis of sliced project | ||||||||
| Description | Unexpected error (File "src/kernel/cilE.ml", line 268, characters 68-74: Assertion failed). | ||||||||
| Additional Information | Revision: 12829 Command: frama-c bug.c -slice-return send -then-on 'Slicing export' -val file bug.c /*@ assigns *p \from \empty; assigns \result ; */ int scanf (char const *, int * p); /*@ assigns \nothing ; */ int send (int x) { return x; } void main(void) { int input; scanf("%d",&input); send (input); } | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
||||||
|
||||||
 Relationships |
| Notes |
|
|
yakobowski (manager) 2011-04-14 10:31 |
Building parts of a new AST inside a copy visitor is really tricky to get right. The above patch ensures that varinfos will not clash between the different projects, but this is not the Right Thing To Do. No better solution for now. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-04-13 08:55 | patrick | New Issue | |
| 2011-04-13 08:55 | patrick | Status | new => assigned |
| 2011-04-13 08:55 | patrick | Assigned To | => pascal |
| 2011-04-13 09:25 | patrick | Description Updated | |
| 2011-04-13 09:25 | patrick | Additional Information Updated | |
| 2011-04-14 10:28 | svn | ||
| 2011-04-14 10:31 | yakobowski | Note Added: 0001785 | |
| 2011-04-14 10:31 | yakobowski | Status | assigned => resolved |
| 2011-04-14 10:31 | yakobowski | Fixed in Version | => Frama-C GIT, precise the release id |
| 2011-04-14 10:31 | yakobowski | Resolution | open => fixed |
| 2011-04-14 13:54 | svn | ||
| 2011-04-14 14:33 | yakobowski | Relationship added | related to 0000780 |
| 2011-10-10 14:13 | signoles | Fixed in Version | Frama-C GIT, precise the release id => Frama-C Nitrogen-20111001 |
| 2011-10-10 14:14 | signoles | Status | resolved => closed |
| 2013-12-19 01:12 | patrick | Source_changeset_attached | => framac master 27c67364 |
| 2013-12-19 01:12 | yakobowski | Source_changeset_attached | => framac master 2a32c195 |
| 2014-02-12 16:54 | patrick | Source_changeset_attached | => framac stable/neon 27c67364 |
| 2014-02-12 16:54 | yakobowski | Source_changeset_attached | => framac stable/neon 2a32c195 |
| 2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |
| Issue History |