2021-01-15 15:25 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001731Frama-CDocumentationpublic2016-06-21 14:17
Assigned Tosignoles 
PlatformAllOSAllOS VersionAll
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001731: Erreur dans la documentation pour plugin contradiction sur nom de fichiers
DescriptionDans 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 Hello_options.ml mais le module référencé est Hello_register et non Hello_options
Steps To ReproduceLire 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.
Additional InformationChanger le fichier Hello_options.ml en fichier Hello_register.ml sera moins couteux que d'aller changer les Hello_register.* dans le code source.
TagsNo tags attached.
Attached Files




signoles (manager)

Last edited: 2014-04-07 11:45

View 2 revisions

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.


zuy (reporter)

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
  let name = 'hello world"
  let shortname = "hello"
  let help = help_msg

But in hello_print.ml 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...


signoles (manager)

Fix committed to master branch.


signoles (manager)

Thanks for the report. Fixed in the development version.

-Issue History
Date Modified Username Field Change
2014-04-05 10:41 zuy New Issue
2014-04-05 10:41 zuy Status new => assigned
2014-04-05 10:41 zuy Assigned To => signoles
2014-04-07 11:33 signoles Note Added: 0005028
2014-04-07 11:33 signoles Status assigned => feedback
2014-04-07 11:45 signoles Note Edited: 0005028 View Revisions
2014-04-07 14:55 zuy Note Added: 0005031
2014-04-07 14:55 zuy Status feedback => assigned
2014-04-07 15:15 signoles Source_changeset_attached => framac master 1eeb9b8c
2014-04-07 15:15 signoles Note Added: 0005032
2014-04-07 15:15 signoles Resolution open => fixed
2014-04-07 15:15 signoles Note Added: 0005033
2014-04-07 15:15 signoles Status assigned => resolved
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:17 signoles Status resolved => closed
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
2016-06-21 14:17 signoles Category Documentation > ACSL => Documentation
+Issue History