--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on November 2009 ---
Hello, jun shen a ?crit : > After looking at the testcode, I find that the only way to use frama is > to write my ocaml application like those test examples and then build > the application into binaries and run it. I'm not sure of what "testcode" you are talking about. Anyway, you can use Frama-C either from its graphical user interface or from its batch mode. If you have in mind to use Frama-C programmatically for developing your own analyzer, the simplest way is to write an external plug-in dynamically loaded by Frama-C. For this purpose, you should have a look at the Plug-in Development Guide for a tutorial and extended details: http://frama-c.cea.fr/download/plugin-developer-Beryllium-20090902.pdf > I wonder whether it is possible to use frama-c as a library, together > with external CIL (for the sake of CIL update). This seems to be > impossible because frama-c changes the CIL API to some extent. Am I > correct? One of the goals of Frama-C is to provide a library for developing new analyzers. But you're correct: Frama-C comes with its own version of CIL which is not compatible with the official Berkeley's version of CIL. > In other words, if some program is using CIL standard API, can it > interoperate with frama-c? e.g. will the sid of one specific statement > vary between standard CIL interpretation and frama-c's? No there are no such guarantees. Hope this helps, Julien Signoles