Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001731Frama-CDocumentationpublic2014-04-05 10:412016-06-21 14:17
Reporterzuy 
Assigned Tosignoles 
PrioritylowSeveritytextReproducibilityalways
StatusclosedResolutionfixed 
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

- Relationships

-  Notes
(0005028)
signoles (manager)
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.

(0005031)
zuy (reporter)
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 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...
(0005032)
signoles (manager)
2014-04-07 15:15

Fix committed to master branch.
(0005033)
signoles (manager)
2014-04-07 15:15

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 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker