Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001067Frama-CDocumentation > manualspublic2012-01-19 14:252016-06-21 14:20
ReporterJochen 
Assigned Topascal 
PrioritynormalSeveritytrivialReproducibilityN/A
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001067: suggest to mention option "-value-help" in value analysis manual
DescriptionIn an attempt to find out the list of all options to the value analysis plug-in, I manually collected all tt-Font text near an occurrence of the string "option" in the value analysis manual ("value-analysis-Nitrogen-20111001.pdf"). After that, I learned about the option "-value-help", which produces another option list. Neither list is contained in the other, but they have a large intersection.

I suggest to mention in the manual the option "-value-help" (and: that it explains some options not explained in the manual). Vice versa, the manual should be mentioned in the output of the "-value-help" option.

In the long run, of course, both option lists should be made equal.
TagsNo tags attached.
Attached Files? file icon cmpOpts [^] (1,118 bytes) 2012-01-19 14:40 [Show Content]

- Relationships

-  Notes
(0002597)
Jochen (reporter)
2012-01-19 14:42

File "cmpOpts" lists all options I found, with "M" meaning "found in manual", and "H" meaning "found in option -value-help".
(0002598)
Jochen (reporter)
2012-01-19 14:44

Some of the options in M\H are seemingly kernel options.
(0002600)
signoles (manager)
2012-01-19 15:00

Actually, since an option -<plugin-shortname>-help is provided for each Frama-C plug-in, it is documented in the general Frama-C User Manual (Section 3.3.2 "Getting Help").

But arguably it could also be documented in each plug-in manual.
(0002601)
pascal (reporter)
2012-01-19 15:08

- the value analysis manual aims to follow a didactic flow and will introduce options that aren't value analysis option but kernel options at the time when they fit in.

- some options listed by in -value-help are intended for advanced users. In fact, all options listed in -value-help and not documented in the value analysis manual are to some extent intended for advanced users.

I could make an index of options in the value analysis manual. This index would refer to uses or descriptions of each option, again regardless of whether it is actually a kernel or value analysis option.
(0004675)
pascal (reporter)
2014-02-12 16:58

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2012-01-19 14:25 Jochen New Issue
2012-01-19 14:25 Jochen Status new => assigned
2012-01-19 14:25 Jochen Assigned To => signoles
2012-01-19 14:40 Jochen File Added: cmpOpts
2012-01-19 14:42 Jochen Note Added: 0002597
2012-01-19 14:44 Jochen Note Added: 0002598
2012-01-19 15:00 signoles Note Added: 0002600
2012-01-19 15:01 signoles Assigned To signoles => pascal
2012-01-19 15:08 pascal Note Added: 0002601
2012-01-26 10:47 svn Checkin
2012-01-26 10:47 svn Status assigned => resolved
2012-01-26 10:47 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2014-02-12 16:58 pascal Note Added: 0004675
2014-02-12 16:58 pascal Status closed => resolved
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
2016-06-21 14:20 signoles Category Documentation > ACSL => Documentation > manuals


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker