--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Plugin Development Guide



Hi David,

David DELMAS a ?crit :
> I read the Plugin Development Guide with great interest. It is a good
> point to be able to write specific plugins implementing semantic
> analyses, but also syntactic checks.

Yes even if Frama-C's main goal is to develop semantic analysers, you 
can use the framework to encode most of the syntactic coding rules 
available in lint like tools.
Your plugin would be a very good starting point for anyone trying to 
implement its custom syntactic rules.
Thanks for showing it in public.

> However, I am not very familiar with OCaml yet. To get started, I tried
> to implement a few simple syntactic checks in the attached file. Could
> you please tell me if this is an appropriate way to implemented such
> things? If you have advice on how to better use the platform, please let
> me know.

Your code seems correct. You should probably mention in the header the 
targetet version of Frama-C. Your plugin works with the unreleased 
Lithium-20081001+alpha1 version.

> By the way, I have a hard time finding all the information about APIs. I
> mainly browse through HTML files generated by "make doc". Is more
> documentation available?

Besides the documentation generated in doc/html/index.html from the 
headers, you have the developer and architecture manuals 
(frama-c-architecture.pdf and plugin-dev.pdf).
Good entry points are db.mli, cil.mli and cil_types.mli.
We will try to improve this generated documentation.


Cheers,
-- 
| Benjamin Monate         | mailto:benjamin.monate@cea.fr     |
| Ing?nieur-Chercheur     | CEA-LIST/DRT/DTSI/SOL/LSL         |
| B?t. 528 Pt. 115a       | 91191 Gif-sur-Yvette CEDEX        |
| T?l. 01 69 08 94 09     | Fax : 01 69 08 83 95              |