Class SceneToStubWriter
java.lang.Object
org.checkerframework.common.wholeprograminference.SceneToStubWriter
Static method
write(org.checkerframework.common.wholeprograminference.scenelib.ASceneWrapper, java.lang.String, org.checkerframework.common.basetype.BaseTypeChecker) writes an AScene to a file in stub file format. 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 TypeMethodDescriptionstatic voidformatAnnotation(StringBuilder sb, org.checkerframework.afu.scenelib.Annotation a) Formats an annotation in Java source format.static StringformatAnnotation(org.checkerframework.afu.scenelib.Annotation a) Returns the String representation of an annotation in Java source format.static voidwrite(ASceneWrapper scene, String filename, BaseTypeChecker checker) Writes the annotations inscenetooutin stub file format.
-
Method Details
-
write
Writes the annotations inscenetooutin stub file format.- Parameters:
scene- the scene to write outfilename- the name of the file to write (must end with .astub)checker- the checker, for computing preconditions and postconditions
-
formatAnnotation
Returns the String representation of an annotation in Java source format.- Parameters:
a- the annotation to print- Returns:
- the formatted annotation
-
formatAnnotation
public static void formatAnnotation(StringBuilder sb, org.checkerframework.afu.scenelib.Annotation a) Formats an annotation in Java source format.- Parameters:
sb- where to format the annotation toa- the annotation to print
-