public class TestCaseGenerator
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
ALL_BOOLS |
static java.lang.String |
ALL_FIELDS |
static java.lang.String |
ALL_HEAPS |
static java.lang.String |
ALL_INTS |
static java.lang.String |
ALL_LOCSETS |
static java.lang.String |
ALL_OBJECTS |
static java.lang.String |
ALL_SEQ |
private java.lang.String |
compileWithOpenJML |
protected java.lang.String |
directory |
private static java.lang.String |
DONT_COPY |
private java.lang.String |
dontCopy |
(package private) java.lang.String |
DummyPostfix |
private java.lang.String |
executeWithOpenJML |
(package private) static int |
fileCounter |
private java.lang.String |
fileName |
private ProofInfo |
info |
static java.lang.String |
JAVA_FILE_EXTENSION_WITH_DOT
The Java source file extension with a leading dot.
|
private boolean |
junitFormat |
private TestGenerationLog |
logger |
protected java.lang.String |
modDir |
private java.lang.String |
MUTName |
static java.lang.String |
NEW_LINE
Constant for the line break which is used by the operating system.
|
private static java.lang.String |
NULLABLE |
static java.lang.String |
OBJENESIS_NAME |
static java.lang.String |
OLDMap |
private OracleGenerator |
oracleGenerator |
private java.lang.String |
oracleMethodCall |
private java.util.List<OracleMethod> |
oracleMethods |
private java.lang.String |
packageName |
private boolean |
rflAsInternalClass |
protected ReflectionClassCreator |
rflCreator |
private Services |
services |
private java.util.Map<Sort,java.lang.StringBuffer> |
sortDummyClass |
static java.lang.String |
TAB |
protected boolean |
useRFL |
Constructor and Description |
---|
TestCaseGenerator(Proof proof) |
TestCaseGenerator(Proof proof,
boolean rflAsInternalClass) |
Modifier and Type | Method and Description |
---|---|
protected java.lang.String |
buildDummyClassForAbstractSort(Sort sort) |
protected java.lang.String |
computeProjectSubPath(java.lang.String modelDir)
Computes the project specific sub path of the output directory
(
directory ) in which the generated files will be stored. |
private void |
copyFiles(java.lang.String srcName,
java.lang.String targName) |
private java.lang.String |
createBoolSet() |
private java.lang.String |
createCompileWithOpenJML(java.lang.String openJMLPath,
java.lang.String objenesisPath) |
protected void |
createDummyClasses() |
private java.lang.String |
createExecuteWithOpenJML(java.lang.String path,
java.lang.String objenesisPath) |
private java.lang.String |
createIntSet() |
private java.lang.String |
createObjectName(ObjectVal o) |
private java.lang.String |
createObjSet(Heap h) |
private java.lang.String |
createOldMap(java.util.Set<java.lang.String> objNames) |
protected void |
createOpenJMLShellScript() |
java.lang.StringBuffer |
createRFLFileContent()
Used by the Eclipse integration to creat the content of the RFL file.
|
java.lang.StringBuffer |
createTestCaseCotent(java.util.Collection<SMTSolver> problemSolvers) |
protected void |
exportCodeUnderTest() |
private boolean |
filterVal(java.lang.String s) |
java.lang.String |
generateJUnitTestCase(Model m,
Node n) |
java.lang.String |
generateJUnitTestSuite(java.util.Collection<SMTSolver> problemSolvers) |
java.lang.String |
generateModifierSetAssertions(Model m) |
java.lang.String |
generateTestCase(Model m,
java.util.Map<java.lang.String,Sort> typeInfMap) |
protected java.util.Map<java.lang.String,Sort> |
generateTypeInferenceMap(Node n) |
private void |
generateTypeInferenceMapHelper(Term t,
java.util.Map<java.lang.String,Sort> map) |
private java.lang.String |
getDummyClassNameFor(Sort sort) |
java.lang.String |
getFileName() |
private java.lang.String |
getFilePrefix(java.lang.String className,
java.lang.String packageName) |
private java.lang.StringBuffer |
getMainMethod(java.lang.String className,
int i) |
java.lang.String |
getMUTCall() |
private ObjectVal |
getObject(Heap h,
java.lang.String name) |
protected java.lang.String |
getOracleAssertion(java.util.List<OracleMethod> oracleMethods) |
java.lang.String |
getPackageName() |
private Term |
getPostCondition() |
private java.lang.String |
getPreName(java.lang.String val) |
private ProgramVariable |
getProgramVariable(Term locationTerm) |
private java.lang.String |
getRemainingConstants(java.util.Collection<java.lang.String> existingConstants,
java.util.Collection<Term> newConstants) |
java.lang.String |
getSafeType(Sort sort) |
private java.lang.String |
getTestMethodSignature(int i) |
private java.lang.String |
getTypeOfValue(Heap heap,
Model m,
java.lang.String val) |
protected java.lang.String |
inferSort(java.util.Map<java.lang.String,Sort> typeInfMap,
java.lang.String progVar) |
void |
initFileName() |
private boolean |
isInPrestate(java.util.Collection<? extends ObjectVal> prestate,
ObjectVal o) |
private boolean |
isInPrestate(java.util.Collection<? extends ObjectVal> prestate,
java.lang.String name) |
boolean |
isJunit() |
protected boolean |
isNumericType(java.lang.String type) |
protected boolean |
isPrimitiveType(java.lang.String type) |
boolean |
isRflAsInternalClass() |
boolean |
isUseRFL() |
static boolean |
modelIsOK(Model m) |
void |
setFileName(java.lang.String fileName) |
void |
setLogger(TestGenerationLog logger) |
void |
setPackageName(java.lang.String packageName) |
protected java.lang.String |
translateValueExpression(java.lang.String val) |
protected void |
writeRFLFile()
Creates the RFL.java file, that provides setter and getter methods using the reflection API
as well as object creation functions based on the objenesis library.
|
void |
writeToFile(java.lang.String file,
java.lang.StringBuffer sb) |
public static final java.lang.String JAVA_FILE_EXTENSION_WITH_DOT
public static final java.lang.String NEW_LINE
Do not use \n
!
private static final java.lang.String NULLABLE
public static final java.lang.String ALL_OBJECTS
public static final java.lang.String ALL_INTS
public static final java.lang.String ALL_BOOLS
public static final java.lang.String ALL_HEAPS
public static final java.lang.String ALL_FIELDS
public static final java.lang.String ALL_SEQ
public static final java.lang.String ALL_LOCSETS
public static final java.lang.String OBJENESIS_NAME
public static final java.lang.String OLDMap
public static final java.lang.String TAB
private Services services
static int fileCounter
private final boolean junitFormat
private static final java.lang.String DONT_COPY
private final boolean rflAsInternalClass
protected boolean useRFL
protected ReflectionClassCreator rflCreator
private final java.lang.String dontCopy
protected final java.lang.String modDir
protected final java.lang.String directory
private TestGenerationLog logger
private java.lang.String fileName
private java.lang.String packageName
private java.lang.String MUTName
private ProofInfo info
private OracleGenerator oracleGenerator
private java.util.List<OracleMethod> oracleMethods
private java.lang.String oracleMethodCall
private final java.util.Map<Sort,java.lang.StringBuffer> sortDummyClass
final java.lang.String DummyPostfix
private java.lang.String compileWithOpenJML
private java.lang.String executeWithOpenJML
public TestCaseGenerator(Proof proof)
public TestCaseGenerator(Proof proof, boolean rflAsInternalClass)
public static boolean modelIsOK(Model m)
private java.lang.String createCompileWithOpenJML(java.lang.String openJMLPath, java.lang.String objenesisPath)
private java.lang.String createExecuteWithOpenJML(java.lang.String path, java.lang.String objenesisPath)
protected java.lang.String computeProjectSubPath(java.lang.String modelDir)
directory
) in which the generated files will be stored.modelDir
- The path to the source files of the performed Proof
.public java.lang.String getMUTCall()
protected java.lang.String buildDummyClassForAbstractSort(Sort sort)
private void copyFiles(java.lang.String srcName, java.lang.String targName) throws java.io.IOException
java.io.IOException
protected void createDummyClasses() throws java.io.IOException
java.io.IOException
protected void writeRFLFile() throws java.io.IOException
java.io.IOException
public java.lang.StringBuffer createRFLFileContent()
protected void createOpenJMLShellScript() throws java.io.IOException
java.io.IOException
protected void exportCodeUnderTest() throws java.io.IOException
java.io.IOException
private boolean filterVal(java.lang.String s)
public java.lang.String generateJUnitTestCase(Model m, Node n) throws java.io.IOException
java.io.IOException
protected java.lang.String getOracleAssertion(java.util.List<OracleMethod> oracleMethods)
private Term getPostCondition()
public java.lang.String generateJUnitTestSuite(java.util.Collection<SMTSolver> problemSolvers) throws java.io.IOException
java.io.IOException
public void initFileName()
public java.lang.StringBuffer createTestCaseCotent(java.util.Collection<SMTSolver> problemSolvers)
protected java.lang.String inferSort(java.util.Map<java.lang.String,Sort> typeInfMap, java.lang.String progVar)
protected java.util.Map<java.lang.String,Sort> generateTypeInferenceMap(Node n)
private void generateTypeInferenceMapHelper(Term t, java.util.Map<java.lang.String,Sort> map)
private ProgramVariable getProgramVariable(Term locationTerm)
private java.lang.String getRemainingConstants(java.util.Collection<java.lang.String> existingConstants, java.util.Collection<Term> newConstants)
private boolean isInPrestate(java.util.Collection<? extends ObjectVal> prestate, ObjectVal o)
private boolean isInPrestate(java.util.Collection<? extends ObjectVal> prestate, java.lang.String name)
public java.lang.String generateModifierSetAssertions(Model m)
public java.lang.String generateTestCase(Model m, java.util.Map<java.lang.String,Sort> typeInfMap)
private java.lang.String createOldMap(java.util.Set<java.lang.String> objNames)
private java.lang.String getPreName(java.lang.String val)
private java.lang.String createObjectName(ObjectVal o)
private java.lang.String getDummyClassNameFor(Sort sort)
private java.lang.String getFilePrefix(java.lang.String className, java.lang.String packageName)
private java.lang.StringBuffer getMainMethod(java.lang.String className, int i)
private java.lang.String createBoolSet()
private java.lang.String createIntSet()
private java.lang.String createObjSet(Heap h)
public java.lang.String getSafeType(Sort sort)
private java.lang.String getTestMethodSignature(int i)
public boolean isJunit()
protected boolean isNumericType(java.lang.String type)
protected boolean isPrimitiveType(java.lang.String type)
public void setLogger(TestGenerationLog logger)
protected java.lang.String translateValueExpression(java.lang.String val)
public void writeToFile(java.lang.String file, java.lang.StringBuffer sb) throws java.io.IOException
java.io.IOException
public boolean isUseRFL()
public java.lang.String getFileName()
public void setFileName(java.lang.String fileName)
public java.lang.String getPackageName()
public void setPackageName(java.lang.String packageName)
public boolean isRflAsInternalClass()