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] problems with plugin-integration

  • Subject: [Frama-c-discuss] problems with plugin-integration
  • From: jean.nicolas at gmx.de (Jean-Pierre Nicolas)
  • Date: Thu, 16 Sep 2010 07:46:28 +0200
Hello,

I've installed frama-c on Ubuntu Lucid Lynx 10.04
I wanted to make a simple plugin "hello_world" like in the description of the documentation "plugin-developer-Boron-20100401.pdf" with the two files Makefile and hello_world.ml
After copying the sources of the documentation and saving both in the folder /home/jean-pierre/Bureau/ocamldoc/ i started the terminal, went to the folder and wrote "make". the terminal said:


jean-pierre at jean-pierre-laptop:~/Bureau/ocamldoc$ make
/usr/share/frama-c/Makefile.dynamic:180: .depend: Aucun fichier ou dossier de ce type
ocamlc.opt -c -I . -w Ael -warn-error A -annot -g -I /usr/lib/frama-c hello_world.ml
File "hello_world.ml", line 12, characters 14-18:
Warning Z: unused variable name.
File "hello_world.ml", line 3, characters 3-119:
Error: Signature mismatch:
       Modules do not match:
         sig val name : string val shortname : string val deser : string end
       is not included in
         sig val name : string val shortname : string val descr : string end
       The field `descr' is required but not provided
make: *** [hello_world.cmo] Erreur 2

what is the problem?

And than I've got another question.
I'm interested in the structure of the file metrics.ml
how does it work? 
it isn't possible to watch the source code of metrics.ml which is used in
Frama-C.
But for my analysation, i need to know why the framework Frama-C change
the C-code in another C-code and then verify the changed code?
I must verify the current C-code with all "switch, if, while, for, do
while, ..." and let it print on the screen.

Thanks,
Jean-Pierre

-- 
Neu: GMX De-Mail - Einfach wie E-Mail, sicher wie ein Brief!  
Jetzt De-Mail-Adresse reservieren: http://portal.gmx.net/de/go/demail