--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problems with plugin-integration



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