UTJML

edu.utep.cs.utjml.compiler
Class Main

java.lang.Object
  extended by org.multijava.util.Utils
      extended by org.multijava.util.compiler.Compiler
          extended by org.multijava.mjc.Main
              extended by org.jmlspecs.checker.Main
                  extended by org.jmlspecs.jmlrac.Main
                      extended by edu.utep.cs.utjml.compiler.Main
All Implemented Interfaces:
Cloneable, TroubleReporter

public class Main
extends Main

This class implements the entry point of the JML compiler. Use java org.jmlspecs.checker.Main --help to get usage options.


Nested Class Summary
 class Main.UtJmlParseTask
          This class parses a group of files, given by filenames as strings, and generates a forest of ASTs.
 
Nested classes/interfaces inherited from class org.jmlspecs.jmlrac.Main
Main.JavaParseTask, Main.JmlGenerateAssertionTask, Main.JmlPrettyPrintTask, Main.JmlWriteAssertionTask
 
Nested classes/interfaces inherited from class org.jmlspecs.checker.Main
Main.JmlCheckAssignableTask, Main.JmlParseTask, Main.JmlTypecheckTask
 
Nested classes/interfaces 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
static UtJmlOptions utjmlOptions
          Command-line options.
 
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()
          Constructs a JML RAC compiler with a default modifier utility.
 
Method Summary
 JCompilationUnitType catchUpRefinedFile(File file)
          Parses a file and returns the AST.
static boolean compile(String[] args)
          Second entry point.
static boolean compile(String[] args, UtJmlOptions opt, OutputStream os)
          Entry point for the GUI
protected  JmlRacGenerator createRacGenerator(RacOptions opt, Main main)
           
protected  void exposeOptions(JmlCommonOptions opt)
          Sets the static field, jmlOptions, to the given arugment so that typechecking routines can access command-line options.
 Main.ParseTask firstTask(ArrayList infiles)
          Generates the first task in the compilation sequence.
 Main.ParseTask firstTask(File filename, Main.ExpectedResult expected)
          Generates the first task in the compilation sequence.
protected  MjcCommonOptions getOptionsInstance(MjcCommonOptions opt)
          Assigns opt to the local instance of RacOptions, assigns opt to an instance of jmlOptions in the checker, and returns opt as an instance of MjcCommonOptions so it can be assigned to the options variable in mjc's Main.
static boolean hasOptionXcs()
          Returns true if the -Xcs, call sequence, is specified.
static boolean hasOptionXtgen()
          Returns true if the -Xtgen, test case generation, is specified.
protected  void initSession()
          Initializes the "class loader" for this compilation session.
static void main(String[] args)
          The entry point when starting this program from the command line.
protected  MjcCommonOptions makeOptionsInstance()
          Creates an object to do the parsing of the command line arguments and to store the values of the flags and options so obtained (it does not actually do the argument parsing).
 
Methods inherited from class org.jmlspecs.jmlrac.Main
classToGenerate, compile, createCompilationUnitContext, createTaskAfter, getFileMap, hasOptionXsymr, hasOptionXsymw, initSecondSession, isSpecMode, prepareSecondRound, setFileMap
 
Methods inherited from class org.jmlspecs.checker.Main
canStopSequenceBeforeAllPasses, catchUpTask, compile, filenameFilter, getDefaultFilter, getWarningFilterNameFromOptions, hasOptionXobspure, hasUnsafeOpWarningOption, includeAllRefinedCUnits, initialize, 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

utjmlOptions

public static UtJmlOptions utjmlOptions
Command-line options.

 invariant racOptions == options;
 

Constructor Detail

Main

public Main()
Constructs a JML RAC compiler with a default modifier utility.

Method Detail

main

public static void main(String[] args)
The entry point when starting this program from the command line.

Parameters:
args - the command line arguments

compile

public static boolean compile(String[] args)
Second entry point. This function is overridden from mjc.Main so that we can * instantiate a derived class Main object.


compile

public static boolean compile(String[] args,
                              UtJmlOptions opt,
                              OutputStream os)
Entry point for the GUI

Parameters:
args - the file, package, and directory names
opt - the options for the tool
os - the output stream for the compiler messages

firstTask

public Main.ParseTask firstTask(ArrayList infiles)
Generates the first task in the compilation sequence. This is a method so subclasses can modify the task sequence.

 also
   requires infiles != null && (\forall Object o; infiles.contains(o);
                                  o instanceof String);
 

Overrides:
firstTask in class Main

firstTask

public Main.ParseTask firstTask(File filename,
                                Main.ExpectedResult expected)
Generates the first task in the compilation sequence. This method returns JML parser if this is the first round; otherwise, this method returns Java parser.

Overrides:
firstTask in class Main

makeOptionsInstance

protected MjcCommonOptions makeOptionsInstance()
Creates an object to do the parsing of the command line arguments and to store the values of the flags and options so obtained (it does not actually do the argument parsing). It is overridden here from mjc.Main so that we can instantiate a RacOptions object, in order to parse some new options specific to this compiler (cf. RacOptions.opt).

Overrides:
makeOptionsInstance in class Main
See Also:
RacOptions

getOptionsInstance

protected MjcCommonOptions getOptionsInstance(MjcCommonOptions opt)
Assigns opt to the local instance of RacOptions, assigns opt to an instance of jmlOptions in the checker, and returns opt as an instance of MjcCommonOptions so it can be assigned to the options variable in mjc's Main. This is done so we can access options that are only processed in MjcCommonOptions.

Overrides:
getOptionsInstance in class Main

exposeOptions

protected void exposeOptions(JmlCommonOptions opt)
Sets the static field, jmlOptions, to the given arugment so that typechecking routines can access command-line options.

 assignable jmlOptions;
 ensures jmlOptions == opt;
 

Overrides:
exposeOptions in class Main

initSession

protected void initSession()
Initializes the "class loader" for this compilation session.

Overrides:
initSession in class Main

catchUpRefinedFile

public JCompilationUnitType catchUpRefinedFile(File file)
Parses a file and returns the AST.

 requires file != null;
 

Overrides:
catchUpRefinedFile in class Main

createRacGenerator

protected JmlRacGenerator createRacGenerator(RacOptions opt,
                                             Main main)
Overrides:
createRacGenerator in class Main

hasOptionXcs

public static boolean hasOptionXcs()
Returns true if the -Xcs, call sequence, is specified.


hasOptionXtgen

public static boolean hasOptionXtgen()
Returns true if the -Xtgen, test case generation, is specified.


UTJML

UTJML is Copyright (C) 2004-2006 by University of Texas at El Paso 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 JML project.