Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:12 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001067Frama-CDocumentation > manualspublic2012-01-19 14:252016-06-21 14:20
ReporterJochen 
Assigned Topascal 
PrioritynormalSeveritytrivialReproducibilityN/A
StatusclosedResolutionfixed 
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 - 
    -absolute-valid-range					M
-all-rounding-modes				H	M
-context-depth					H	M
-context-valid-pointers				H	M
-context-width					H	M
-cpp-command						M
-cpp-extra-args						M
-deps							M
-inout							M
-input							M
-lib-entry						M
-load							M
-machdep						M
-main							M
-memory-footprint				H
-no-overflow						M
-no-results					H	M
-no-results-function				H	M
-obviously-terminates				H
-obviously-terminates-function			H
-ocode							M
-out							M
-out-external						M
-pp-annot						M
-print							M
-propagate-top					H
-remove-redundant-alarms			H
-save							M
-separate-n					H
-separate-of					H
-separate-stmts					H
-slevel						H	M
-slevel-function				H	M
-subdivide-float-var				H
-ulevel							M
-undefined-pointer-comparison-propagate-all	H	M
-unsafe-arrays						M
-unspecified-access					M
-val						H	M
-val-after-results				H
-val-builtin					H
-val-ignore-recursive-calls			H
-val-print					H
-val-print-callstacks				H
-val-show-progress				H
-val-signed-overflow-alarms			H	M
-val-use-spec					H	M
-value-debug					H
-value-h					H
-value-help					H
-value-verbose					H
-wlevel						H
    ? file icon cmpOpts (1,118 bytes) 2012-01-19 14:40 +

-Relationships
+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.
+Notes

-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
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
2013-12-19 01:11 pascal Source_changeset_attached => framac master d6c5e92d
2014-02-12 16:54 pascal Source_changeset_attached => framac stable/neon d6c5e92d
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
+Issue History