--- layout: fc_discuss_archives title: Message 70 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)



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                    |