Frama-C Bug Tracking System - Frama-C
View Issue Details
0001731Frama-CDocumentationpublic2014-04-05 10:412016-06-21 14:17
Frama-C Neon-20140301 
Frama-C Sodium 
0001731: Erreur dans la documentation pour plugin contradiction sur nom de fichiers
Dans la documentation de développement de plugin "plugin-development-guide-N-X" notamment dans la documentation de plugin-development-guide-Neon-20140301 à la page 17, il est fait référence à la création d'un fichier mais le module référencé est Hello_register et non Hello_options
Lire la documentation et essayer de faire le tutoriel, on tombe sur une incohérence si on s'en tient à la lecture et probablement sur des bugs disant module not found si on copie colle pour tester.
Changer le fichier en fichier sera moins couteux que d'aller changer les Hello_register.* dans le code source.
No tags attached.
Issue History
2014-04-05 10:41zuyNew Issue
2014-04-05 10:41zuyStatusnew => assigned
2014-04-05 10:41zuyAssigned To => signoles
2014-04-07 11:33signolesNote Added: 0005028
2014-04-07 11:33signolesStatusassigned => feedback
2014-04-07 11:45signolesNote Edited: 0005028View Revisions
2014-04-07 14:55zuyNote Added: 0005031
2014-04-07 14:55zuyStatusfeedback => assigned
2014-04-07 15:15signolesNote Added: 0005032
2014-04-07 15:15signolesResolutionopen => fixed
2014-04-07 15:15signolesNote Added: 0005033
2014-04-07 15:15signolesStatusassigned => resolved
2015-03-17 22:17signolesFixed in Version => Frama-C Sodium
2015-03-17 22:17signolesStatusresolved => closed
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL
2016-06-21 14:17signolesCategoryDocumentation > ACSL => Documentation

2014-04-07 11:33   
(edited on: 2014-04-07 11:45)
I find no occurrence of Hello_register in the plug-in development guide. Could you please indicate more precisely where its (their) occurrence(s) is (are)? Also, the code snapshots of the tutorial are compiled against the corresponding Frama-C version [EDIT: they should be, but they were not in the most recent versions of Frama-C]. So they should at least compile without error.
2014-04-07 14:55   
The plugin development guide (Neon-20140301) specify a file named hello_options (to the middle of page 17) and contains : let help_msg = 'out a warm welcome message to the user' module Self = Plugin.Register (struct let name = 'hello world" let shortname = "hello" let help = help_msg end) But in file the module calling as parent of Self is Hello_register (i.e let print_hello () = Hello_register.Self.result 'Hello, World") instead of Hello_options.Self...
2014-04-07 15:15   
Fix committed to master branch.
2014-04-07 15:15   
Thanks for the report. Fixed in the development version.