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)

Indeed a surprising example, but it can be explained after all. Let me 
recall the semantics of assigns clauses from the ACSL document:

   assigns L

means that any memory location that is allocated in the pre-state and 
that do not belong to the set L remains unchanged.

Thus: since &x is not allocated in the pre-state, this function only 
modifies *one* memory location of the pre-state, that is p->rc, then any 
assigns clause containing at least
p->rc is correct. You can try just the clause

assigns p->rc;

and it is proven valid too.

Please try to think about assigns clause from the client's point of 
view: if any code calls main1(p,r) then it can only observe the side 
effect on p->rc, and not on *(p->rc) which is not an allocated memory 
location.


- Claude


Dillon Pariente wrote:
> Thank you Claude for your answer!
> 
> (Indeed, assigns state was different with Caduceus => my old 
> non-regression examples have to be deeply revisited!)
> 
> Now, BTS is enriched with \at(...,Post) support demand.
> 
> By the way, would you mind explaining why the following annotated code 
> POs are fully discharged?
> The difference with the previous one is that a *dangling* pointer is 
> used instead of the second parameter.
> 
> /*=========================*/
> typedef struct { int * rc; } S;
> 
> /*@
> requires \valid(p)
>    && \valid(p->rc)
>    && \valid(r);
> assigns *p->rc,p->rc;
> */
> int main1(  S* p,int* r)
> { int x;
>   p->rc = &x;
>   *(p->rc) = 55;
>   return 1;
> }
> /*=========================*/
> /*
> frama-c -jessie-analysis <file>.c
> */
> 
> Thanks in advance for your comments!
> Dillon
> 
>> 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;
>  > }
>  > /*=========================*/
> 
> 
> 
> _______________________________________________
> 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                    |