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

escjava
Class Options

java.lang.Object
  extended byjavafe.Options
      extended byjavafe.SrcToolOptions
          extended byescjava.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()

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

The ESC/Java2 Project Homepage