org.checkerframework.common.wholeprograminference

Class WholeProgramInferenceScenesHelper

java.lang.Object

org.checkerframework.common.wholeprograminference.WholeProgramInferenceScenesHelper

public class WholeProgramInferenceScenesHelper
extends Object

This class stores annotations for fields, method return types, and method parameters.

The set of annotations inferred for a certain class is stored in an AScene, which writeScenesToJaif() can write into a .jaif file. For example, a class field of a class whose fully-qualified name is my.package.MyClass will have its inferred type stored in a Scene, and later written into a file named my.package.MyClass.jaif.

This class populates the initial Scenes by reading existing .jaif files on the jaifFilesPath directory. Having more information in those initial .jaif files means that the precision achieved by the whole-program inference analysis will be better. writeScenesToJaif() rewrites the initial .jaif files, and may create new ones.

Field Summary

Fields

Modifier and Type	Field and Description
static String	jaifFilesPath Directory where .jaif files will be written to and read from.

Constructor Summary

Constructors

Constructor and Description
WholeProgramInferenceScenesHelper(boolean ignoreNullAssignments)

Method Summary

Modifier and Type	Method and Description
protected annotations.el.AClass	getAClass(String className, String jaifPath) Returns the AClass in an AScene, given a className and a jaifPath.
protected String	getJaifPath(String className) Returns the String representing the .jaif path of a class given its name.
protected annotations.el.AScene	getScene(String jaifPath) Returns the Scene stored in a .jaif file path passed as input.
protected void	updateAnnotationSetInScene(annotations.el.ATypeElement type, AnnotatedTypeFactory atf, String jaifPath, AnnotatedTypeMirror rhsATM, AnnotatedTypeMirror lhsATM, TypeUseLocation defLoc) Updates the set of annotations in a location of a Scene.
void	writeScenesToJaif() Write all modified scenes into .jaif files.

Methods inherited from class java.lang.Object

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

Field Detail

jaifFilesPath

public static final String jaifFilesPath

Directory where .jaif files will be written to and read from. This directory is relative to where the CF's javac command is executed.

Constructor Detail

WholeProgramInferenceScenesHelper

public WholeProgramInferenceScenesHelper(boolean ignoreNullAssignments)

Method Detail

writeScenesToJaif

public void writeScenesToJaif()

Write all modified scenes into .jaif files. (Scenes are modified by the method updateAnnotationSetInScene(annotations.el.ATypeElement, org.checkerframework.framework.type.AnnotatedTypeFactory, java.lang.String, org.checkerframework.framework.type.AnnotatedTypeMirror, org.checkerframework.framework.type.AnnotatedTypeMirror, org.checkerframework.framework.qual.TypeUseLocation).)

getJaifPath

protected String getJaifPath(String className)

Returns the String representing the .jaif path of a class given its name.

getScene

protected annotations.el.AScene getScene(String jaifPath)

Returns the Scene stored in a .jaif file path passed as input. If the file does not exist, an empty Scene is created.

getAClass

protected annotations.el.AClass getAClass(String className,
                                          String jaifPath)

Returns the AClass in an AScene, given a className and a jaifPath.

updateAnnotationSetInScene

protected void updateAnnotationSetInScene(annotations.el.ATypeElement type,
                                          AnnotatedTypeFactory atf,
                                          String jaifPath,
                                          AnnotatedTypeMirror rhsATM,
                                          AnnotatedTypeMirror lhsATM,
                                          TypeUseLocation defLoc)

Updates the set of annotations in a location of a Scene.

• If there was no previous annotation for that location, then the updated set will be the annotations in newATM.
• If there was a previous annotation, the updated set will be the LUB between the previous annotation and newATM.

Parameters:

type - ATypeElement of the Scene which will be modified

atf - the annotated type factory of a given type system, whose type hierarchy will be used

jaifPath - used to identify a Scene

rhsATM - the RHS of the annotated type on the source code

lhsATM - the LHS of the annotated type on the source code

defLoc - the location where the annotation will be added