Class SceneToStubWriter


public final class SceneToStubWriter extends Object
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 Details

    • write

      public static void write(ASceneWrapper scene, String filename, BaseTypeChecker checker)
      Writes the annotations in scene to out in stub file format.
      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(org.checkerframework.afu.scenelib.Annotation a)
      Returns the String representation of an annotation in Java source format.
      a - the annotation to print
      the formatted annotation
    • formatAnnotation

      public static void formatAnnotation(StringBuilder sb, org.checkerframework.afu.scenelib.Annotation a)
      Formats an annotation in Java source format.
      sb - where to format the annotation to
      a - the annotation to print