JML

org.jmlspecs.jmlspec
Class Main

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.util.compiler.Compiler
          extended byorg.multijava.mjc.Main
              extended byorg.jmlspecs.jmlspec.Main
All Implemented Interfaces:
Cloneable, Constants, Constants, TroubleReporter

public class Main
extends Main
implements Constants

A class implementing the entry point of the jmlspec specification skeleton generator/comparator. Use java org.jmlspecs.jmlspec.Main --help to get usage options.

Version:
$Revision: 1.27 $
Author:
David Cok

Nested Class Summary
 class Main.JspBinaryPrinterTask
           
 class Main.JspCompareTask
          A task for generating specification skeletons.
 class Main.JspParseTask
          A task for generating specification skeletons.
 class Main.JspPrettyPrinterTask
          A task for generating specification skeletons.
(package private) static class Main.SuffixFilter
          This class is used with the Directory.list method to list those files in a directory that this program is interested in processing - in this case, all those that end in a valid suffix.
 
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.Filter, Main.ParseTask, Main.PreprocessTask, Main.PrettyPrintTask, Main.ResolveSpecializerTask, Main.ResolveTopMethodTask, Main.Task, Main.TaskTimes, Main.TranslateMJTask, Main.TreeProcessingTask, Main.Trees, Main.TypecheckTask
 
Field Summary
(package private) static String[] also
           
protected static String[] annotation
           
(package private)  ArrayList binaries
           
protected static String[] classAnnotation
           
(package private) static String[] comment
           
static int javaSuffixIndex
           
(package private)  Map map
          Map of fully-qualified class names (/-separated) to the arrays of ASTs that hold the parsed versions of all of the refinement files.
(package private) static String[] nocomment
           
static int PRI_SKELETON_GENERATION
          The task priority for generating test class.
static String[] validSuffixes
          Valid suffixes for specification files.
 
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
 
Fields inherited from interface org.multijava.mjc.Constants
ACC_MODIFIER_FLAGS_MASK, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_PURE, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, IMPLICITLY_NON_NULL, JAV_ASSERTION_ERROR, JAV_CLASS, JAV_CLASSLOADER, JAV_CLASSNOTFOUND_EXCEPTION, JAV_CLONE, JAV_CLONEABLE, JAV_CONSTRUCTOR, JAV_ERROR, JAV_EXCEPTION, JAV_INIT, JAV_LENGTH, JAV_NAME_SEPARATOR, JAV_NOCLASSDEFFOUND_ERROR, JAV_OBJECT, JAV_OUTER_THIS, JAV_RMJ_RUNTIME_EXCEPTION, JAV_RUNTIME, JAV_RUNTIME_EXCEPTION, JAV_SERIALIZABLE, JAV_STATIC_INIT, JAV_STRING, JAV_STRINGBUFFER, JAV_SUPER, JAV_THIS, JAV_THROWABLE, MJ_ANCHOR, NULLITY_MODS, OPE_BAND, OPE_BNOT, OPE_BOR, OPE_BSR, OPE_BXOR, OPE_EQ, OPE_GE, OPE_GT, OPE_LAND, OPE_LE, OPE_LNOT, OPE_LOR, OPE_LT, OPE_MINUS, OPE_NE, OPE_PERCENT, OPE_PLUS, OPE_POSTDEC, OPE_POSTINC, OPE_PREDEC, OPE_PREINC, OPE_SIMPLE, OPE_SL, OPE_SLASH, OPE_SR, OPE_STAR, TID_ARRAY, TID_BOOLEAN, TID_BYTE, TID_CHAR, TID_CLASS, TID_DOUBLE, TID_FLOAT, TID_INT, TID_LONG, TID_MAX, TID_SHORT, TID_VOID, UNIV_ARRAY_TMP, UNIV_TMP
 
Fields inherited from interface org.multijava.util.classfile.Constants
ACC_ABSTRACT, ACC_FINAL, ACC_INTERFACE, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_STRICT, ACC_SUPER, ACC_SYNCHRONIZED, ACC_SYNTHETIC, ACC_TRANSIENT, ACC_VOLATILE, ATT_ANCHOR, ATT_BRIDGE, ATT_CODE, ATT_CONSTANTVALUE, ATT_DEPRECATED, ATT_DISPATCHER, ATT_EXCEPTIONS, ATT_GENERIC, ATT_GENERIC_FUNCTIONS, ATT_INNERCLASSES, ATT_LINENUMBERTABLE, ATT_LOCALVARIABLETABLE, ATT_MM_BODY, ATT_REDIRECTOR, ATT_RMJ_GLUE, ATT_RMJ_SIGNATURE, ATT_RUNTIME_VISIBLE_ANNOTATIONS, ATT_RUNTIME_VISIBLE_PARAMETER_ANNOTATIONS, ATT_SIGNATURE, ATT_SOURCEFILE, ATT_SYNTHETIC, ATT_UNIVERSE_FIELD, ATT_UNIVERSE_METHOD, ATT_UNIVERSE_VERSION, CST_CLASS, CST_DOUBLE, CST_FIELD, CST_FLOAT, CST_INTEGER, CST_INTERFACEMETHOD, CST_LONG, CST_METHOD, CST_NAMEANDTYPE, CST_STRING, CST_UTF8, ENV_DEBUG_MODE, ENV_USE_CACHE, JAVA_MAGIC, JAVA_MAJOR, JAVA_MINOR, MAX_CODE_PER_METHOD, opc_aaload, opc_aastore, opc_aconst_null, opc_aload, opc_aload_0, opc_aload_1, opc_aload_2, opc_aload_3, opc_anewarray, opc_areturn, opc_arraylength, opc_astore, opc_astore_0, opc_astore_1, opc_astore_2, opc_astore_3, opc_athrow, opc_baload, opc_bastore, opc_bipush, opc_caload, opc_castore, opc_checkcast, opc_d2f, opc_d2i, opc_d2l, opc_dadd, opc_daload, opc_dastore, opc_dcmpg, opc_dcmpl, opc_dconst_0, opc_dconst_1, opc_ddiv, opc_dload, opc_dload_0, opc_dload_1, opc_dload_2, opc_dload_3, opc_dmul, opc_dneg, opc_drem, opc_dreturn, opc_dstore, opc_dstore_0, opc_dstore_1, opc_dstore_2, opc_dstore_3, opc_dsub, opc_dup, opc_dup2, opc_dup2_x1, opc_dup2_x2, opc_dup_x1, opc_dup_x2, opc_f2d, opc_f2i, opc_f2l, opc_fadd, opc_faload, opc_fastore, opc_fcmpg, opc_fcmpl, opc_fconst_0, opc_fconst_1, opc_fconst_2, opc_fdiv, opc_fload, opc_fload_0, opc_fload_1, opc_fload_2, opc_fload_3, opc_fmul, opc_fneg, opc_frem, opc_freturn, opc_fstore, opc_fstore_0, opc_fstore_1, opc_fstore_2, opc_fstore_3, opc_fsub, opc_getfield, opc_getstatic, opc_goto, opc_goto_w, opc_i2b, opc_i2c, opc_i2d, opc_i2f, opc_i2l, opc_i2s, opc_iadd, opc_iaload, opc_iand, opc_iastore, opc_iconst_0, opc_iconst_1, opc_iconst_2, opc_iconst_3, opc_iconst_4, opc_iconst_5, opc_iconst_m1, opc_idiv, opc_if_acmpeq, opc_if_acmpne, opc_if_icmpeq, opc_if_icmpge, opc_if_icmpgt, opc_if_icmple, opc_if_icmplt, opc_if_icmpne, opc_ifeq, opc_ifge, opc_ifgt, opc_ifle, opc_iflt, opc_ifne, opc_ifnonnull, opc_ifnull, opc_iinc, opc_iload, opc_iload_0, opc_iload_1, opc_iload_2, opc_iload_3, opc_imul, opc_ineg, opc_instanceof, opc_invokeinterface, opc_invokespecial, opc_invokestatic, opc_invokevirtual, opc_ior, opc_irem, opc_ireturn, opc_ishl, opc_ishr, opc_istore, opc_istore_0, opc_istore_1, opc_istore_2, opc_istore_3, opc_isub, opc_iushr, opc_ixor, opc_jsr, opc_jsr_w, opc_l2d, opc_l2f, opc_l2i, opc_ladd, opc_laload, opc_land, opc_lastore, opc_lcmp, opc_lconst_0, opc_lconst_1, opc_ldc, opc_ldc2_w, opc_ldc_w, opc_ldiv, opc_lload, opc_lload_0, opc_lload_1, opc_lload_2, opc_lload_3, opc_lmul, opc_lneg, opc_lookupswitch, opc_lor, opc_lrem, opc_lreturn, opc_lshl, opc_lshr, opc_lstore, opc_lstore_0, opc_lstore_1, opc_lstore_2, opc_lstore_3, opc_lsub, opc_lushr, opc_lxor, opc_monitorenter, opc_monitorexit, opc_multianewarray, opc_new, opc_newarray, opc_nop, opc_pop, opc_pop2, opc_putfield, opc_putstatic, opc_ret, opc_return, opc_saload, opc_sastore, opc_sipush, opc_swap, opc_tableswitch, opc_wide, opc_xxxunusedxxx, POO_ASCII_CONSTANT, POO_CLASS_CONSTANT, POO_DOUBLE_CONSTANT, POO_FLOAT_CONSTANT, POO_INTEGER_CONSTANT, POO_LONG_CONSTANT, POO_NAT_CONSTANT, POO_REF_CONSTANT, POO_STRING_CONSTANT, TYP_ADDRESS, TYP_DOUBLE, TYP_FLOAT, TYP_INT, TYP_LONG, TYP_REFERENCE, TYP_VOID
 
Constructor Summary
Main()
           
 
Method Summary
 String checkPackageName(String packageName, boolean quiet)
          Checks whether a syntactically valid package name actually exists, and returns the directory location of the root of the package or null if there is no package by that name on the sourcepath or classpath.
static boolean compile(String[] args)
          Generates JML skeleton with the given argument, args, and returns true if all the skeletons are successfully generated.
static boolean compile(String[] args, JspOptions opt, OutputStream os)
          Entry point for the GUI
protected  Main.Task createTaskAfter(Main.Task oldTask)
          Adds JspPrettyPrinterTask or JspCompareTask after the regular parsing.
 void doBinaries()
           
protected  FilenameFilter filenameFilter()
          This filter returns all the files that are processed when a directory or package is named on the command-line.
(package private)  File findFile(String qname, String suffix)
           
static int findSuffixIndex(String s)
          Generates an int corresponding to the suffix; no particular order, just has to be unique - used as the index into an array.
 Main.ParseTask firstTask(ArrayList infiles)
          Generates the first task in the compilation sequence.
protected  MjcCommonOptions getOptionsInstance(MjcCommonOptions opt)
          Returns opt as an instance of MjcCommonOptions so it can be assigned to the options variable in mjc's Main.
protected  String getWarningFilterNameFromOptions(MjcCommonOptions opts)
          Get the warning filter's class name from the options structure.
 void handlePackages(ArrayList packages, ArrayList dirs, ArrayList infiles)
          Processes all the package names found on the command-line, altering the list of directories or files as appropriate.
static void main(String[] args)
          An entry point when starting from the command line.
protected  MjcCommonOptions makeOptionsInstance()
          This function 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).
protected  boolean runInitialization(String[] args)
          Invoked from within the method run to do the argument parsing and compiler setup prior to actually parsing files via the task mechanism; returns true if no errors are encountered during initialization; if false is returned the initialization is not necessarily complete.
protected  void runSetInitialTasks(ArrayList infiles)
          Sets up the initial tasks that start the parsing.
 void setTemplates(JspOptions options)
           
 
Methods inherited from class org.multijava.mjc.Main
activeSequenceID, adoptCompilationUnitContext, bugReportBoilerplate, bugReportProperty, bugReportRequest, catchUp, catchUp, catchUpGF, catchUpType, classToGenerate, compile, contextBehavior, createCompilationUnitContext, currentlyParsingFor, expandAtFiles, experimentalArrayHandling, failedParsing, firstCheckingTask, firstTask, genCode, Generic, Generic, getClasses, getDefaultFilter, getFilter, handleDirectories, handleNonOptions, handlePackageName, hasAlreadyFailedToParseFor, hasAlreadySuccessfullyParsed, initialize, initSession, initSession, interruptCompilation, isAnExpectedResult, isCurrentlyParsingFor, mainSequenceID, nonNullTypes, noteError, optimizeCode, options, parseArguments, parseAtFile, parseComments, prettyPrint, processTaskQueue, quietMode, RecommendedWarning, reportTrouble, reportTroubleFiltered, RMJ, run, run, runCompilation, runParser, 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

binaries

ArrayList binaries

map

Map map
Map of fully-qualified class names (/-separated) to the arrays of ASTs that hold the parsed versions of all of the refinement files.


PRI_SKELETON_GENERATION

public static final int PRI_SKELETON_GENERATION
The task priority for generating test class.


validSuffixes

public static final String[] validSuffixes
Valid suffixes for specification files.


javaSuffixIndex

public static final int javaSuffixIndex

annotation

protected static String[] annotation

classAnnotation

protected static String[] classAnnotation

nocomment

static final String[] nocomment

comment

static final String[] comment

also

static final String[] also
Constructor Detail

Main

public Main()
Method Detail

main

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

Parameters:
args - The command line arguments

compile

public static boolean compile(String[] args)
Generates JML skeleton with the given argument, args, and returns true if all the skeletons are successfully generated.


compile

public static boolean compile(String[] args,
                              JspOptions 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

runInitialization

protected boolean runInitialization(String[] args)
Description copied from class: Main
Invoked from within the method run to do the argument parsing and compiler setup prior to actually parsing files via the task mechanism; returns true if no errors are encountered during initialization; if false is returned the initialization is not necessarily complete.

Overrides:
runInitialization in class Main

handlePackages

public void handlePackages(ArrayList packages,
                           ArrayList dirs,
                           ArrayList infiles)
Description copied from class: Main
Processes all the package names found on the command-line, altering the list of directories or files as appropriate. The implementation for mjc simply converts package names to the absolute path names of the directories in which they are found (per the sourcepath and classpath) and adds the directory to the list in dirs.

Overrides:
handlePackages in class Main

checkPackageName

public String checkPackageName(String packageName,
                               boolean quiet)
Description copied from class: Main
Checks whether a syntactically valid package name actually exists, and returns the directory location of the root of the package or null if there is no package by that name on the sourcepath or classpath.

Overrides:
checkPackageName in class Main

filenameFilter

protected FilenameFilter filenameFilter()
This filter returns all the files that are processed when a directory or package is named on the command-line.

Overrides:
filenameFilter in class Main

makeOptionsInstance

protected MjcCommonOptions makeOptionsInstance()
This function 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 JspOptions object, in order to parse some new options specific to this compiler (cf. JspOptions.opt).

Overrides:
makeOptionsInstance in class Main
See Also:
JspOptions

getOptionsInstance

protected MjcCommonOptions getOptionsInstance(MjcCommonOptions opt)
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

getWarningFilterNameFromOptions

protected String getWarningFilterNameFromOptions(MjcCommonOptions opts)
Description copied from class: Main
Get the warning filter's class name from the options structure. This is a hook method that can be overridden by subclasses.

Overrides:
getWarningFilterNameFromOptions in class Main

firstTask

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

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

Overrides:
firstTask in class Main

runSetInitialTasks

protected void runSetInitialTasks(ArrayList infiles)
Description copied from class: Main
Sets up the initial tasks that start the parsing. Additional tasks may be generated if these files reference other classes that need parsing.

Overrides:
runSetInitialTasks in class Main

createTaskAfter

protected Main.Task createTaskAfter(Main.Task oldTask)
Adds JspPrettyPrinterTask or JspCompareTask after the regular parsing. Note that we only do the parsing, no other checking.

Overrides:
createTaskAfter in class Main

doBinaries

public void doBinaries()

findFile

File findFile(String qname,
              String suffix)

findSuffixIndex

public static int findSuffixIndex(String s)
Generates an int corresponding to the suffix; no particular order, just has to be unique - used as the index into an array.


setTemplates

public void setTemplates(JspOptions options)

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.