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] WP plugin / question about address of variable on stack

Hi,

> I have not an answer to your question but I would like to understand why you
> require that the arguments of swap are not zero.
> Is it not enough that they are valid pointers?

It all depends what a "valid" pointer is for Frama-C. I could not
found a good description, nor the deductive rules used.
Do you have pointers?

The validity of the value of a pointer is something really context
dependent. In most of the cases, the mapping of the address NULL is
set up so that accessing its content throws an internal processor
exception. But it may very well be that 0 be a valid address to
dereference, in the context of microprocessors or OS (think interrupt
handlers).

> At least, this is what we thought when we specified swap in section 6.2 of
> our "ACSL by Example" document
> http://www.first.fraunhofer.de/fileadmin/FIRST/ACSL-by-Example.pdf .

This document is great, thanks. I was not aware of your work with Frama-C.

I hope that somebody will be able to help me with this issue, though.
Please!

Thanks,
Sylvain Nahas


> Regards
>
> Jens
>
> On 17 Oct 2011, at 09:21, sylvain nahas wrote:
>
>> Hi,
>>
>> I am exercising the WP Frama-C plugin, and stumbled onto the following problem.
>>
>> Consider:
>>
>> ------------------------------------------------------------------------------
>> /*@ requires val1_valid: \valid(val1) && ( val1 != \null );
>> ?@ requires val2_valid: \valid(val2) && ( val2 != \null );
>>
>> ?@ ensures C: *val1 == \old(*val2) ;
>> ?@ ensures D: *val2 == \old(*val1) ;
>>
>> ?@ assigns *val1,*val2 ;
>> @*/
>>
>> void swap(int *val1,int *val2)
>> {
>> ? ? ? int tmp = *val1;
>> ? ? ? *val1 = *val2;
>> ? ? ? *val2 = tmp;
>> }
>>
>> /*@ assigns \nothing ; */
>> void call_swap()
>> {
>> ? ? ? int a = 1;
>> ? ? ? int b = 2;
>> ? ? ? /*@ assert A_is_valid: \valid(&a); */
>> ? ? ? /*@ assert A_is_not_null: &a != \null; */
>> ? ? ? /*@ assert B_is_valid: \valid(&b); */
>> ? ? ? /*@ assert B_is_not_null: &b != \null; */
>> ? ? ? swap(&a, &b);
>> }
>> ------------------------------------------------------------------------------
>> [ Partial ] Pre-condition 'val1_valid' in 'swap' at call 'swap' (file
>> swap.c, line 38)
>> ? ? ? ? ? ?By WP-Store, with pending:
>> ? ? ? ? ? ? - Assertion 'A_is_not_null' (file swap.c, line 35)
>> ? ? ? ? ? ? - Assertion 'B_is_not_null' (file swap.c, line 37)
>> ------------------------------------------------------------------------------
>>
>> I can get only a partial proof of the code above, whereas IMO it could
>> be completely validated.
>>
>> As I understand the issue, the WP plugin can not deduce from the fact
>> a variable is declared on the function's stack that a pointer that
>> references its address is not null.
>>
>> Is it so? What are the recommended practice in this case to get a full
>> certification of the code?
>>
>> BTW, I could not find in the ACSL doc. a clear/formal description of
>> what \valid means. Is there one?
>>
>> Thanks much in advance,
>> Sylvain Nahas
>>
>> _______________________________________________
>> 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
>
>
> _______________________________________________
> 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
>