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