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

  • Subject: [Frama-c-discuss] ask for slicing spec
  • From: jshen.cn.sh at gmail.com (jun shen)
  • Date: Thu, 5 Nov 2009 22:44:48 -0700
  • In-reply-to: <e4a09de30909251853i52e44551t4681529738e60642@mail.gmail.com>
  • References: <e4a09de30909251853i52e44551t4681529738e60642@mail.gmail.com>
Hello,

I have one question about the usage of frama-c.

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

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?

If my description is not clear, let me know.
-- 
Regards,
Jun
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091105/d2697253/attachment.htm