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 |
protected java.lang.String |
directory |
static java.lang.String |
JAVA_FILE_EXTENSION_WITH_DOT
The Java source file extension with a leading dot.
|
protected java.lang.String |
modDir |
static java.lang.String |
NEW_LINE
Constant for the line break which is used by the operating system.
|
static java.lang.String |
OBJENESIS_NAME |
static java.lang.String |
OLDMap |
protected ReflectionClassCreator |
rflCreator |
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. |
protected void |
createDummyClasses() |
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() |
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) |
java.lang.String |
getFileName() |
java.lang.String |
getMUTCall() |
protected java.lang.String |
getOracleAssertion(java.util.List<OracleMethod> oracleMethods) |
java.lang.String |
getPackageName() |
java.lang.String |
getSafeType(Sort sort) |
protected java.lang.String |
inferSort(java.util.Map<java.lang.String,Sort> typeInfMap,
java.lang.String progVar) |
void |
initFileName() |
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
!
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
protected boolean useRFL
protected ReflectionClassCreator rflCreator
protected final java.lang.String modDir
protected final java.lang.String directory
public TestCaseGenerator(Proof proof)
public TestCaseGenerator(Proof proof, boolean rflAsInternalClass)
public static boolean modelIsOK(Model m)
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)
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
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)
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)
public java.lang.String generateModifierSetAssertions(Model m)
public java.lang.String generateTestCase(Model m, java.util.Map<java.lang.String,Sort> typeInfMap)
public java.lang.String getSafeType(Sort sort)
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()
Copyright © 2003-2019 The KeY-Project.