--help fails with an exception

[fpoli]

Executing silicon --help fails with an exception. Also:

• The formatting of the description of some options is broken (--proverSaturationTimeoutWeights, --stateConsolidationMode, --z3SaturationTimeoutWeights).
• -Llogger=level is indented in a different way.
• The description of --numberOfParallelVerifiers misses a ).
• I'd increase the maximum line length; the right column is quite narrow. I'd also put a newline between different options.

Output of silicon --help:

Silicon 1.1-SNAPSHOT (09888100@(detached))
Usage: Silicon [options] <file>

Options:
      --alternativeFunctionVerificationOrder       Calculate the order in which
                                                   functions are verified and
                                                   function axioms become
                                                   available in an alternative
                                                   way that takes dependencies
                                                   between functions through
                                                   predicate unfoldings into
                                                   account. This is more
                                                   complete in some cases (see
                                                   Silicon issue #355) but less
                                                   complete in others (see test
                                                   all/issues/silicon/unofficial007).
      --assertionMode  <arg>...                    Determines how assertion
                                                   checks are encoded in SMTLIB.
                                                   Options are 'pp' (push-pop)
                                                   and 'cs' (soft constraints)
                                                   (default: cs).
      --assertTimeout  <arg>                       Timeout (in ms) per SMT
                                                   solver assertion (default: 0,
                                                   i.e. no timeout).Ignored when
                                                   using the cvc5 prover.
      --assumeInjectivityOnInhale                  Assumes injectivity of the
                                                   receiver expression when
                                                   inhaling quantified
                                                   permissions, instead of
                                                   checking it.
      --checkTimeout  <arg>                        Timeout (in ms) per SMT
                                                   solver check. Solver checks
                                                   differ from solver asserts in
                                                   that a failing assert always
                                                   yields a verification error
                                                   whereas a failing check
                                                   doesn't, at least not
                                                   directly. However, failing
                                                   checks might result in
                                                   performance degradation, e.g.
                                                   when a dead program path is
                                                   nevertheless explored, and
                                                   indirectly in verification
                                                   failures due to
                                                   incompletenesses, e.g. when
                                                   the held permission amount is
                                                   too coarsely
                                                   underapproximated (default:
                                                   10).Ignored when using the
                                                   cvc5 prover.
      --conditionalizePermissions                  Potentially reduces the
                                                   number of symbolic execution
                                                   paths, by conditionalising
                                                   permission expressions. E.g.
                                                   rewrite "b ==> acc(x.f, p)"
                                                   to "acc(x.f, b ? p :
                                                   none)".This is an
                                                   experimental feature; report
                                                   problems if you observe any.
      --counterexample  <arg>                      Return counterexample for
                                                   errors. Pass 'native' for
                                                   returning the native model
                                                   from the backend, 'variables'
                                                   for returning a model of all
                                                   local Viper variables, or
                                                   'mapped' (only available on
                                                   Silicon) for returning a
                                                   model with Ref variables
                                                   resolved to object-like
                                                   structures.
      --cvc5Exe  <arg>                             cvc5 executable. The
                                                   environment variable CVC5_EXE
                                                   can also be used to specify
                                                   the path of the executable.
      --disableCaches                              Disables various caches in
                                                   Silicon's state.
      --disableCatchingExceptions                  Don't catch exceptions (can
                                                   be useful for debugging
                                                   problems with Silicon)
      --disableChunkOrderHeuristics                Disable heuristic ordering of
                                                   quantified chunks (context:
                                                   iterated separating
                                                   conjunctions).
      --disableHavocHack407                        A Viper method call to
                                                   ___silicon_hack407_havoc_all_R,
                                                   where R is a field or
                                                   predicate, results in Silicon
                                                   havocking all instances of R.
                                                   See also Silicon issue #407.
      --disableISCTriggers                         Don't pick triggers for
                                                   quantifiers, let the SMT
                                                   solver do it (context:
                                                   iterated separating
                                                   conjunctions).
      --disableShortCircuitingEvaluations          Disable short-circuiting
                                                   evaluation of AND, OR. If
                                                   disabled, evaluating e.g., i
                                                   > 0 && f(i), will fail if f's
                                                   precondition requires i > 0.
      --disableSubsumption                         Don't add assumptions gained
                                                   by verifying an assert
                                                   statement
      --disableTempDirectory                       Disable the creation of
                                                   temporary data (default:
                                                   ./tmp)
      --disableValueMapCaching                     Disable caching of value maps
                                                   (context: iterated separating
                                                   conjunctions).
      --enableBranchconditionReporting             Report branch conditions (can
                                                   be useful for assertions that
                                                   fail on multiple branches)
      --enableMoreCompleteExhale                   Enable a more complete exhale
                                                   version.
      --enablePredicateTriggersOnInhale            Emit predicate-based function
                                                   trigger on each inhale of a
                                                   predicate instance (context:
                                                   heap-dependent functions).
      --excludeMethods  <arg>                      Exclude methods from
                                                   verification (default: '').
                                                   Is applied after the include
                                                   pattern.
      --handlePureConjunctsIndividually            Handle pure conjunction
                                                   individually.Increases
                                                   precision of error reporting,
                                                   but may slow down
                                                   verification.
      --includeMethods  <arg>                      Include methods in
                                                   verification (default: '*').
                                                   Wildcard characters are '?'
                                                   and '*'.
  -Llogger=level [logger=level]...                 Set level of certain internal
                                                   loggers
      --logConfig  <arg>                           Path to config file
                                                   specifying SymbExLogger
                                                   options
      --logLevel  <arg>                            One of the log levels ALL,
                                                   TRACE, DEBUG, INFO, WARN,
                                                   ERROR, OFF
      --mapAxiomatizationFile  <arg>               Source file with map
                                                   axiomatisation. If omitted,
                                                   built-in one is used.
      --maxHeuristicsDepth  <arg>                  Maximal number of nested
                                                   heuristics applications
                                                   (default: 3)
      --multisetAxiomatizationFile  <arg>          Source file with multiset
                                                   axiomatisation. If omitted,
                                                   built-in one is used.
      --numberOfErrorsToReport  <arg>              Number of errors per member
                                                   before the verifier stops. If
                                                   this number is set to 0, all
                                                   errors are reported.
      --numberOfParallelVerifiers  <arg>           Number of verifiers run in
                                                   parallel. This number plus
                                                   one is the number of provers
                                                   run in parallel (default: 8
      --plugin  <arg>                              Load plugin(s) with given
                                                   class name(s). Several
                                                   plugins can be separated by
                                                   ':'. The fully qualified
                                                   class name of the plugin
                                                   should be specified.
      --printMethodCFGs                            Print a DOT (Graphviz)
                                                   representation of the CFG of
                                                   each method to verify to a
                                                   file
                                                   '<tempDirectory>/<methodName>.dot'.
      --printTranslatedProgram                     Print the final program that
                                                   is going to be verified to
                                                   stdout.
      --prover  <arg>                              One of the provers Z3, cvc5.
                                                   (default: Z3).
      --proverArgs  <arg>                          Command-line arguments which
                                                   should be forwarded to the
                                                   prover. The expected format
                                                   is "<opt> <opt> ... <opt>",
                                                   excluding the quotation
                                                   marks.
      --proverConfigArgs  <arg>...                 Configuration options which
                                                   should be forwarded to the
                                                   prover. The expected format
                                                   is "<key>=<val> <key>=<val>
                                                   ... <key>=<val>", excluding
                                                   the quotation marks. The
                                                   configuration options given
                                                   here will override those from
                                                   Silicon's prover preamble.
      --proverEnableResourceBounds                 Use prover's resource bounds
                                                   instead of timeouts
      --proverLogFile  <arg>                       Log file containing the
                                                   interaction with the prover,
                                                   extension smt2 will be
                                                   appended. (default:
                                                   <tempDirectory>/logfile.smt2)
      --proverRandomizeSeeds                       Set various random seeds of
                                                   the prover to random values
      --proverResourcesPerMillisecond  <arg>       Prover resources per
                                                   milliseconds. Is used to
                                                   convert timeouts to resource
                                                   bounds.
      --proverSaturationTimeout  <arg>             Timeout (in ms) used for the
                                                   prover's state saturation
                                                   calls (default: 100). A
                                                   timeout of 0 disables all
                                                   saturation checks.Note that
                                                   for the cvc5 prover, state
                                                   saturation calls can either
                                                   be disabled (weights or base
                                                   timeout of 0) or forced with
                                                   no timeout (positive weight
                                                   and base timeout).
      --proverSaturationTimeoutWeights  <arg>...   Weights used to compute the
                                                   effective timeout for the
                                                   prover's state saturation
                                                   calls, which are made at
                                                   various points during a
                                                   symbolic execution. The
                                                   effective timeouts for a
                                                   particular saturation call is
                                                   computed by multiplying the
                                                   corresponding weight with the
                                                   base timeout for saturation
                                                   calls. Defaults to the
                                                   following weights:
    after
                                                   program preamble: 1.0

                                                   after inhaling contracts:
                                                   0.5
    after unfold: 0.4

                                                   after inhale: 0.2
    before
                                                   repeated prover queries:
                                                   0.02
Weights must be
                                                   non-negative, a weight of 0
                                                   disables the corresponding
                                                   saturation call and a minimal
                                                   timeout of 10ms is
                                                   enforced.Note that for the
                                                   cvc5 prover, state saturation
                                                   calls can either be disabled
                                                   (weights or base timeout of
                                                   0) or forced with no timeout
                                                   (positive weight and base
                                                   timeout).
      --qpSplitTimeout  <arg>                      Timeout (in ms) used by QP's
                                                   split algorithm when 1)
                                                   checking if a chunk holds no
                                                   further permissions, and 2)
                                                   checking if sufficiently many
                                                   permissions have already been
                                                   split off.
      --recursivePredicateUnfoldings  <arg>        Evaluate n unfolding
                                                   expressions in the body of
                                                   predicates that
                                                   (transitively) unfold other
                                                   instances of themselves
                                                   (default: 1)
      --sequenceAxiomatizationFile  <arg>          Source file with sequence
                                                   axiomatisation. If omitted,
                                                   built-in one is used.
      --setAxiomatizationFile  <arg>               Source file with set
                                                   axiomatisation. If omitted,
                                                   built-in one is used.
      --stateConsolidationMode  <arg>              One of the following modes:

                                                   0: Minimal work, many
                                                   incompletenesses
  1: Most
                                                   work, fewest
                                                   incompletenesses
  2: Similar
                                                   to 1, but less eager
  3:
                                                   Less eager and less complete
                                                   than 1
  4: Intended for use
                                                   with --moreCompleteExhale

      --tempDirectory  <arg>                       Path to which all temporary
                                                   data will be written
                                                   (default: ./tmp)
      --timeout  <arg>                             Time out after approx. n
                                                   seconds. The timeout is for
                                                   the whole verification, not
                                                   per method or proof
                                                   obligation (default: 0, i.e.
                                                   no timeout).
      --z3Args  <arg>                              Warning: This option is
                                                   deprecated due to
                                                   standardization in option
                                                   naming. Please use
                                                   'proverArgs' instead...
                                                   Command-line arguments which
                                                   should be forwarded to Z3.
                                                   The expected format is "<opt>
                                                   <opt> ... <opt>", excluding
                                                   the quotation marks.
      --z3ConfigArgs  <arg>...                     Warning: This option is
                                                   deprecated due to
                                                   standardization in option
                                                   naming. Please use
                                                   'proverConfigArgs' instead...
                                                   Configuration options which
                                                   should be forwarded to Z3.
                                                   The expected format is
                                                   "<key>=<val> <key>=<val> ...
                                                   <key>=<val>", excluding the
                                                   quotation marks. The
                                                   configuration options given
                                                   here will override those from
                                                   Silicon's Z3 preamble.
      --z3EnableResourceBounds                     Warning: This option is
                                                   deprecated due to
                                                   standardization in option
                                                   naming. Please use
                                                   'proverEnableResourceBounds'
                                                   instead... Use Z3's resource
                                                   bounds instead of timeouts
      --z3Exe  <arg>                               Z3 executable. The
                                                   environment variable Z3_EXE
                                                   can also be used to specify
                                                   the path of the executable.
      --z3LogFile  <arg>                           Warning: This option is
                                                   deprecated due to
                                                   standardization in option
                                                   naming. Please use
                                                   'proverLogFile' instead...
                                                   Log file containing the
                                                   interaction with the prover,
                                                   extension smt2 will be
                                                   appended. (default:
                                                   <tempDirectory>/logfile.smt2).
      --z3RandomizeSeeds                           Warning: This option is
                                                   deprecated due to
                                                   standardization in option
                                                   naming. Please use
                                                   'proverRandomizeSeeds'
                                                   instead... Set various Z3
                                                   random seeds to random values
      --z3ResourcesPerMillisecond  <arg>           Warning: This option is
                                                   deprecated due to
                                                   standardization in option
                                                   naming. Please use
                                                   'proverResourcesPerMillisecond'
                                                   instead... Z3 resources per
                                                   milliseconds. Is used to
                                                   convert timeouts to resource
                                                   bounds.
      --z3SaturationTimeout  <arg>                 Warning: This option is
                                                   deprecated due to
                                                   standardization in option
                                                   naming. Please use
                                                   'proverSaturationTimeout'
                                                   instead... Timeout (in ms)
                                                   used for Z3 state saturation
                                                   calls (default: 100). A
                                                   timeout of 0 disables all
                                                   saturation checks.
      --z3SaturationTimeoutWeights  <arg>...       Warning: This option is
                                                   deprecated due to
                                                   standardization in option
                                                   naming. Please use
                                                   'proverSaturationTimeoutWeights'
                                                   instead... Weights used to
                                                   compute the effective timeout
                                                   for Z3 state saturation
                                                   calls, which are made at
                                                   various points during a
                                                   symbolic execution. The
                                                   effective timeouts for a
                                                   particular saturation call is
                                                   computed by multiplying the
                                                   corresponding weight with the
                                                   base timeout for saturation
                                                   calls. Defaults to the
                                                   following weights:
    after
                                                   program preamble: 1.0

                                                   after inhaling contracts:
                                                   0.5
    after unfold: 0.4

                                                   after inhale: 0.2
    before
                                                   repeated Z3 queries:
                                                   0.02
Weights must be
                                                   non-negative, a weight of 0
                                                   disables the corresponding
                                                   saturation call and a minimal
                                                   timeout of 10ms is enforced.
  -h, --help                                       Show help message

 trailing arguments:
  file (required)   The file to verify.
Verification aborted exceptionally: org.rogach.scallop.exceptions.RequiredOptionNotFound: Required option 'file' not found
org.rogach.scallop.exceptions.RequiredOptionNotFound: Required option 'file' not found
    at org.rogach.scallop.Scallop.parseRest$1(Scallop.scala:127)
    at org.rogach.scallop.Scallop.goParseRest$1(Scallop.scala:153)
    at org.rogach.scallop.Scallop.goParseRest$1(Scallop.scala:141)
    at org.rogach.scallop.Scallop.parse(Scallop.scala:197)
    at org.rogach.scallop.Scallop.parse(Scallop.scala:85)
    at org.rogach.scallop.Scallop.parsed$lzycompute(Scallop.scala:291)
    at org.rogach.scallop.Scallop.parsed(Scallop.scala:291)
    at org.rogach.scallop.Scallop.$anonfun$get$7(Scallop.scala:435)
    at scala.Option.map(Option.scala:242)
    at org.rogach.scallop.Scallop.get(Scallop.scala:434)
    at org.rogach.scallop.ScallopConfBase$$anon$1.$anonfun$fn$1(ScallopConfBase.scala:202)
    at scala.Function1.$anonfun$andThen$1(Function1.scala:85)
    at org.rogach.scallop.ScallopOption.value$lzycompute(ScallopOption.scala:25)
    at org.rogach.scallop.ScallopOption.value(ScallopOption.scala:25)
    at org.rogach.scallop.ScallopOption.foreach(ScallopOption.scala:90)
    at viper.silicon.Silicon.setLogLevelsFromConfig(Silicon.scala:321)
    at viper.silicon.Silicon.start(Silicon.scala:129)
    at viper.silicon.SiliconFrontend.configureVerifier(Silicon.scala:355)
    at viper.silicon.SiliconFrontend.configureVerifier(Silicon.scala:336)
    at viper.silver.frontend.SilFrontend.parseCommandLine(SilFrontend.scala:229)
    at viper.silver.frontend.SilFrontend.parseCommandLine$(SilFrontend.scala:228)
    at viper.silicon.SiliconFrontend.parseCommandLine(Silicon.scala:336)
    at viper.silver.frontend.SilFrontend.prepare(SilFrontend.scala:118)
    at viper.silver.frontend.SilFrontend.prepare$(SilFrontend.scala:113)
    at viper.silicon.SiliconFrontend.prepare(Silicon.scala:336)
    at viper.silver.frontend.SilFrontend.execute(SilFrontend.scala:153)
    at viper.silver.frontend.SilFrontend.execute$(SilFrontend.scala:147)
    at viper.silicon.SiliconFrontend.execute(Silicon.scala:336)
    at viper.silicon.SiliconRunner$.main(Silicon.scala:381)
    at viper.silicon.SiliconRunner.main(Silicon.scala)

[fpoli]

Also, the default of assertionMode is wrong. It's push-pop in the code.

[marcoeilers]

-Llogger=level is indented in a different way. I agree it looks weird, but that seems to be a feature of the library we're using for this kind of option, and I don't really want to change the type of option in case that breaks anyone's code. I've addressed the rest (except for the newline between options, which I also haven't found a way to do with the current library).

[fpoli]

Feel free to close this issue when the exeption is fixed. The other stuff might be subjective.