Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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                    |