ESCCLI

Introduction

The Extended Static Checking system has its own command line interface, based on the original command line interface for ESC/Java2 and recent extensions by Mobius and other reseachers.

TOC

Syntax

• Options begin with a dash "-", parameters do not; syntax is {}
• Options are case-sensitive

Excluded Combinations

The following combinations of options are not possible:

• -PrettyPrintVC -PrintVC
• -eaJML -eaJava
• -prover|svcg -NoCheck
• -noTrace -VerboseTrace
• -Loop <positive integer|half-integer>, -LoopSafe, -LoopFallThru
• -Routine -RoutineIndirect
• -idc -erst
• -inlineConstructors -inlineCheckDepth|inlineDepthPastCheck

Non-Exclusive Options

• CounterExample
• NoSemicolonWarnings
• Simplify
• Specs <pathname | filename>
• Typecheck
• NoRedundancy
• NoTrace
• nonNullByDefault
• NoWarn
• PlainWarning
• Start
• Stats
• Suggest
• VCLimit
• Warn

Dependent Options

• NoSingleDynmaicAssignment => nospvc

Parameter Types

Filenames::String

Pathnames::String

Provers::String

Positive Integers::Integer

Positive Halves::IntegerDigit

Numbers that are either positive integers or halfway between two position integers e.g. 1.5

[http://en.wikipedia.org/wiki/Half-integer]

Routines::String

• Routine identifiers e.g. a method identifier
• Fully qualified signatures of routines e.g. a method signature

Categories::String

• Categories of Warnings

Defaults

• -Loop 1.5
• -JMLAssertions
• -Prover simplify
• -VCLimit 500000

Synonyms and Abbreviations

||Abbreviation_'||'_Synonym|| ||bpf||BackPredFile|| ||bnd||BubbleNotDown|| ||eaJML||JMLAssertions|| ||eaJava||JavaAssertions|| ||era||ReachabilityAnalysis|| ||erst||ReachabilitySpecTest|| ||ersta||ReachabilitySpecTestAll|| ||sds||ShowDesuguredSpecs|| ||pcc||PrintCounterExampleContext|| ||pgc||PrintGuardedCommands|| ||ppvc||PrettyPrintVC|| ||pvc||PrintVC|| ||pjt||PrintJavaWithTypes|| ||npdsa||NoDynamicSingleAssignment|| ||psda||PrintDynamicSingleAssignment|| ||nvu||NoVariableUniquification|| ||ac||AssertContinue|| ||nne||NonNullElements|| ||inChk||ConsistencyCheck||

Parameters

||Option_'||'''Parameter'''||'''Allowed Values'''||'_Default|| ||Loop||Number of iterations to check||Positive multiple of 0.5||1.5||

Multiple Instances of Options

Most of the options cannot be repeated (or make no sense to be repeated), some can be. For instance -warn seems to support multiple occurrences.

The -warn option is interesting as the category string is implemented as an enumeration.

Declarative Specification

The command line interface ESC/Java2 will be modeled as a declarative specification written in first-order JML with generalised quantifiers over finite domains.

Version: 2 Time: Thu Jul 24 12:49:32 2008 Author: dcochran (dcochran) IP: 193.1.132.32