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 Main

java.lang.Object
  extended byjavafe.Tool
      extended byjavafe.FrontEndTool
          extended byjavafe.SrcTool
              extended byescjava.Main
All Implemented Interfaces:
Listener
Direct Known Subclasses:
GUI

public class Main
extends SrcTool

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.

See Also:
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

jarlocation

public static final java.lang.String jarlocation

version

public static final java.lang.String version
Our version number

See Also:
Constant Field Values

annotationHandler

private AnnotationHandler annotationHandler

stages

public int stages

keepProver

boolean keepProver

gctranslator

public static Translate gctranslator
An instance of the GC->VC translator

Constructor Detail

Main

public Main()
Method Detail

name

public java.lang.String name()
Return the name of this tool. E.g., "ls" or "cp".

Used in usage and error messages.

Specified by:
name in class Tool

makeOptions

public Options makeOptions()
Description copied from class: SrcTool
* Main processing code: * *

Overrides:
makeOptions in class SrcTool

options

public static Options options()

makeStandardTypeReader

public StandardTypeReader makeStandardTypeReader(java.lang.String path,
                                                 java.lang.String sourcePath,
                                                 PragmaParser P)
Returns the Esc StandardTypeReader, EscTypeReader.

Overrides:
makeStandardTypeReader in class FrontEndTool

makePragmaParser

public PragmaParser makePragmaParser()
Returns the EscPragmaParser.

Overrides:
makePragmaParser in class FrontEndTool

makePrettyPrint

public PrettyPrint makePrettyPrint()
Returns the pretty printer to set PrettyPrint.inst to.

Overrides:
makePrettyPrint in class FrontEndTool

makeTypeCheck

public TypeCheck makeTypeCheck()
Called to obtain an instance of the javafe.tc.TypeCheck class (or a subclass thereof). May not return null. By default, returns javafe.tc.TypeCheck.

Overrides:
makeTypeCheck in class FrontEndTool

notify

public void notify(CompilationUnit justLoaded)
Override SrcTool.notify to ensure all lexicalPragmas get registered as they are loaded.

Specified by:
notify in interface Listener
Overrides:
notify in class SrcTool

main

public static void main(java.lang.String[] args)
Start up an instance of this tool using command-line arguments args.

This is the main entry point for the escjava command.


clear

public void clear(boolean complete)
Description copied from class: FrontEndTool
Called to clear any static initializations, so that the parser can be called multiple times within one process. Called as part of construction of a new Main.

Overrides:
clear in class FrontEndTool

compile

public static int compile(java.lang.String[] args)
An entry point for the tool useful for executing tests, since it returns the exit code.

Parameters:
args - The command-line arguments the program was invoked with
Returns:
The exit code for the program, indicating either a successful exit or an exit with errors or an exit because of an out of memory condition
See Also:
Tool.run(java.lang.String[])

setup

public 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).

Overrides:
setup in class FrontEndTool

setDefaultSimplify

public void setDefaultSimplify()

setupPaths

public void setupPaths()
Overrides:
setupPaths in class FrontEndTool

preload

public void preload()
Description copied from class: SrcTool
Hook for any work needed before any files are loaded.

Overrides:
preload in class SrcTool

preprocess

public void preprocess()
Hook for any work needed before handleCU is called on each CompilationUnit to process them.

Overrides:
preprocess in class SrcTool

fileToPrintStream

private java.io.PrintStream fileToPrintStream(java.lang.String dir,
                                              java.lang.String fname)
A wrapper for opening output files for printing. dir can be null.


postload

public void postload()
Description copied from class: SrcTool
Called for any work after loading files

Overrides:
postload in class SrcTool

postprocess

public void postprocess()
Hook for any work needed after handleCU has been called on each CompilationUnit to process them.

Overrides:
postprocess in class SrcTool

handleCU

public void handleCU(CompilationUnit cu)
This method is called on each 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.

Overrides:
handleCU in class SrcTool

handleTD

public void handleTD(TypeDecl td)
This method is called by SrcTool on the TypeDecl of each outside type that SrcTool is to process.

In addition, it calls itself recursively to handle types nested within outside types.

Overrides:
handleTD in class SrcTool

processTD

private boolean processTD(TypeDecl td)
Run all the requested stages on a given TypeDecl; return true if we had to abort.


processTypeDeclElem

private void processTypeDeclElem(TypeDeclElem te,
                                 TypeSig sig,
                                 InitialState initState)
Run stages 3+..6 as requested on a TypeDeclElem. requires te is not from a binary file, sig is the TypeSig for te's parent, and initState != null.


processRoutineDecl

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. requires - r is not from a binary file, sig is the TypeSig for r's parent, and initState != null.


doProving

public int doProving(Expr vc,
                     RoutineDecl r,
                     Set directTargets,
                     FindContributors scope)

computeBody

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.

Returns:
null if r doesn't have a body.

removeSpaces

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

The ESC/Java2 Project Homepage