Frama-C Bug Tracking System - Frama-C
View Issue Details
0001085Frama-CDocumentationpublic2012-02-08 10:512016-06-21 14:24
Reporterpascal 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001085: Cute boolean options too cute for their own good
Description$ bin/toplevel.opt -kernel-help
Description: General options provided by the Frama-C kernel

Most options of the form '-option-name' and without any parameter
have an opposite with the name '-no-option-name'.

***** LIST OF AVAILABLE OPTIONS:

*** ANALYSIS OPTIONS

...
-safe-arrays for arrays that are fields inside structs, assume that
                    accesses are in bounds (set by default)
...

There is no way to know that the option to unset this option is -unsafe-arrays
TagsNo tags attached.
Attached Files

Notes
(0002677)
signoles   
2012-02-08 14:04   
I agree that it would be better to give the non-standard opposite name (if any) of the option in its description.

Note however that you already get:
$ frama-c -kernel-help
...
-safe-arrays ...
...
-unsafe-arrays opposite of option "-safe-arrays"
...
(0002982)
yakobowski   
2012-04-29 14:44   
It seems there has been a regression following the resolution of this bug:

frama-c -kernel-help
[...]
-unsafe-arrays undocumented
(0002983)
signoles   
2012-04-29 20:20   
The regression probably comes from commit 18346 instead of 18359. Will be fixed tomorrow.

Issue History
2012-02-08 10:51pascalNew Issue
2012-02-08 10:51pascalStatusnew => assigned
2012-02-08 10:51pascalAssigned To => signoles
2012-02-08 14:04signolesNote Added: 0002677
2012-02-08 14:04signolesStatusassigned => acknowledged
2012-04-27 11:24svn
2012-04-27 11:24svnStatusacknowledged => resolved
2012-04-27 11:24svnResolutionopen => fixed
2012-04-29 14:44yakobowskiNote Added: 0002982
2012-04-29 14:44yakobowskiStatusresolved => feedback
2012-04-29 14:44yakobowskiResolutionfixed => reopened
2012-04-29 20:20signolesNote Added: 0002983
2012-04-30 09:47svn
2012-04-30 09:47signolesStatusfeedback => resolved
2012-04-30 09:47signolesResolutionreopened => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2013-12-19 01:11signolesSource_changeset_attached => framac master 19c3a925
2014-02-12 16:54signolesSource_changeset_attached => framac stable/neon 19c3a925
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL
2016-06-21 14:24signolesCategoryDocumentation > ACSL => Documentation