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] How to use a predicate with OCaml code but not by hand?

  • Subject: [Frama-c-discuss] How to use a predicate with OCaml code but not by hand?
  • From: njucslzh0714 at gmail.com (刘自恒)
  • Date: Fri, 7 Oct 2011 23:09:32 +0800
Hi,

   First, an example as below:

/*@
   predicate is_valid_int_range(int* p, int n) =
           (0 <= n) && \valid_range(p,0,n-1);

   lemma foo: \forall int* p,n; is_valid_int_range(p,n) <==>
\valid_range(p,0,n-1);

*/

/*@
   requires is_valid_int_range(a, n);
   requires is_valid_int_range(b, n);

   assigns \nothing;

   behavior all_equal:
     assumes \forall int i; 0 <= i < n ==> a[i] == b[i];
     ensures \result == 1;

   behavior some_not_equal:
     assumes \exists int i; 0 <= i < n && a[i] != b[i];
     ensures \result == 0;

   complete behaviors all_equal, some_not_equal;
   disjoint behaviors all_equal, some_not_equal;
*/
int equal(const int* a, int n, const int* b)
{
  for (int i = 0; i < n; i++)
          if (a[i] == b[i])
          {
            count = count + 1;
              }

       return count;
}


Now how can I use the predicate "is_valid_int_range" with OCaml code but not
by hand if it is pre-defined somewhere? That is the annotations such as
"requires is_valid_int_range(a, n);" can be generated automatically. Its
name and its profile have been extracted.

Best Wishes.

Henry
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111007/40bbc45f/attachment.htm>