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] [Why3-club] PVS TCC problem

This is now fixed in commit 62029d7743d6.
--
Jean-Christophe


On 13/09/2013 20:49, Claude Marche wrote:
>
> You're right this is a bug in the printer for PVS. It definitely should
> translate any Why3 type into TYPE+. Thanks for noticing and reporting,
> this will be fixed asap.
>
> - Claude
>
> On 09/13/2013 11:32 AM, Dragan wrote:
>> Hi all,
>>
>> I have tried to discharge PVS theorem(s) and obligation generated by
>> frama-c-Oxygen -> why2/jessie -> why3 -> PVS using simple example
>> written in c language.
>> *void swap( int *a , int *b)*
>> *{*
>> *  int tmp = *a;*
>> *  *a = *b;*
>> *  *b = tmp;*
>> *  return;*
>> *}*
>> *
>> *
>> */*@ requires \valid(a) &&  \valid(b);*
>> *  @ ensures A: *a==\old(*b); *
>> *  @ ensures B: *b==\old(*a);*
>> *  @ assigns *a,*b;*
>> *  @*/*
>> * *
>> *void swap( int *a, int *b );*
>>
>> There is something interesting I found in *jessie->PVS transformation
>> and* I think this is important to report.
>> I have successfully proved
>> theorem  *wp_parameter_swap_ensures_default *generated automatically.
>> However I cannot discharge TCC:
>> *select_TCC1[t: TYPE, v: TYPE]: OBLIGATION*
>> *  EXISTS (x2: [[memory[t, v], pointer[t]] -> v]): TRUE;*
>> All axioms provided above definition
>> *select[t: TYPE, v: TYPE](x: memory[t, v], x1: pointer[t]): v*
>> seemed to me are not suitable for discharging this obligation.
>> Then I have contacted Sam Owre and we agreed with the following:
>> The problem is that as it stands, the TCC is actually false.
>> This is because v is a simple type parameter that can be instantiated to
>> any type, including an empty one, whereas the argument types for select
>> are guaranteed to be nonempty.
>> The easiest fix if this was a manually written spec is to change
>> the declaration for select to
>>
>> select[t: TYPE, v: TYPE+](x: memory[t, v], x1: pointer[t]): v
>>                         ^
>>       Note the *'+'* here !
>>
>> (or perhaps change memory to be empty if v is and nonempty otherwise,
>> but this is probably more difficult).  I think what is going on
>> here is that* Why2/jessie-Why3  assumes all types to be nonempty,
>> whereas PVS
>> doesn't share that assumption. *
>>
>> When I added that* '+'* myself, I got no TCCs.
>> Please find attached tar.gz ( notice that example
>> contain *int* and *real* lib (provided by *Why3*) included as well ).
>>
>> Another important thing :
>> There are several problems I found during installation  why3 and PVS.
>> So I am going to write installation note with all corrections that needs
>> to be done.
>>
>> Regards
>>
>> --
>> Dragan Stosic
>> Senior developer at IBM
>> phone: 085-773-1050
>> e-mail: dragan.stosic at gmail.com <mailto:dragan.stosic at gmail.com>
>> e-mail:DRAGANST at ie.ibm.com <mailto:e-mail%3ADRAGANST at ie.ibm.com>
>> IBM Technology Campus
>> Damastown Industrial Estate
>> Mulhuddart
>> Dublin 15
>> Ireland
>>
>>
>> _______________________________________________
>> Why3-club mailing list
>> Why3-club at lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>>
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>