Usage

Web Form

On the prototype page you see two text fields.

In the first text field you can type an input Java program. Optionally, you can select an example file from the drop-down menu above the text field. Click on the button "load file" to load the example into the field.

The second text field contains the output of the JSA prototype. To analyse the Java program click on the button "Infer Types" that is located on the left hand side between the input and the output text field. In the context drop-down box, you can choose the kind of contexts for the analysis. The output will tell you either that type checking was successful, or give information on the error. Below, depending on the "Verbosity" checkbox, you will get information about various analyze stages. See Analyzer for a more detailed explanation of the phases.

 

Command Line

Run the executable jsax  without arguments to get a description of the command-line syntax:

Usage: jsax [options] java-files...

All given Java files are analyzed simultaneously.

  Options:
    --javart=<file>     -- specify complete file name of java runtime library
                               (rt.jar or classes.jar)

    --verbose           -- verbose output
    --parse-only        -- stop after parsing input files
    --type-only         -- stop after typing (no constraint solving)

    --monoid=<file>     -- use custom monoid description file 
                           (other than default.mon)

    --context=<type>    -- choose context-sensitive analysis <type>:
        insensitive: no contexts (default)
        kcfa:        10-CFA with stack of method / line number pairs

    --solver=<slv>      -- choose constraint solver <slv>
        succinct:    use Succinct Solver (default)