--- layout: fc_discuss_archives title: Message 68 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C/Jessie: assigning a pointer with a formal parameter (of type pointer)



Hi,

The first VC is not proved because it is wrong: assigns clause are 
evaluated in the pre-state by default, so assigns *(p->rc) means that 
the cell pointed by p->rc IN THE PRE_STATE is modified.

You should use

   assigns *\at(p->rc,Post), p->rc

However, I just checked and the Post label is not yet well handled by 
Jessie. It can be probably solved easily...

So, if you want to fill a bug report, fill it by asking for a full 
support by the Post label in jessie...


- Claude

Pariente Dillon wrote:
> 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
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |