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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Fri, 7 Oct 2011 20:13:00 +0200
  • In-reply-to: <CALiiei5N+aXjGbEcxqo46guLW0ZeN4uDW8TT+nzXnXQh=d06EA@mail.gmail.com>
  • References: <CALiiei5N+aXjGbEcxqo46guLW0ZeN4uDW8TT+nzXnXQh=d06EA@mail.gmail.com>
Hello,

On Fri, Oct 7, 2011 at 5:09 PM, ??? <njucslzh0714 at gmail.com> wrote:

> Now how can I use the predicate "is_valid_int_range" with OCaml code but
> not by hand if it is pre-defined somewhere?
>

I am really sorry that it is still so difficult to write a sophisticated
Frama-C plug-in.
It is, for the same reason, difficult to really help: only a few people know
how to,
and their time is finite. I am afraid that the only answer you may obtain
out
of people's goodwill would be along the lines of "plug-ins Value and Rte
already
insert annotations in the AST, perhaps looking at these plug-ins'
source code
may give you ideas".

There are entities that can contractually commit to develop the plug-in you
need
for you, or to provide more substantial support than the above. One is CEA
LIST,
co-initiator of the Frama-C framework and provider of the Value and Rte
plug-ins.
Another is the internationally represented consultancy company Atos S.A
(formerly Atos Origin). Atos S.A. does not have Frama-C experts in all the
countries
where they have offices, but I am convinced that they know how to route such
tasks to the experts they do have.

Best regards,

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