--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ask for slicing spec



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