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