--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on June 2009 ---
Hello, (The following issue was discussed earlier with some of you, but I don't think it is resolved nor recorded into the BTS) In the following annotated code: /*=========================*/ typedef struct { int * rc; } S; /*@ requires \valid(p) && \valid(p->rc) && \valid(r); assigns *(p->rc),p->rc; */ int main1( S* p,int* r) { p->rc = r; *(p->rc) = 55; return 1; } /*=========================*/ no ATP is able to discharge the first PO, with command-line: frama-c -jessie-analysis file.c Please confirm if this is a feature (code+this kind of assigns clause) not yet available in Jessie, and that there is no ... particular tricking issue!? If so, I'll add a record into the BTS for traceability. Thanks in advance! Best regards, Dillon PARIENTE -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090622/fb23dbc0/attachment.htm