--- layout: fc_discuss_archives title: Message 108 from Frama-C-discuss on September 2013 ---
[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
>