JML

org.jmlspecs.racwrap
Class Main

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.util.compiler.Compiler
          extended byorg.multijava.mjc.Main
              extended byorg.jmlspecs.checker.Main
                  extended byorg.jmlspecs.jmlrac.Main
                      extended byorg.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.

Constructor Detail

Main

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

Method Detail

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)

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.