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
private static Main	instance
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.
static Main	getInstance()
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.
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

instance

private static Main instance

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

getInstance

public static Main getInstance()

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

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