de.uka.ilkd.key.util.rifl

Class RIFLTransformer

java.lang.Object

de.uka.ilkd.key.util.rifl.RIFLTransformer

public class RIFLTransformer
extends java.lang.Object

Facet class for interpreting RIFL specifications. The Requirements for Information Flow Language (RIFL) is a tool-independent specification language developed in the RS3 project. Method transform reads a RIFL file and Java sources and writes JML* information flow specifications to the original Java files.

changes (weigl, 2016-08-16): changed interfaces to File. This avoid some crud string operations on filenames

Author:

bruns, weigl, 2016-08-17

Field Summary

Fields

Modifier and Type	Field and Description
private static JavaProgramFactory	JPF
private java.util.List<java.io.File>	result

Constructor Summary

Constructors

Constructor and Description
RIFLTransformer()

Method Summary

Modifier and Type	Method and Description
void	doTransform(java.io.File riflFilename, java.io.File source, java.io.File savePath)
private void	ensureTargetDirExists(java.io.File target)
private static java.io.File	getBaseDirPath(java.io.File origSourcePath)
static java.io.File	getDefaultSavePath(java.io.File origSourcePath) Returns the default save path for transformed Java files.
java.util.List<java.io.File>	getProblemFiles()
static void	main(java.lang.String[] args) Entry point for the stand-alone RIFL to JML* tool.
private java.util.Map<CompilationUnit,java.io.File>	readJava(java.io.File root)
private SpecificationContainer	readRIFL(java.io.File fileName)
private java.io.File	relative(java.io.File root, java.io.File javaFile)
static boolean	transform(java.io.File riflFilename, java.io.File javaSource)
static boolean	transform(java.io.File riflFilename, java.io.File javaSource, java.io.File savePath, KeYRecoderExcHandler kexh) Transforms plain Java files + RIFL specification to Java+JML* specifications.
static boolean	transform(java.io.File riflFilename, java.io.File javaSource, KeYRecoderExcHandler kexh)
private void	writeJavaFile(java.io.File target, CompilationUnit cu) Writes a single Java file.
private void	writeProblemFile(java.io.File problemFileName, java.lang.String newJavaFolder, java.lang.String poname)

Methods inherited from class java.lang.Object

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

Field Detail

result

private java.util.List<java.io.File> result

JPF

private static final JavaProgramFactory JPF

Constructor Detail

RIFLTransformer

public RIFLTransformer()
                throws javax.xml.parsers.ParserConfigurationException,
                       org.xml.sax.SAXException

Throws:

javax.xml.parsers.ParserConfigurationException

org.xml.sax.SAXException

Method Detail

main

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

Entry point for the stand-alone RIFL to JML* tool.

transform

public static boolean transform(java.io.File riflFilename,
                                java.io.File javaSource,
                                java.io.File savePath,
                                KeYRecoderExcHandler kexh)

Transforms plain Java files + RIFL specification to Java+JML* specifications.

Parameters:

riflFilename - path to a RIFL file

javaSource - path to Java sources (should be a directory)

savePath - custom save path

kexh -

transform

public static boolean transform(java.io.File riflFilename,
                                java.io.File javaSource,
                                KeYRecoderExcHandler kexh)

transform

public static boolean transform(java.io.File riflFilename,
                                java.io.File javaSource)

getDefaultSavePath

public static java.io.File getDefaultSavePath(java.io.File origSourcePath)

Returns the default save path for transformed Java files.

Parameters:

origSourcePath - path to a directory or single Java file

Returns:

path to the transformed directory

getBaseDirPath

private static java.io.File getBaseDirPath(java.io.File origSourcePath)

readJava

private java.util.Map<CompilationUnit,java.io.File> readJava(java.io.File root)
                                                      throws java.io.IOException,
                                                             ParserException

Throws:

java.io.IOException

ParserException

relative

private java.io.File relative(java.io.File root,
                              java.io.File javaFile)

readRIFL

private SpecificationContainer readRIFL(java.io.File fileName)
                                 throws java.io.IOException,
                                        org.xml.sax.SAXException,
                                        javax.xml.parsers.ParserConfigurationException

Throws:

java.io.IOException

org.xml.sax.SAXException

javax.xml.parsers.ParserConfigurationException

doTransform

public void doTransform(java.io.File riflFilename,
                        java.io.File source,
                        java.io.File savePath)
                 throws java.io.IOException,
                        org.xml.sax.SAXException,
                        ParserException,
                        javax.xml.parsers.ParserConfigurationException

Throws:

java.io.IOException

org.xml.sax.SAXException

ParserException

javax.xml.parsers.ParserConfigurationException

writeProblemFile

private void writeProblemFile(java.io.File problemFileName,
                              java.lang.String newJavaFolder,
                              java.lang.String poname)

ensureTargetDirExists

private void ensureTargetDirExists(java.io.File target)
                            throws java.io.IOException

Throws:

java.io.IOException

writeJavaFile

private void writeJavaFile(java.io.File target,
                           CompilationUnit cu)
                    throws java.io.IOException

Writes a single Java file.

Throws:

java.io.IOException

getProblemFiles

public java.util.List<java.io.File> getProblemFiles()