--- layout: fc_discuss_archives title: Message 11 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?



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>