kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

ktest --help throws an exception #523

Closed grosu closed 10 years ago

grosu commented 10 years ago

See at the end:

fslwork$ ktest --help
usage: ktest <file> [options]
<file> is either a K definition (single job mode) or an XML configuration
(batch mode).
 -h,--help                                   Print this help message.
    --version                                Print version information.
 -v,--verbose                                Verbose output.
    --color <[on|off|extended]>              Use colors in output. (Default:
                                             on)
    --programs <dir>                         Programs directory in single job
                                             mode, or a root directory for
                                             programs in batch mode. By default
                                             this is the directory where <file>
                                             reside.
    --extension <string>                     The list of program extensions
                                             separated by whitespaces. Required
                                             in single job mode, invalid in
                                             batch mode.
    --exclude <file>                         The list of programs which will
                                             not be tested. Valid only in
                                             single job mode.
    --results <dir>                          Directory containing input and
                                             expected output for programs in
                                             single job mode, or a root
                                             directory for the expected I/O for
                                             programs in batch mode. By default
                                             this is the directory where <file>
                                             reside.
    --skip <steps>                           The list of steps to be skipped,
                                             separated by whitespace. A step is
                                             either [kompile|pdf|krun].
 -d,--directory <dir>                        A root directory where K
                                             definitions reside. By default
                                             this is the current directory.
                                             Valid only in batch mode.
    --report                                 Generate a junit-like report.
    --timeout <num>                          Time limit for each process
                                             (milliseconds). Default is 300000
                                             milliseconds.
    --update-out                             Update existing .out files.
    --generate-out                           Newly generate .out files if
                                             needed.
    --threads <threads>                      Maximum number of threads spawned
                                             for parallel execution.
    --ignore-white-spaces <on|off>           Ignore white spaces when comparing
                                             results. (Default: on).
    --ignore-balanced-parentheses <on|off>   Ignore balanced parentheses when
                                             comparing results. (Default: on).
    --dry                                    Dry run: print out the command to
                                             be executed without actual
                                             execution.

Exception in thread "main" java.lang.NullPointerException
    at org.kframework.main.Main.main(Main.java:79)
fslwork$ 
daejunpark commented 10 years ago

Will it be fixed in the pull request #522? It seems to be same with the issue #407.

osa1 commented 10 years ago

Yes.

osa1 commented 10 years ago

I'm closing this as it's fixed in referenced patch.

yilongli commented 10 years ago

If you type incorrect option after the krun, say, krun --helpme, you still get an NPE error.

See the end of the output:

Error while parsing commandline:Unrecognized option: --helpme
usage: krun [options] <file>

 -h,--help                          Print this help message.
    --version                       Print version information.
 -v,--verbose                       Verbose output.
    --debug                         Debug messages
 -d,--directory <dir>               Path to the directory in which the kompiled
                                    K definition resides. The default is the
                                    current directory.
    --main-module <name>            Specify main module in which a program
                                    starts to execute. The default is the
                                    module specified in the given compiled K
                                    definition.
    --syntax-module <name>          Specify main module for syntax. The default
                                    is the module specified in the given
                                    compiled K definition.
    --io <[on|off]>                 Use real IO when running the definition.
                                    (Default: enabled).
    --color <[on|off|extended]>     Use colors in output. (Default: on).
    --terminal-color <color-name>   Background color of the terminal. Cells
                                    won't be colored in this color. (Default:
                                    black).
    --parser <command>              Command used to parse programs. (Default:
                                    kast).
    --config-var-parser <file>      Command used to parse configuration
                                    variables. (Default: kast -e).  See
                                    --parser above. Applies to subsequent -c
                                    options until another parser is specified
                                    with this option.
 -c,--config-var <name=value>       Specify values for variables in the
                                    configuration.
 -o,--output <mode>                 How to display Maude results. <mode> is
                                    either
                                    [pretty|smart|compatible|kore|raw|binary|no
                                    ne]. (Default: pretty).
    --search                        In conjunction with it you can specify 3
                                    options that are optional: pattern (the
                                    pattern used for search), bound (the number
                                    of desired solutions) and depth (the
                                    maximum depth of the search).
    --search-final                  Same as --search but only return final
                                    states, even if --depth is provided.
    --search-all                    Same as --search but return all matching
                                    states, even if --depth is not provided.
    --search-one-step               Same as --search but search only one
                                    transition step.
    --search-one-or-more-steps      Same as --search-all but exclude initial
                                    state, even if it matches.
    --pattern <string>              Specify a term and/or side condition that
                                    the result of execution or search must
                                    match in order to succeed. Return the
                                    resulting matches as a list of
                                    substitutions. In conjunction with it you
                                    can specify other 2 options that are
                                    optional: bound (the number of desired
                                    solutions) and depth (the maximum depth of
                                    the search).
    --bound <num>                   The number of desired solutions for search.
    --depth <num>                   The maximum number of computational steps
                                    to execute or search the definition for.
    --graph                         Displays the search graph generated by the
                                    last search.
    --backend <backend>             Specify the krun backend to execute with.
                                    <backend> is either [maude|java]. (Default:
                                    maude).
    --simulation <string>           Simulation property of two programs in two
                                    semantics.
 -X,--help-experimental             Print help on non-standard options.

Exception in thread "main" java.lang.NullPointerException
    at org.kframework.main.Main.main(Main.java:79)
osa1 commented 10 years ago

This is an unrelated issue. Original issue was for ktest, not for krun.

yilongli commented 10 years ago

Yes, it was for ktest. But it looks like a generic problem, even the line of code which throws the exception is the same.

osa1 commented 10 years ago

Closing as this no longer happens.