|
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 |
java.lang.Objectjavafe.Tool
javafe.FrontEndTool
javafe.SrcTool
escjava.Main
Top level control module for ESC for Java.
This class (and its superclasses) handles parsing
escjava
's command-line arguments and orchestrating the
other pieces of the front end and escjava to perform the requested
operations.
Tool
,
SrcTool
Field Summary | |
private AnnotationHandler |
annotationHandler
|
static Translate |
gctranslator
An instance of the GC->VC translator |
static java.lang.String |
jarlocation
|
(package private) boolean |
keepProver
|
int |
stages
|
static java.lang.String |
version
Our version number |
Fields inherited from class javafe.SrcTool |
loaded |
Fields inherited from class javafe.FrontEndTool |
compositeClassPath, compositeSourcePath |
Fields inherited from class javafe.Tool |
badUsageExitCode, errorExitCode, okExitCode, options, outOfMemoryExitCode |
Constructor Summary | |
Main()
|
Method Summary | |
void |
clear(boolean complete)
Called to clear any static initializations, so that the parser can be called multiple times within one process. |
static int |
compile(java.lang.String[] args)
An entry point for the tool useful for executing tests, since it returns the exit code. |
protected GuardedCmd |
computeBody(RoutineDecl r,
InitialState initState)
This method computes the guarded command (including assuming the precondition, the translated body, the checked postcondition, and the modifies constraints) for the method or constructor r in scope scope . |
int |
doProving(Expr vc,
RoutineDecl r,
Set directTargets,
FindContributors scope)
|
private java.io.PrintStream |
fileToPrintStream(java.lang.String dir,
java.lang.String fname)
A wrapper for opening output files for printing. |
void |
handleCU(CompilationUnit cu)
This method is called on each CompilationUnit that
this tool processes. |
void |
handleTD(TypeDecl td)
This method is called by SrcTool on the TypeDecl of each outside type that SrcTool is to process. |
static void |
main(java.lang.String[] args)
Start up an instance of this tool using command-line arguments args . |
Options |
makeOptions()
* Main processing code: * * |
PragmaParser |
makePragmaParser()
Returns the EscPragmaParser. |
PrettyPrint |
makePrettyPrint()
Returns the pretty printer to set PrettyPrint.inst to. |
StandardTypeReader |
makeStandardTypeReader(java.lang.String path,
java.lang.String sourcePath,
PragmaParser P)
Returns the Esc StandardTypeReader, EscTypeReader. |
TypeCheck |
makeTypeCheck()
Called to obtain an instance of the javafe.tc.TypeCheck class (or a subclass thereof). |
java.lang.String |
name()
Return the name of this tool. |
void |
notify(CompilationUnit justLoaded)
Override SrcTool.notify to ensure all lexicalPragmas get registered as they are loaded. |
static Options |
options()
|
void |
postload()
Called for any work after loading files |
void |
postprocess()
Hook for any work needed after handleCU has been
called on each CompilationUnit to process them. |
void |
preload()
Hook for any work needed before any files are loaded. |
void |
preprocess()
Hook for any work needed before handleCU is called
on each CompilationUnit to process them. |
private java.lang.String |
processRoutineDecl(RoutineDecl r,
TypeSig sig,
InitialState initState)
Run stages 3+..6 as requested on a RoutineDeclElem; returns a short (~ 1 word) status message. |
private boolean |
processTD(TypeDecl td)
Run all the requested stages on a given TypeDecl; return true if we had to abort. |
private void |
processTypeDeclElem(TypeDeclElem te,
TypeSig sig,
InitialState initState)
Run stages 3+..6 as requested on a TypeDeclElem. |
private static java.lang.String |
removeSpaces(java.lang.String s)
|
void |
setDefaultSimplify()
|
void |
setup()
Override setup so can issue version # as soon as possible (aka, just after decode options so know if -quiet or -testMode issued or not). |
void |
setupPaths()
|
Methods inherited from class javafe.SrcTool |
frontEndToolProcessing, handleAllCUs, loadAllFiles, loadInputEntry, resolveInputEntry, resolveList |
Methods inherited from class javafe.FrontEndTool |
handleOptions, processOptions, run |
Methods inherited from class javafe.Tool |
badOptionUsage, currentTime, spaceUsed, timeUsed, usage |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
public static final java.lang.String jarlocation
public static final java.lang.String version
private AnnotationHandler annotationHandler
public int stages
boolean keepProver
public static Translate gctranslator
Constructor Detail |
public Main()
Method Detail |
public java.lang.String name()
Used in usage and error messages.
name
in class Tool
public Options makeOptions()
SrcTool
makeOptions
in class SrcTool
public static Options options()
public StandardTypeReader makeStandardTypeReader(java.lang.String path, java.lang.String sourcePath, PragmaParser P)
makeStandardTypeReader
in class FrontEndTool
public PragmaParser makePragmaParser()
makePragmaParser
in class FrontEndTool
public PrettyPrint makePrettyPrint()
PrettyPrint.inst
to.
makePrettyPrint
in class FrontEndTool
public TypeCheck makeTypeCheck()
null
. By
default, returns javafe.tc.TypeCheck
.
makeTypeCheck
in class FrontEndTool
public void notify(CompilationUnit justLoaded)
notify
in interface Listener
notify
in class SrcTool
public static void main(java.lang.String[] args)
args
.
This is the main entry point for the escjava
command.
public void clear(boolean complete)
FrontEndTool
clear
in class FrontEndTool
public static int compile(java.lang.String[] args)
args
- The command-line arguments the program was invoked with
Tool.run(java.lang.String[])
public void setup()
setup
in class FrontEndTool
public void setDefaultSimplify()
public void setupPaths()
setupPaths
in class FrontEndTool
public void preload()
SrcTool
preload
in class SrcTool
public void preprocess()
handleCU
is called
on each CompilationUnit
to process them.
preprocess
in class SrcTool
private java.io.PrintStream fileToPrintStream(java.lang.String dir, java.lang.String fname)
public void postload()
SrcTool
postload
in class SrcTool
public void postprocess()
handleCU
has been
called on each CompilationUnit
to process them.
postprocess
in class SrcTool
public void handleCU(CompilationUnit cu)
CompilationUnit
that
this tool processes. This method overrides the implementation
given in the superclass, adding a couple of lines before the
superclass implementation is called.
handleCU
in class SrcTool
public void handleTD(TypeDecl td)
In addition, it calls itself recursively to handle types nested within outside types.
handleTD
in class SrcTool
private boolean processTD(TypeDecl td)
private void processTypeDeclElem(TypeDeclElem te, TypeSig sig, InitialState initState)
private java.lang.String processRoutineDecl(RoutineDecl r, TypeSig sig, InitialState initState)
public int doProving(Expr vc, RoutineDecl r, Set directTargets, FindContributors scope)
protected GuardedCmd computeBody(RoutineDecl r, InitialState initState)
r
in scope scope
.
null
if r
doesn't have a body.private static java.lang.String removeSpaces(java.lang.String s)
|
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 |