Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava
Class Options

    java.lang.Object
      javafe.Options
          javafe.SrcToolOptions
              escjava.Options

Direct Known Subclasses:
  GUI.Options

public class Options
extends SrcToolOptions

This class parses the options on the command-line and is a structure for holding the values of options.

Field Summary
`boolean` | `allocUseOpt`
`boolean` | `allowAlsoRequires`
`boolean` | `assertContinue`
`int` | `assertionMode`
`boolean` | `bubbleNotDown`
`boolean` | `checkPurity` Temporary option to turn on purity checking, since it is off by default until purity issues with inheritance are resolved.
`boolean` | `checkRedundantSpecs` Statically check against redundant specs?
`boolean` | `checkSpecs`
`java.lang.String` | `ClassVCPrefix`
`boolean` | `counterexample`
`boolean` | `desugaredSpecs` When set, prints out the desugared specs for debugging purposes.
`boolean` | `dsa`
`(package private) java.lang.String[][]` | `escPrivateOptionData`
`(package private) java.lang.String[][]` | `escPublicOptionData`
`boolean` | `excuseNullInitializers`
`boolean` | `filterInvariants`
`boolean` | `filterMethodSpecs`
`boolean` | `guardedVC`
`java.lang.String` | `guardedVCDir`
`java.lang.String` | `guardedVCFileExt`
`java.lang.String` | `guardedVCFileNumbers`
`java.lang.String` | `guardedVCGuardFile`
`java.lang.String` | `guardedVCPrefix`
`Set` | `guardVars`
`boolean` | `ifpvc2dot`
`Set` | `ignoreAnnSet`
`boolean` | `inferPredicates`
`boolean` | `inlineConstructors`
`boolean` | `inlineDepthFlags`
`boolean` | `inlineFromConstructors`
`static int` | `JAVA_ASSERTIONS`
`static int` | `JML_ASSERTIONS`
`boolean` | `lastVarUseOpt`
`boolean` | `lazySubst`
`static int` | `LOOP_FALL_THRU`
`static int` | `LOOP_FAST`
`static int` | `LOOP_SAFE`
`int` | `loopTranslation`
`int` | `loopUnrollCount`
`boolean` | `loopUnrollHalf`
`int` | `mapsUnrollCount`
`boolean` | `mergeInv`
`java.lang.String` | `MethodVCPrefix`
`int` | `namePCsize`
`boolean` | `nestQuantifiers`
`boolean` | `nne` Enable support for generating type-predicates for the \nonnullelements keyword.
`boolean` | `noDirectTargetsOpt`
`boolean` | `noNotCheckedWarnings` When true, does not print any warnings about things not checked.
`boolean` | `noOutCalls`
`boolean` | `noPeepOptGCAssertFalse`
`boolean` | `noSemicolonWarnings` JML requires semicolons to terminate annotations.
`boolean` | `noVarCheckDeclsAndUses`
`boolean` | `nvcg`
`boolean` | `nvcgpi`
`boolean` | `nvu`
`boolean` | `parsePlus` When true, parses pragmas that begin with /*+@, which are normally parsed only by JML; this allows test runs in which everything JML parses is parsed by escjava, to see if we have full coverage of all of JML.
`boolean` | `passify`
`boolean` | `pcc`
`boolean` | `pdsa`
`boolean` | `peepOptE`
`boolean` | `peepOptGC`
`boolean` | `pgc`
`boolean` | `pjt`
`boolean` | `plainWarning`
`boolean` | `pPvs`
`boolean` | `preciseTargets`
`boolean` | `predAbstract`
`boolean` | `prettyPrintVC` When set, pretty-prints the VCs that are obtained with verbose output or in the log (-sxLog)
`boolean` | `printAssumers`
`boolean` | `printCompilationUnitsOnLoad`
`boolean` | `pSimplify`
`boolean` | `pvc`
`boolean` | `pvsProof`
`int` | `rewriteDepth`
`Set` | `routinesToCheck`
`Set` | `routinesToSkip`
`boolean` | `showCallDetails`
`boolean` | `showFields`
`boolean` | `showLoopDetails`
`java.lang.String` | `simplify`
`java.lang.String` | `specspath` The dirpath or jar file of system specs to use.
`boolean` | `spvc`
`int` | `stages` Number of stages to run.
`int` | `startLine`
`boolean` | `statsQuantifierComplexity`
`boolean` | `statsSpace`
`boolean` | `statsTermComplexity`
`boolean` | `statsTime`
`boolean` | `statsVariableComplexity`
`boolean` | `strictExceptions`
`int` | `strongAssertPost` The following values are used: 0-never, 1-atomic (default), 2-always
`boolean` | `suggest`
`java.lang.String` | `sxLog`
`boolean` | `testRef` When true, pretty prints each compilation unit on the command-line; this is only used for testing, to test the combining of refinements.
`int` | `traceInfo`
`boolean` | `trackReadChars`
`java.lang.String` | `univBackPredFile`
`boolean` | `useAllInvPostBody`
`boolean` | `useAllInvPostCall`
`boolean` | `useAllInvPreBody`
`boolean` | `useDefpred`
`boolean` | `useFcnsForAllocations`
`boolean` | `useFcnsForMethods`
`boolean` | `useFcnsForModelVars`
`boolean` | `useHarvey`
`boolean` | `useIntQuantAntecedents`
`boolean` | `useOldStringHandling`
`boolean` | `useSammy`
`boolean` | `useSimplify`
`boolean` | `useThrowable` JML allows only subtypes of Exception in signals clauses.
`boolean` | `vc2dot`
`int` | `vclimit`
`int` | `wpnxw`
`boolean` | `wpp`

Fields inherited from class javafe.SrcToolOptions
`allowAvoidSpec, allowDepend, avoidSpec, processRecursively`

Fields inherited from class javafe.Options
`assertionsEnabled, assertIsKeyword, currentdir, eol, fileOrigin, inputEntries, issueUsage, NEVER_BINARY, NEVER_SOURCE, noCautions, PREFER_BINARY, PREFER_RECENT, PREFER_SOURCE, quiet, showErrorLocation, sysPath, testMode, userPath, userSourcePath, v`

Constructor Summary
`Options()`

Method Summary
`java.lang.String` | `nowarnOptionString()`
`int` | `processOption(java.lang.String option, java.lang.String[] args, int offset)` Process next tool option.
`private java.util.Vector` | `readFile(java.lang.String filename)`
`java.lang.String` | `showNonOptions()` Print non-option usage info to `System.err`.
`java.lang.String` | `showOptions(boolean all)` Generate all command-line option information.

Methods inherited from class javafe.Options
`checkMoreArguments, format, processFileOfArgs, processOptions, processOptionsLoop, showOptionArray, usage`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

### escPublicOptionData

    final java.lang.String[][] escPublicOptionData

### escPrivateOptionData

    final java.lang.String[][] escPrivateOptionData

### simplify

    public java.lang.String simplify

### useSimplify

    public boolean useSimplify

### useSammy

    public boolean useSammy

### useHarvey

    public boolean useHarvey

### pvsProof

    public boolean pvsProof

### nvcg

    public boolean nvcg

### nvcgpi

    public boolean nvcgpi

### pSimplify

    public boolean pSimplify

### pPvs

    public boolean pPvs

### vc2dot

    public boolean vc2dot

### ifpvc2dot

    public boolean ifpvc2dot

### suggest

    public boolean suggest

### pjt

    public boolean pjt

### nvu

    public boolean nvu

### pgc

    public boolean pgc

### pdsa

    public boolean pdsa

### pvc

    public boolean pvc

### pcc

    public boolean pcc

### counterexample

    public boolean counterexample

### statsTime

    public boolean statsTime

### statsSpace

    public boolean statsSpace

### statsTermComplexity

    public boolean statsTermComplexity

### statsVariableComplexity

    public boolean statsVariableComplexity

### statsQuantifierComplexity

    public boolean statsQuantifierComplexity

### plainWarning

    public boolean plainWarning

### useOldStringHandling

    public boolean useOldStringHandling

### useThrowable

    public boolean useThrowable

  JML allows only subtypes of Exception in signals clauses. Thus signals clauses cannot be written about Errors. Set this option to true to have annotations allow any Throwable.

### specspath

    public java.lang.String specspath

  The dirpath or jar file of system specs to use.

### checkRedundantSpecs

    public boolean checkRedundantSpecs

  Statically check against redundant specs? Default is true.

### traceInfo

    public int traceInfo

### prettyPrintVC

    public boolean prettyPrintVC

  When set, pretty-prints the VCs that are obtained with verbose output or in the log (-sxLog)

### desugaredSpecs

    public boolean desugaredSpecs

  When set, prints out the desugared specs for debugging purposes.

### testRef

    public boolean testRef

  When true, pretty prints each compilation unit on the command-line; this is only used for testing, to test the combining of refinements.

### checkPurity

    public boolean checkPurity

  Temporary option to turn on purity checking, since it is off by default until purity issues with inheritance are resolved.

### strictExceptions

    public boolean strictExceptions

### parsePlus

    public boolean parsePlus

  When true, parses pragmas that begin with /*+@, which are normally parsed only by JML; this allows test runs in which everything JML parses is parsed by escjava, to see if we have full coverage of all of JML.

### noNotCheckedWarnings

    public boolean noNotCheckedWarnings

  When true, does not print any warnings about things not checked.

### noSemicolonWarnings

    public boolean noSemicolonWarnings

  JML requires semicolons to terminate annotations. ESC/Java2 will warn about such missing semicolons; these were not required in ESC/Java. When the following option is true, such warnings are suppressed to support old ESC/Java annotations.

### rewriteDepth

    public int rewriteDepth

### spvc

    public boolean spvc

### dsa

    public boolean dsa

### passify

    public boolean passify

### wpp

    public boolean wpp

### useDefpred

    public boolean useDefpred

### wpnxw

    public int wpnxw

### namePCsize

    public int namePCsize

### peepOptE

    public boolean peepOptE

### peepOptGC

    public boolean peepOptGC

### lazySubst

    public boolean lazySubst

### mergeInv

    public boolean mergeInv

### JAVA_ASSERTIONS

    public static final int JAVA_ASSERTIONS

See Also:
  Constant Field Values

### JML_ASSERTIONS

    public static final int JML_ASSERTIONS

See Also:
  Constant Field Values

### assertionMode

    public int assertionMode

### useAllInvPostCall

    public boolean useAllInvPostCall

### useAllInvPostBody

    public boolean useAllInvPostBody

### useAllInvPreBody

    public boolean useAllInvPreBody

### allocUseOpt

    public boolean allocUseOpt

### LOOP_FAST

    public static final int LOOP_FAST

See Also:
  Constant Field Values

### LOOP_SAFE

    public static final int LOOP_SAFE

See Also:
  Constant Field Values

### LOOP_FALL_THRU

    public static final int LOOP_FALL_THRU

See Also:
  Constant Field Values

### loopTranslation

    public int loopTranslation

### loopUnrollCount

    public int loopUnrollCount

### loopUnrollHalf

    public boolean loopUnrollHalf

### mapsUnrollCount

    public int mapsUnrollCount

### preciseTargets

    public boolean preciseTargets

### predAbstract

    public boolean predAbstract

### inferPredicates

    public boolean inferPredicates

### noDirectTargetsOpt

    public boolean noDirectTargetsOpt

### nestQuantifiers

    public boolean nestQuantifiers

### lastVarUseOpt

    public boolean lastVarUseOpt

### noVarCheckDeclsAndUses

    public boolean noVarCheckDeclsAndUses

### useIntQuantAntecedents

    public boolean useIntQuantAntecedents

### excuseNullInitializers

    public boolean excuseNullInitializers

### strongAssertPost

    public int strongAssertPost

  The following values are used:
  0-never, 1-atomic (default), 2-always

### showCallDetails

    public boolean showCallDetails

### showLoopDetails

    public boolean showLoopDetails

### bubbleNotDown

    public boolean bubbleNotDown

### startLine

    public int startLine

### vclimit

    public int vclimit

### checkSpecs

    public boolean checkSpecs

### noOutCalls

    public boolean noOutCalls

### printAssumers

    public boolean printAssumers

### noPeepOptGCAssertFalse

    public boolean noPeepOptGCAssertFalse

### assertContinue

    public boolean assertContinue

### trackReadChars

    public boolean trackReadChars

### guardedVC

    public boolean guardedVC

### guardedVCDir

    public java.lang.String guardedVCDir

### guardedVCFileNumbers

    public java.lang.String guardedVCFileNumbers

### guardedVCGuardFile

    public java.lang.String guardedVCGuardFile

### guardedVCPrefix

    public java.lang.String guardedVCPrefix

### guardedVCFileExt

    public java.lang.String guardedVCFileExt

### guardVars

    public Set guardVars

### ClassVCPrefix

    public java.lang.String ClassVCPrefix

### MethodVCPrefix

    public java.lang.String MethodVCPrefix

### ignoreAnnSet

    public Set ignoreAnnSet

### printCompilationUnitsOnLoad

    public boolean printCompilationUnitsOnLoad

### useFcnsForModelVars

    public boolean useFcnsForModelVars

### useFcnsForMethods

    public boolean useFcnsForMethods

### useFcnsForAllocations

    public boolean useFcnsForAllocations

### filterInvariants

    public boolean filterInvariants

### filterMethodSpecs

    public boolean filterMethodSpecs

### routinesToCheck

    public Set routinesToCheck

### routinesToSkip

    public Set routinesToSkip

### inlineConstructors

    public boolean inlineConstructors

### inlineDepthFlags

    public boolean inlineDepthFlags

### inlineFromConstructors

    public boolean inlineFromConstructors

### sxLog

    public java.lang.String sxLog

### allowAlsoRequires

    public boolean allowAlsoRequires

### showFields

    public boolean showFields

### stages

    public int stages

  Number of stages to run. The stages currently in order are:

           1. loading, parsing, and type checking
           2. generating the type-specific background predicate
              3. translating from Java to GC
              4. translating from GC to DSA
           5. generating the VC from the GC
           6. calling the theorem prover to verify the VC

  Defaults to running all stages (6); must be positive.

  -nocheck sets `stages` to run all but the last stage (5). The -stages option can be used to set `stages` to a particular value.

### univBackPredFile

    public java.lang.String univBackPredFile

### nne

    public boolean nne

  Enable support for generating type-predicates for the \nonnullelements keyword. Disabled by default.

Constructor Detail

### Options

    public Options()

Method Detail

### showOptions

    public java.lang.String showOptions(boolean all)

  Generate all command-line option information.

  Overrides:
    `showOptions` in class `SrcToolOptions`
  Parameters:
    `all` - if true show all non-public (experimental) switches as well.
  Returns:
    a String containing all command-line option information.

### showNonOptions

    public java.lang.String showNonOptions()

  Description copied from class: `SrcToolOptions`
  Print non-option usage info to `System.err`. Output must include at least one newline.

  Overrides:
    `showNonOptions` in class `SrcToolOptions`
  Returns:
    non-option usage information in a string.

### processOption

    public int processOption(java.lang.String option,
                             java.lang.String[] args,
                             int offset)
                      throws UsageError

  Process next tool option.

  See `Options.processOptions(String [])` for the complete specification of this routine.

  Overrides:
    `processOption` in class `SrcToolOptions`
  Throws:
    `UsageError`

### readFile

    private java.util.Vector readFile(java.lang.String filename)

### nowarnOptionString

    public java.lang.String nowarnOptionString()

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage