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] Frama-C plug-in

  • Subject: [Frama-c-discuss] Frama-C plug-in
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Wed, 30 Nov 2011 16:09:24 +0100
  • In-reply-to: <1322661567.3940.98.camel@iti27.informatik.htw-dresden.de>
  • References: <1322661567.3940.98.camel@iti27.informatik.htw-dresden.de>
Hello Boris,

First I send my answer on Frama-C discuss for the sake of dissemination 
and saving.

Second I assume from now that you are using Frama-C Nitrogen-20111001 
which is the latest public available version of Frama-C.

On 11/30/2011 02:59 PM, Boris Hollas wrote:
> I want to write a Frama-C plugin that adds postconditions to functions.
> Eg, for the function
>
> void foo(bar *this) {
> this->x = 0;
> }
>
> I want to add the postcondition
>
> ensures this->x == 0;
>
> I assume that Frama-C provides an AST so I needn't write my own parser.

You're right.

> However, the plug-in-developer manual doesn't describe how to access the
> AST and how to insert postconditions so that other plug-ins such as WP
> or Jessie can use them.  First of all, is writing a plug-in the right
> approach for my purpose?

Yes it is.

More important, where can I get the required
> information?

 From the developer point of view, Frama-C is an huge library where it 
is arguably difficult to find what you want.

The Plug-in Development Guide is an useful source of information, but it 
is unfortunately partially out-of-date and we [the Frama-C development 
team] have no time nor funding to update it (by being the main author of 
the original version of this manual, my personal estimation is that the 
update would require several men.month of work to get a decent 
maintainable result [1]).

Are there other manuals, example code?

Example of code may be found in the open-source release: you can read 
the source of the plug-in you are interested in. Of course, code of 
complex plug-in like WP is much more difficult to understand than the 
code of a lightweight plug-in like Occurrence. Furthermore there is 
usually only few documentation about implementation details because we 
only write the minimal useful comments for the 1, 2 or 3 Frama-C 
developers who maintain each module. Unfortunately, as far as I know, 
there is no open-source plug-in which extends function contract.

Another source of documentation is the Frama-C API available in HTML 
format as a single tarbal at 
frama-c.com/download/frama-c-Nitrogen-20111001_api.tar.gz. In our team, 
many of us prefer to have a direct look at the .mli file (module 
interface) by using their favorite text editor: anyway the contents is 
pretty much the same, except that the HTML files hide internal values 
useless for any plug-in developers.

By reading the index of these HTML pages, you can see that there is a 
module Ast which provides an access to the Frama-C AST. This AST is 
extensively described in module Cil_types. Here you can find that the 
type of C functions extended by its ACSL contract is called 
kernel_function. The documentation says that it is a record with mutable 
fields, but you must use module Kernel_function to safely access it, 
especially via Kernel_function.get_spec and Kernel_function.set_spec. 
This last function was only introduced in Frama-C Nitrogen and you must 
use it to add your new postcondition. It is a higher-order function 
which takes as argument the way you want to modify the old contract. 
Maybe the simplest way to provide this information is to use a Frama-C 
visitor. Visitors are well described in the Frama-C Plug-in Development 
Guide and they are several examples of use in the Frama-C sources.

Hope this helps,
Julien

[1] A step in the direction of maintainability would be to have an 
applicant to the last internship described here : 
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:positions#internships...