--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on September 2010 ---
Hello, -------- Message d'origine-------- De: frama-c-discuss-bounces at lists.gforge.inria.fr de la part de Jean-Pierre Nicolas Date: jeu. 16/09/2010 07:46 > 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? Where did you get the sources from? The issue is that your hello_world.ml defines a value named deser instead of the descr expected by the Plugin.Register functor. It smells very much like a typo, but it is neither present in the manual nor in src/dummy/hello_world.ml referenced from there. > 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. The code for the metrics plugin is located in src/metrics: metrics_parameters.ml defines the option of the plugin, register.ml performs the computation (and registers its entry point within the kernel), and register_gui.ml installs the corresponding gui components. > 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. Most Frama-C's operations operate on the elaborated AST, where type-checking, name resolution, and a few normalization steps have occured. There is also an untyped AST, which reflects exactly the original syntax of the code (modulo pre-processing, which occurs entirely outside of Frama-C). It is defined in cil/src/frontc/cabs.ml, with a visitor in cil/src/frontc/cabsvisit.ml. The pretty-printer for cabs (in cil/src/frontc/cprint.ml) has been unmaintained for a long time, but the next version of Frama-C should be much better in this regard. Hope this helps, -- Virgile Prevosto Ing?nieur-Chercheur CEA, LIST, Laboratoire des logiciels s?rs -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: non disponible Type: application/ms-tnef Taille: 4224 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100916/e14a4e6b/attachment.bin>