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] 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