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