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] Plugin Development Guide

  • Subject: [Frama-c-discuss] Plugin Development Guide
  • From: benjamin.monate at cea.fr (Benjamin Monate)
  • Date: Thu Oct 9 11:03:00 2008
  • In-reply-to: <1223480262.18514.86.camel@imladris>
  • References: <1223480262.18514.86.camel@imladris>
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              |