Requires of behaviors lost
ID0001035: This issue was created automatically from Mantis Issue 1035. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001035 | Frama-C | Plug-in > wp | public | 2011-11-30 | 2012-01-24 |
| Reporter | yakobowski | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | - |
Description :
The wp currently loses 'required' clauses attached to a behavior. The example below can be used to test this; the access to *p should be proven valid.
Cmdline : frama-c -wp -wp-rte
/*@ behavior p: assumes x == 1; requires \valid(p); behavior q: assumes x!= 1; disjoint behaviors; */ void f(int x, int *p) { if (x == 1) *p = 1; }