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 Main

    java.lang.Object
      javafe.Tool
          javafe.FrontEndTool
              javafe.SrcTool
                  escjava.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)

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