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 limit ?

  • Subject: [Frama-c-discuss] Frama-C limit ?
  • From: Emilie.Timbou at continental-corporation.com (Emilie.Timbou at continental-corporation.com)
  • Date: Mon, 15 Jun 2009 16:49:27 +0200
Bonjour 
J'ai un gros projet qui comporte ? peu pr?s un millier de headers  et 
autant de fichiers C.
J'ai besoin d'utiliser les prouvers avec le plug-in Jessie sur un fichier 
contenu dans ce projet. (test.c)
Le probl?me c'est que le fichier C ?tudi? fait appel ? tous les autre 
fichiers C du projet, ce n'est pas moi qui est ?crit les diff?rents 
programmes et donc je ne peux pas les modifier.

-->     J'ai donc test? la ligne de commande  "frama-c  -jessie-analysis 
-jessie-gui test.c " 
                => test.c ?tant le fichier sur lequel je voudrais 
travailler
Cette simple ligne de commande me donne comme erreur:
        "> No code for function  __clz, default assigns generated
         > No code for function ..... , default assigns generated
         > ....
         > Fatal error: exception Assert_failure ("src/jessie/rewrite.ml, 
219, 3) " 

-->     J'ai donc test? par la suite la ligne de commande "frama-c 
-jessie-analysis -jessie-gui  *.c"
Cette ligne de commande analyse tous les fichiers contenus dans le projet 
Elle me donne comme erreur:
        "> Fatal error: exception Failure ("Buffer.add: cannot grow 
buffer")


-->     J'ai test? la ligne de commande " frama-c-gui -val  test.c"
        "> Could not find entry point : main "
La fen?tre de Frama-C s'ouvre. Par contre, le fichier ne contient pas de 
"main ", du coup, il ne pas lancer la Value Analysis ==> tout ? fait 
normal.
        En fait, dans l'interface de Frama-c, il y a la liste de tout les 
headers n?cessaire pour faire fonctionner le programme sauf que les appel 
de fonction sont surlign? en orange et barr?. Il serait peut ?tre 
judicieux de mettre les fichiers C correspondant afin de verifier que cel? 
puisse fonctionner, c'est ? dire que les fichiers C list?s dans 
l'interface graphique


-->     J'ai test? la ligne de commande "frama-c-gui -val *.c"
Cette ligne de commande est valide et analyse tous les fichiers pr?sents 
dans le projet.
Cette ligne me donne comme erreur:
        "> Fatal error: exception Invalid_argument (Array.make")"


QUESTION:
1) Faire appel seulement au fichier dont j'ai besoin ne me permet pas de 
l'?tudier car Frama-C ne connaitra pas toutes les fonctions appel?es par 
le programme pour son ex?cution, est ce une bonne id?e de faire passer 
tous les fichiers dans Frama-C ?

2) Apparemment d'apr?s les message d'erreurs obtenu lors de mes diff?rents 
test, Frama-C ne peut pas tenir compte de tous les fichiers pr?sents dans 
le r?pertoire, il ne que prendre  que 98 fichiers C. 
N'aurai t'il pas un autre moyen de faire passer tous les fichiers? ou 
serai-ce une limite de l'outil ?

3) Dans le forum de discussion, je n'ai pas trouv? d'exemple ayant fait 
appel ? l'option " - jessie-project-name <s>" , pourrai-je avoir un 
exemple d'appel ?

Cordialement,


P.S : Je fais appel ? vous en priorit? en fran?ais afin d'avoir une 
r?ponse assez rapidement et je le fais en fran?ais pour bien me faire 
comprendre.. Je posterai sur le forum de discussion en anglais par la 
suite afin de partager mon soucis.
-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090615/f6cc1583/attachment.htm