Frame Validity
ID0001828: This issue was created automatically from Mantis Issue 1828. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001828 | Frama-C | Plug-in > wp | public | 2014-07-08 | 2015-03-17 |
| Reporter | correnson | Assigned To | patrick | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Sodium |
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); }