public class TestCaseGenerator extends Object
Constructor and Description |
---|
TestCaseGenerator(Proof proof) |
TestCaseGenerator(Proof proof,
boolean rflAsInternalClass) |
public static final String JAVA_FILE_EXTENSION_WITH_DOT
public static final String NEW_LINE
Do not use \n
!
private static final String NULLABLE
public static final String ALL_OBJECTS
public static final String ALL_INTS
public static final String ALL_BOOLS
public static final String ALL_HEAPS
public static final String ALL_FIELDS
public static final String ALL_SEQ
public static final String ALL_LOCSETS
public static final String OBJENESIS_NAME
public static final String OLDMap
public static final String TAB
private Services services
static int fileCounter
private final boolean junitFormat
private static final String DONT_COPY
private final boolean rflAsInternalClass
protected boolean useRFL
protected ReflectionClassCreator rflCreator
private final String dontCopy
protected final String modDir
protected final String directory
private TestGenerationLog logger
private String fileName
private String packageName
private String MUTName
private ProofInfo info
private OracleGenerator oracleGenerator
private List<OracleMethod> oracleMethods
private String oracleMethodCall
private final Map<Sort,StringBuffer> sortDummyClass
final String DummyPostfix
private String compileWithOpenJML
private String executeWithOpenJML
public TestCaseGenerator(Proof proof)
public TestCaseGenerator(Proof proof, boolean rflAsInternalClass)
public static boolean modelIsOK(Model m)
private String createCompileWithOpenJML(String openJMLPath, String objenesisPath)
protected String computeProjectSubPath(String modelDir)
directory
) in which the generated files will be stored.modelDir
- The path to the source files of the performed Proof
.public String getMUTCall()
private void copyFiles(String srcName, String targName) throws IOException
IOException
protected void createDummyClasses() throws IOException
IOException
protected void writeRFLFile() throws IOException
IOException
public StringBuffer createRFLFileContent()
protected void createOpenJMLShellScript() throws IOException
IOException
protected void exportCodeUnderTest() throws IOException
IOException
private boolean filterVal(String s)
public String generateJUnitTestCase(Model m, Node n) throws IOException
IOException
protected String getOracleAssertion(List<OracleMethod> oracleMethods)
private Term getPostCondition()
public String generateJUnitTestSuite(Collection<SMTSolver> problemSolvers) throws IOException
IOException
public void initFileName()
public StringBuffer createTestCaseCotent(Collection<SMTSolver> problemSolvers)
private void generateTypeInferenceMapHelper(Term t, Map<String,Sort> map)
private ProgramVariable getProgramVariable(Term locationTerm)
private String getRemainingConstants(Collection<String> existingConstants, Collection<Term> newConstants)
private boolean isInPrestate(Collection<? extends ObjectVal> prestate, ObjectVal o)
private boolean isInPrestate(Collection<? extends ObjectVal> prestate, String name)
private StringBuffer getMainMethod(String className, int i)
private String createBoolSet()
private String createIntSet()
private String getTestMethodSignature(int i)
public boolean isJunit()
protected boolean isNumericType(String type)
protected boolean isPrimitiveType(String type)
public void setLogger(TestGenerationLog logger)
public void writeToFile(String file, StringBuffer sb) throws IOException
IOException
public boolean isUseRFL()
public String getFileName()
public void setFileName(String fileName)
public String getPackageName()
public void setPackageName(String packageName)
public boolean isRflAsInternalClass()