envgen
Class EnvGenerator

java.lang.Object
  |
  +--envgen.EnvGenerator

public class EnvGenerator

extends java.lang.Object

Main class of the Environment Generator that processes command line options, loads classes, and redirects to either drivers or stubs generator.

Field Summary

static java.lang.String	analysisPackageName
static IApproach	approach
static Assumptions	assumptions
static boolean	atomicStepsMode Set to insert atomic steps into generated environment.
static boolean	cfgAnalysis
static int	chainLength Integer field that keeps track of value k in k-limiting.
static java.lang.String	code
static ICodeGenerator	codeGen
static java.lang.String	context Set to identify the framework to be used with the generated program (Bandera or JPF).
static int	debug Set to print debugging messages.
static boolean	driverMode Set to generate a driver for a given unit.
static boolean	dump
static java.util.HashMap	envTable Table of environment (external) classes.
static boolean	ifElseCodeCond Set to generate drivers using ifelse statements.
static java.lang.String	inputFileName
static boolean	mustSE
static int	numThreads Number of threads to be generated in the most general driver.
static boolean	ofaAnalysis
static java.lang.String	outputDirName
static boolean	packageAnalysis Analyze effects on fields that are relevant to certain package behavior (GUI, container)
static java.lang.String	packageName The name of the directory, where generated files are to be stored.
static boolean	printEnvActions Set to print out environment actions.
static boolean	returnSensitivity Analyze environment containers, preserving some of their internal structure.
static boolean	rwAnalysis
static boolean	safeLockAnalysis
static boolean	seAnalysis Set to use a side-effects analysis to discover side-effects information of the environment methods.
static boolean	singleEventCond Set to automatically generate a Single Event Condition and to combine it with a given specification.
static java.lang.String	sourceFileName Name of the java source file.
static java.lang.String	specFileName The name of the specification file.
static boolean	stubsMode Set to generate stubs.
static boolean	unitAnalysis Analyze unit and generate code based on the analysis
static java.util.HashMap	unitTable Table of unit (internal) classes.

Constructor Summary

(package private)

EnvGenerator(java.lang.String inputFileName)

Method Summary

static void	genDrivers()
static void	genStubs()
static void	getStatistics()
static void	main(java.lang.String[] args) Reads the command line options and launges generation of specified components.
Assumptions	performRWAnalysis()
static void	printHelp() Prints available options.
static void	processCmdLine(java.lang.String[] args) Processes command line input.
static void	processInput(java.lang.String[] args)
static java.lang.String[]	readInput(java.lang.String inputFileName)

Methods inherited from class java.lang.Object

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

Field Detail

unitTable

public static java.util.HashMap unitTable

Table of unit (internal) classes.

envTable

public static java.util.HashMap envTable

Table of environment (external) classes. It gets automatically discovered from the specification of the unit. Contains external classes with only those methods and fields that get referenced inside the unit. Hashtable is used to keep pairs (ClassName, Class) in order to be able to keep track of classes based on their names.

approach

public static IApproach approach

assumptions

public static Assumptions assumptions

codeGen

public static ICodeGenerator codeGen

inputFileName

public static java.lang.String inputFileName

driverMode

public static boolean driverMode

Set to generate a driver for a given unit. This is a default mode. By default generates the most general driver.

stubsMode

public static boolean stubsMode

Set to generate stubs.

specFileName

public static java.lang.String specFileName

The name of the specification file.

context

public static java.lang.String context

Set to identify the framework to be used with the generated program (Bandera or JPF). By default, JPF is used.

code

public static java.lang.String code

ifElseCodeCond

public static boolean ifElseCodeCond

Set to generate drivers using ifelse statements. By default switch statements are used.

singleEventCond

public static boolean singleEventCond

Set to automatically generate a Single Event Condition and to combine it with a given specification. By default, this condition is checked while traversing the buchi automaton.

atomicStepsMode

public static boolean atomicStepsMode

Set to insert atomic steps into generated environment.

printEnvActions

public static boolean printEnvActions

Set to print out environment actions.

packageName

public static java.lang.String packageName

The name of the directory, where generated files are to be stored.

outputDirName

public static java.lang.String outputDirName

numThreads

public static int numThreads

Number of threads to be generated in the most general driver. By default, 2 threads are generated.

sourceFileName

public static java.lang.String sourceFileName

Name of the java source file.

seAnalysis

public static boolean seAnalysis

Set to use a side-effects analysis to discover side-effects information of the environment methods.

rwAnalysis

public static boolean rwAnalysis

cfgAnalysis

public static boolean cfgAnalysis

chainLength

public static int chainLength

Integer field that keeps track of value k in k-limiting. The value can be varied by the user. The larger the value, the more precise information will be produced by the analyses. The default value is 2 which lets the analysis identify side-effects to obejcts and their fields, and fields of their fields.

returnSensitivity

public static boolean returnSensitivity

Analyze environment containers, preserving some of their internal structure.

mustSE

public static boolean mustSE

ofaAnalysis

public static boolean ofaAnalysis

packageAnalysis

public static boolean packageAnalysis

Analyze effects on fields that are relevant to certain package behavior (GUI, container)

analysisPackageName

public static java.lang.String analysisPackageName

unitAnalysis

public static boolean unitAnalysis

Analyze unit and generate code based on the analysis

safeLockAnalysis

public static boolean safeLockAnalysis

dump

public static boolean dump

debug

public static int debug

Set to print debugging messages.

Constructor Detail

EnvGenerator

EnvGenerator(java.lang.String inputFileName)

Method Detail

main

public static void main(java.lang.String[] args)

Reads the command line options and launges generation of specified components.

genDrivers

public static void genDrivers()

genStubs

public static void genStubs()

performRWAnalysis

public Assumptions performRWAnalysis()

printHelp

public static void printHelp()

Prints available options.

processCmdLine

public static void processCmdLine(java.lang.String[] args)

Processes command line input.

processInput

public static void processInput(java.lang.String[] args)

readInput

public static java.lang.String[] readInput(java.lang.String inputFileName)

getStatistics

public static void getStatistics()