--- layout: fc_discuss_archives title: Message 80 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] need frama-c help to develop plugin



Hello,

please use English when this list is among the recipients of your  
message.

> Nous devons d?velopper un plugin sous frama-c qui permet de modifier  
> un
> fichier source en langage C (on veut par exemple lui retirer des  
> lignes,
> enlever une instruction ...)
> L'int?ret pour nous d'utiliser frama-c est de profiter des plugins  
> d?j?
> incorpor?es ainsi que des fonctions de base comme obviously (on doit
> partir d'un fichier C dans le format g?n?r? par obviously).

To reassure non-French readers of this list, this sentence is hard to
parse even with the benefit of the language. Are you saying
that there exists something called "obviously" that is one of Frama-C's
base functionalities? Should we know about it? I googled
"obviously C transformation" and "obviously ensi bourges", and at this
point I have to concede that I don't know...

Frama-C transforms the C source in an Abstract Syntax Tree on which
it is possible to do analyses. It is possible to print back the AST into
a C program, but the result is never going to be exactly like the  
original with
removed lines or statements. Just getting a file that is syntactically
correct C may be difficult if you intend to remove some constructs.

A rather simple C transformation plug-in that you can use for  
inspiration
is the so-called "semantic constant folding" plug-in that substitutes
constant expressions by their values. You can find it in
.../src/constant_propagation. A less simple C transformation plug-in
is the Slicing plug-in. You may have to use some of the latter's  
building
blocks, especially the Program Dependency Graph.

> Probl?me principal pour l'instant : malgr? la doc, nous n'arrivons  
> pas ?
> comprendre le fonctionnement de frama-c au niveau de la lecture du  
> fichier
> source.

The point of writing a Frama-C plug-in is that you don't have to  
understand
how it reads input files. If it is acceptable for you to have the  
input files
go through the AST representation before being output again,
concentrate on understanding how to manipulate the AST.

Pascal