org.jmlspecs.racwrap
Class Main

java.lang.Object
  org.multijava.util.Utils
      org.multijava.util.compiler.Compiler
          org.multijava.mjc.Main
              org.jmlspecs.checker.Main
                  org.jmlspecs.jmlrac.Main
                      org.jmlspecs.racwrap.Main

All Implemented Interfaces:

Cloneable, TroubleReporter

public class Main

extends Main

This is the Main class for generating assertion code from JML specs that goes into wrappers, rather that inline. There are two tasks that need to be done here. One is to compile the original code normally, as if not processed by JML. The other is to compile the wrapper generated code.

Nested Class Summary
class	Main.CollateFilesTask           CollateFilesTask is used to put all the source files into a list.
class	Main.PrintFactoryTask           PrintFactoryTask actually also prints the static members of the class
class	Main.PrintInterfaceTask           PrintInterfaceTask is used for outputting the interface for the input file.
class	Main.PrintOrigTask           PrintOrigTask is used to print the modified original class
class	Main.PrintWrapperTask           PrintWrapperTask is used to print the wrappers class

 

Nested classes inherited from class org.jmlspecs.jmlrac.Main

Main.JavaParseTask, Main.JmlGenerateAssertionTask, Main.JmlPrettyPrintTask, Main.JmlWriteAssertionTask

 

Nested classes inherited from class org.jmlspecs.checker.Main

Main.JmlCheckAssignableTask, Main.JmlParseTask, Main.JmlTypecheckTask

 

Nested classes inherited from class org.multijava.mjc.Main

Main.CheckInitializerTask, Main.CheckInterfaceTask, Main.ContextBehavior, Main.DFilter, Main.ExpectedGF, Main.ExpectedIndifferent, Main.ExpectedResult, Main.ExpectedType, Main.ParseTask, Main.PreprocessTask, Main.PrettyPrintTask, Main.ResolveSpecializerTask, Main.ResolveTopMethodTask, Main.Task, Main.TaskTimes, Main.TranslateMJTask, Main.TreeProcessingTask, Main.Trees, Main.TypecheckTask

 

Field Summary
private  String[]	args
private  List	origFiles           these are the original source files.
private  ArrayList	wrapFiles           these are the files that the wrapper version generated.
private  Map	wrapMap           maps directories to classes in that directory for which racwrap has generated files.

 

Fields inherited from class org.jmlspecs.jmlrac.Main

isSecondRound, modUtil, PRI_GENERATE_ASSERTION, PRI_GENERATE_SYMBOL, racOptions

 

Fields inherited from class org.jmlspecs.checker.Main

jmlOptions, refinedFileSequenceSet

 

Fields inherited from class org.multijava.mjc.Main

activeSequenceID, activeTaskPriority, allowUniverseAnnotations, allowUniverseBytecode, allowUniverseChecks, allowUniverseDynChecks, allowUniverseKeywords, allowUniversePurity, appName, classes, codeGenNeeded, contextsCreated, destination, errorFound, errorLimit, filesFound, mostSevereWarningIssued, options, parseJavadoc, PRI_CHECK_INITIALIZER, PRI_CHECK_INTERFACE, PRI_PARSE, PRI_PREPROCESS, PRI_PRETTY_PRINT, PRI_RESOLVE_SPECIALIZER, PRI_TOP_METHODS, PRI_TRANSLATE_MJ, PRI_TYPECHECK, taskQueue, uncheckedWarningsIssued, UNIVERSE_ANNOTATIONS, UNIVERSE_BYTECODE, UNIVERSE_CHECKS, UNIVERSE_DYNCHECKS, UNIVERSE_FULL, UNIVERSE_NO, UNIVERSE_PARSE, UNIVERSE_PURITY, universeVersion

 

Fields inherited from class org.multijava.util.compiler.Compiler

PRINT_TO_ERR, PRINT_TO_OUT

 

Fields inherited from class org.multijava.util.Utils

DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO

 

Constructor Summary

Main()           The the constructor for the wrapper based runtime assertion check generator.

 

Method Summary
static boolean	compile(String[] args)           Entry point for other programs wishing to use the wrapper generator.
protected  Main.Task	createTaskAfter(Main.Task oldTask)           This method uses the type of oldTask and the command line options to sequence tasks.
PrintStream	createTempFile(JmlCompilationUnit cunit, String filename)
static void	main(String[] args)           The main entry point when starting this program from the command line.
void	setArgs(String[] args)

 

Methods inherited from class org.jmlspecs.jmlrac.Main

classToGenerate, compile, createCompilationUnitContext, createRacGenerator, exposeOptions, firstTask, firstTask, getFileMap, getOptionsInstance, hasOptionXsymr, hasOptionXsymw, initSecondSession, isSpecMode, makeOptionsInstance, prepareSecondRound, setFileMap

 

Methods inherited from class org.jmlspecs.checker.Main

canStopSequenceBeforeAllPasses, catchUpRefinedFile, catchUpTask, compile, filenameFilter, getDefaultFilter, getWarningFilterNameFromOptions, hasOptionXobspure, hasUnsafeOpWarningOption, includeAllRefinedCUnits, initialize, initSession, isCommandLineFile, isSpecOrJmlMode, jmlNoBodyOK, makeRelative, parseArguments

 

Methods inherited from class org.multijava.mjc.Main

activeSequenceID, adoptCompilationUnitContext, bugReportBoilerplate, bugReportProperty, bugReportRequest, catchUp, catchUp, catchUpGF, catchUpType, checkPackageName, compile, contextBehavior, currentlyParsingFor, expandAtFiles, experimentalArrayHandling, failedParsing, firstCheckingTask, genCode, Generic, Generic, getClasses, getFilter, handleDirectories, handleNonOptions, handlePackageName, handlePackages, hasAlreadyFailedToParseFor, hasAlreadySuccessfullyParsed, initSession, interruptCompilation, isAnExpectedResult, isCurrentlyParsingFor, mainSequenceID, nonNullTypes, noteError, optimizeCode, options, parseAtFile, parseComments, prettyPrint, processTaskQueue, quietMode, RecommendedWarning, reportTrouble, reportTroubleFiltered, RMJ, run, run, runCompilation, runInitialization, runParser, runSetInitialTasks, safeMath, setAllowUniverses, setContextBehavior, setMainSequenceID, setUniverseChecks, setUniversePurity, subdirectoryFilter, successfullyParsed, suppressWarning, taskQueueEmptied, universeBytecode, universeBytecodeAnnotations, universeChecks, universeDynChecks, universeKeywords, universePurity, universeVersion, validPackageName, verboseMode

 

Methods inherited from class org.multijava.util.compiler.Compiler

getTimestamp, inform, inform, inform, inform, inform, inform, inform, inform, inform, modUtil, run, setOutputStream, verifyFiles, verifyFiles

 

Methods inherited from class org.multijava.util.Utils

assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

args

private String[] args

wrapFiles

private ArrayList wrapFiles

these are the files that the wrapper version generated.

wrapMap

private Map wrapMap

maps directories to classes in that directory for which racwrap has generated files.

origFiles

private List origFiles

these are the original source files.

Main

public Main()

The the constructor for the wrapper based runtime assertion check generator.

setArgs

public void setArgs(String[] args)

main

public static void main(String[] args)

The main entry point when starting this program from the command line.

Parameters:

args - The command line arguments.

compile

public static boolean compile(String[] args)

Entry point for other programs wishing to use the wrapper generator.

Parameters:

args - The command line arguments.

Returns:

true is the compilation was successful

createTaskAfter

protected Main.Task createTaskAfter(Main.Task oldTask)

This method uses the type of oldTask and the command line options to sequence tasks. The first task is created by the createFirstTask method of the parent.

Overrides:

createTaskAfter in class Main

Parameters:

oldTask - the previous task.

Returns:

The next task that needs to be done

createTempFile

public PrintStream createTempFile(JmlCompilationUnit cunit,
                                  String filename)