org.checkerframework.common.wholeprograminference

Class SceneToStubWriter

java.lang.Object

org.checkerframework.common.wholeprograminference.SceneToStubWriter

public final class SceneToStubWriter
extends Object

SceneToStubWriter provides a static method that writes an AScene in stub file format to a file write(org.checkerframework.common.wholeprograminference.scenelib.ASceneWrapper, java.lang.String, org.checkerframework.common.basetype.BaseTypeChecker). This class is the equivalent of IndexFileWriter from the Annotation File Utilities, but outputs the results in the stub file format instead of jaif format. This class is not part of the Annotation File Utilities, a library for manipulating .jaif files, because it has nothing to do with .jaif files.

This class works by taking as input a scene-lib representation of a type augmented with additional information, stored in javac's format (e.g. as TypeMirrors or Elements). ASceneWrapper stores this additional information. This class walks the scene-lib representation structurally and outputs the stub file as a string, by combining the information scene-lib stores with the information gathered elsewhere.

The additional information is necessary because the scene-lib representation of a type does not have enough information to print full types.

This writer is used instead of IndexFileWriter if the -Ainfer=stubs command-line argument is present.

Method Summary

Modifier and Type	Method and Description
static String	formatAnnotation(scenelib.annotations.Annotation a) Returns the String representation of an annotation in Java source format.
static void	write(ASceneWrapper scene, String filename, BaseTypeChecker checker) Writes the annotations in scene to out in stub file format.

Methods inherited from class java.lang.Object

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

Method Detail

write

public static void write(ASceneWrapper scene,
                         String filename,
                         BaseTypeChecker checker)

Writes the annotations in scene to out in stub file format.

Parameters:

scene - the scene to write out

filename - the name of the file to write (must end with .astub)

checker - the checker, for computing preconditions and postconditions

formatAnnotation

public static String formatAnnotation(scenelib.annotations.Annotation a)

Returns the String representation of an annotation in Java source format.

Parameters:

a - the annotation to print

Returns:

the formatted annotation