View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001828 | Frama-C | Plug-in > wp | public | 2014-07-08 14:26 | 2015-03-17 22:18 | ||||
Reporter | correnson | ||||||||
Assigned To | patrick | ||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | |||||||||
Target Version | Fixed in Version | Frama-C Sodium | |||||||
Summary | 0001828: Frame Validity | ||||||||
Description | //@ requires \valid(one); void f(int *one){ int two; //@ assert one != &two; } int *zero; //@ requires \valid(zero) && \valid(one); void frame(int *one, int arg){ int two; //@ assert formal: \separated(one,&arg,&two); //@ assert global: \separated(zero,&arg,&two); } | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
patrick (developer) 2014-08-21 09:12 Last edited: 2014-08-21 10:20 |
The initial issue was bettween locals and formals. The same kind of problem exists between locals and globals, and between formals and globals... So the example of description was extended. |
patrick (developer) 2014-09-15 10:11 |
Fix committed to master branch. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2014-07-08 14:26 | correnson | New Issue | |
2014-07-08 14:26 | correnson | Status | new => assigned |
2014-07-08 14:26 | correnson | Assigned To | => correnson |
2014-08-21 09:07 | patrick | Description Updated | View Revisions |
2014-08-21 09:12 | patrick | Note Added: 0005409 | |
2014-08-21 09:53 | patrick | Description Updated | View Revisions |
2014-08-21 09:55 | patrick | Note Edited: 0005409 | View Revisions |
2014-08-21 10:12 | patrick | Description Updated | View Revisions |
2014-08-21 10:18 | patrick | Description Updated | View Revisions |
2014-08-21 10:19 | patrick | File Added: bts1828_frame.i | |
2014-08-21 10:20 | patrick | Note Edited: 0005409 | View Revisions |
2014-09-15 10:11 | correnson | Source_changeset_attached | => framac master 7a6aae68 |
2014-09-15 10:11 | patrick | Source_changeset_attached | => framac master 9c44791c |
2014-09-15 10:11 | patrick | Note Added: 0005455 | |
2014-09-15 10:11 | patrick | Assigned To | correnson => patrick |
2014-09-15 10:11 | patrick | Status | assigned => resolved |
2014-09-15 10:11 | patrick | Resolution | open => fixed |
2015-03-17 22:17 | signoles | Fixed in Version | => Frama-C Sodium |
2015-03-17 22:18 | signoles | Status | resolved => closed |