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 void
formatAnnotation
(StringBuilder sb, org.checkerframework.afu.scenelib.Annotation a) Formats an annotation in Java source format.static String
formatAnnotation
(org.checkerframework.afu.scenelib.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 inscene
toout
in stub file format.
-
Method Details
-
write
Writes the annotations inscene
toout
in 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
-