--- layout: fc_discuss_archives title: Message 93 from Frama-C-discuss on September 2013 ---
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 e-mail:DRAGANST at ie.ibm.com IBM Technology Campus Damastown Industrial Estate Mulhuddart Dublin 15 Ireland -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130913/35d39bbc/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: swap-jessie.tar.gz Type: application/x-gzip Size: 48307 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130913/35d39bbc/attachment-0001.bin>