\at(...,Post) in assigns clause
ID0000160: This issue was created automatically from Mantis Issue 160. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000160 | Frama-C | Plug-in > jessie | public | 2009-06-22 | 2014-02-12 |
| Reporter | dpariente | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Beryllium-20090601-beta1 |
Description :
"at"'s labels support in assigns clause is needed in Jessie to be able to discharge all behavioral POs from the following annotated test code:
typedef struct { int * rc; } S;
/*@ requires \valid(p) && \valid(p->rc) && \valid(r); assigns \at(p->rc,Post),p->rc; / int main1( S p,int r) {p->rc = r; *(p->rc) = 55; return 1; }
//Command-line: frama-c -jessie-analysis e28.c