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

  • Subject: [Frama-c-discuss] PVS TCC problem
  • From: dragan.stosic at gmail.com (Dragan)
  • Date: Fri, 13 Sep 2013 10:32:10 +0100
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>