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 ]
IDProjectCategoryView StatusLast Update
0001067Frama-CDocumentation > manualspublic2016-06-21 14:20
Assigned Topascal 
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 +




Jochen (reporter)

File "cmpOpts" lists all options I found, with "M" meaning "found in manual", and "H" meaning "found in option -value-help".


Jochen (reporter)

Some of the options in M\H are seemingly kernel options.


signoles (manager)

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.


pascal (reporter)

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


pascal (reporter)

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