--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on October 2011 ---
[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?



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>