Commits

Colin Gordon committed ac72724 Merge

merge w/ latest CF changes

Comments (0)

Files changed (103)

build-common.properties

 checker.lib=${checker.loc}/dist/checker.jar
 checker.qual.lib=${checker.loc}/dist/checker-qual.jar
 
+checker.sources.lib=${checker.loc}/dist/checker-source.jar
+checker.javadoc.lib=${checker.loc}/dist/checker-javadoc.jar
+
 
 # How to find the error-prone compiler
 # TODO: currently you have to copy this .jar to ~/.ant/lib
     </target>
 
 
-    <target name="prep-ManualTaglet">
+    <target name="prep-ManualTaglet" depends="prep">
         <java fork="true"
               failonerror="true"
-              classpath="${javac.lib}:${javadoc.lib}:${java.home}/../lib/tools.jar"
+              classpath="${javac.lib}:${javadoc.lib}"
               classname="com.sun.tools.javac.Main">
             <jvmarg line="-Xbootclasspath/p:${javac.lib}:${javadoc.lib}"/>
             <arg value="-g"/>

checker/build.xml

         <delete file="jdk/jdk7.jar"/>
         <delete file="jdk/jdk8.jar"/>
         <delete file="jdk/jdk9.jar"/>
+
+        <delete dir="${dist}"/>
     </target>
 
     <target name="clean-nojdk" description="Remove generated files, but not the jdkX.jar files">
 
         <delete file="${checker.lib}"/>
         <delete file="${checker.qual.lib}"/>
+        <delete file="${checker.sources.lib}"/>
+        <delete file="${checker.javadoc.lib}"/>
+
         <delete failonerror="false">
             <fileset dir="${tests.build}" includes="**/*.class"/>
             <fileset dir="jdk" includes="**/*.class"/>
             <exclude name=""/>
         </fileset>
 
-        <fileset id="src.astub.files" dir="${src}" includes="**/*.properties,**/*.astub"/>
+        <fileset id="dataflow.src.astub.files" dir="${dataflow.loc}/${src}">
+            <include name="**/*.properties"/>
+            <include name="**/*.astub"/>
+        </fileset>
+
+        <fileset id="framework.src.astub.files" dir="${framework.loc}/${src}">
+            <include name="**/*.properties"/>
+            <include name="**/*.astub"/>
+        </fileset>
+
+        <fileset id="checker.src.astub.files" dir="${checker.loc}/${src}">
+            <include name="**/*.properties"/>
+            <include name="**/*.astub"/>
+        </fileset>
 
         <!-- I can't figure out how to combine filesets (or even selectors)
              to get just one *.uptodate property, so do them individually
         </uptodate>
 
         <uptodate property="src.astub.files.uptodate" targetfile="${build}">
-          <srcfiles refid="src.astub.files"/>
+          <srcfiles refid="dataflow.src.astub.files"/>
+          <srcfiles refid="framework.src.astub.files"/>
+          <srcfiles refid="checker.src.astub.files"/>
         </uptodate>
 
         <uptodate property="framework.lib.uptodate" targetfile="${build}" srcfile="${framework.lib}"/>
             description="Compile files.  Does not update any jars">
 
         <copy todir="${build}" preservelastmodified="true">
-            <fileset refid="src.astub.files"/>
+            <fileset refid="dataflow.src.astub.files"/>
+            <fileset refid="framework.src.astub.files"/>
+            <fileset refid="checker.src.astub.files"/>
         </copy>
 
         <pathconvert pathsep=" " property="src.files.spaceseparated">
                 <fileset dir="${src}">
                     <include name="**/*.java"/>
                 </fileset>
+                <!-- Recompile dependent projects with annotations-in-comments
+                     enabled, in order to get classes with qualified types. -->
+                <fileset dir="${javacutil.loc}/${src}">
+                    <include name="**/*.java"/>
+                <!-- Exclude ManualTaglet to not depend on javadoc. -->
+                    <exclude name="**/javacutil/dist/**"/>
+                </fileset>
+                <!-- Do not re-compile the stubparser, as it is not lint clean.
+                <fileset dir="${stubparser.loc}/${src}">
+                    <include name="**/*.java"/>
+                </fileset>
+                -->
+                <fileset dir="${dataflow.loc}/${src}">
+                    <include name="**/*.java"/>
+                </fileset>
+                <fileset dir="${framework.loc}/${src}">
+                    <include name="**/*.java"/>
+                </fileset>
             </path>
         </pathconvert>
 
     -->
     <target name="javadoc" depends="prep,prep-ManualTaglet,build.check.uptodate" description="Create Javadoc documentation">
 
-        <ant dir="${framework.loc}">
-            <target name="javadoc"/>
-        </ant>
-
         <!-- This relative path is wrong; running "ant -find" from a
         subdirectory fails. -->
         <javadoc sourcepath="${src}:${javacutil.loc}/${src}:${dataflow.loc}/${src}:${stubparser.loc}/${src}:${framework.loc}/${src}" destdir="${api.doc}"
                  failonerror="true"
                  executable="${javadoc.bin}"
-                 classpath="${build}:${framework.lib}:${javac.lib}:${javadoc.lib}:${java.home}/../lib/tools.jar:${junit.lib}"
+                 classpath="${build}:${javac.lib}:${javadoc.lib}:${junit.lib}"
                  excludepackagenames="org.checkerframework.framework.stub"
                  bootclasspath="${javac.lib}:${javadoc.lib}:${java.home}/lib/rt.jar">
+
             <package name="org.checkerframework.javacutil.*"/>
             <package name="org.checkerframework.dataflow.*"/>
-            <!-- TODO: should contain stubparser, but there
+            <!-- TODO: should contain stubparser, but there are
                  build errors with it!
             <package name="org.checkerframework.stubparser.*"/>
             -->
             <package name="org.checkerframework.framework.*"/>
+            <package name="org.checkerframework.common.*"/>
             <package name="org.checkerframework.checker.*"/>
 
             <link href="http://types.cs.washington.edu/checker-framework/api/jdk/"/>
             <link href="http://types.cs.washington.edu/checker-framework/api/javac/tree/"/>
             <taglet name="org.checkerframework.javacutil.dist.ManualTaglet"
-                    path="${javacutil.loc}/build"/>
+                    path="${build}:${javacutil.loc}/${build}:${javacutil.lib}"/>
         </javadoc>
     </target>
 
+    <target name="javadoc.jar" depends="javadoc" description="Create jar of all javadoc documentation">
+        <jar destfile="${checker.javadoc.lib}" basedir="${api.doc}"></jar>
+    </target>
+
+    <target name="sources.jar" description="Create a jar of all source files except those in the jdk directory.">
+        <jar destfile="${checker.sources.lib}">
+            <fileset dir=".."
+                includes="**/src/**"
+                excludes="**/jdk/**,**/dist/**,eclipse/**,maven-plugin/**,tutorial/**,checker/tests/**,framework/tests/**"/>
+        </jar>
+    </target>
+
     <!-- This creates checker.jar -->
     <target name="jar" depends="build,checker-qual-jar"
             description="Create checker.jar file">
         <delete dir="${build.reports}"/>
 
-        <unjar src="${framework.lib}" dest="${build}" />
+        <!-- Only unjar the stubparser - everything else is recompiled. -->
+        <unjar src="${stubparser.lib}" dest="${build}" />
 
         <jar destfile="${checker.lib}" basedir="${build}" excludes="polyall/,tests/,lubglb/,jtreg/">
             <manifest>
 
         <java fork="true"
               failonerror="true"
-              classpath="${javac.lib}:${junit.lib}:${build}:${framework.lib}"
+              classpath="${build}:${javac.lib}:${junit.lib}"
               classname="com.sun.tools.javac.Main">
             <jvmarg line="-Xbootclasspath/p:${javac.lib}"/>
             <arg value="-g"/>
                 <pathelement path="${build}"/>
                 <pathelement path="${tests.build}"/>
                 <pathelement path="${javac.lib}"/>
-                <pathelement path="${framework.lib}"/>
-                <pathelement path="${checker.lib}"/>
                 <pathelement path="${junit.lib}"/>
             </classpath>
 
     <target name="all-tests-nojar" depends="build-tests"
             description="Run tests for all checkers, WITHOUT building anything">
       <ant dir="${framework.loc}">
-          <target name="all-tests"/>
+          <target name="all-tests-nojar"/>
       </ant>
 
       <!-- TODO: for all -nojdk targets:
               <pathelement path="${build}"/>
               <pathelement path="${tests.build}"/>
               <pathelement path="${javac.lib}"/>
-              <pathelement path="${framework.lib}"/>
-              <pathelement path="${checker.lib}"/>
               <pathelement path="${junit.lib}"/>
           </classpath>
 
             <sequential>
                 <property name="coverage.options" value=""/>    <!-- default -->
                 <property name="coverage.classpath" value=""/>  <!-- default -->
-                <property name="checker.classpath" value="${javac.lib}:${javap.lib}:${framework.lib}:${checker.lib}"/>
+                <property name="checker.classpath" value="${build}:${javac.lib}:${javap.lib}:${checker.lib}"/>
                 <jtreg
                     dir="jtreg"
                     workDir="${build.jtreg.dir}/@{name}/work"
                     <include name="**/*.java"/>
                     <exclude name=""/>
                 </fileset>
+                <fileset dir="${javacutil.loc}/${src}">
+                    <include name="**/*.java"/>
+                    <!-- Exclude ManualTaglet to not depend on javadoc. -->
+                    <exclude name="**/javacutil/dist/**"/>
+                </fileset>
+
+                <fileset dir="${stubparser.loc}/${src}">
+                    <include name="**/*.java"/>
+                    <!-- Ignore the huge, auto-generated parser.
+                         TODO: might be a nice benchmark for performance optimization? -->
+                    <exclude name="**/AST*.java"/>
+                    <exclude name="**/Token.java"/>
+                </fileset>
+                <!-- Do not check dataflow, it doesn't have all purity
+                     annotations. TODO: should be easy to fix. Or solved
+                     once we inherit those annotations.
+                <fileset dir="${dataflow.loc}/${src}">
+                    <include name="**/*.java"/>
+                </fileset>
+                -->
+                <fileset dir="${framework.loc}/${src}">
+                    <include name="**/*.java"/>
+                </fileset>
             </path>
         </pathconvert>
 
         <echo message="${src.files}" file="${tmpdir}/srcfiles-checker.txt"/>
         <java fork="true"
               failonerror="true"
-              classpath="${javac.lib}:${framework.lib}:${checker.lib}:${junit.lib}"
+              classpath="${build}:${javac.lib}:${checker.lib}:${framework.lib}:${junit.lib}"
               classname="com.sun.tools.javac.Main">
             <jvmarg line="-Xbootclasspath/p:${javac.lib}"/>
             <arg value="-g"/>
             description="Run the compiler message keys checker on the Framework">
         <antcall target="-run-checker">
             <param name="checker-name" value="org.checkerframework.checker.compilermsgs.CompilerMessagesChecker"/>
-            <param name="checker-args" value="-Awarns -Apropfiles=./src/org/checkerframework/checker/lock/messages.properties:./src/org/checkerframework/checker/javari/messages.properties:./src/org/checkerframework/checker/interning/messages.properties:./src/org/checkerframework/checker/basetype/messages.properties:./src/org/checkerframework/checker/nullness/messages.properties:./src/org/checkerframework/checker/initialization/messages.properties:./src/org/checkerframework/checker/linear/messages.properties:./src/org/checkerframework/checker/regex/messages.properties:./src/org/checkerframework/checker/util/report/messages.properties:./src/org/checkerframework/checker/formatter/messages.properties:./src/org/checkerframework/checker/value/messages.properties:./src/org/checkerframework/checker/guieffects/messages.properties"/>
+            <param name="checker-args" value="-Awarns -Apropfiles=./src/org/checkerframework/checker/lock/messages.properties:./src/org/checkerframework/checker/javari/messages.properties:./src/org/checkerframework/checker/interning/messages.properties:${framework.loc}/src/org/checkerframework/common/basetype/messages.properties:./src/org/checkerframework/checker/nullness/messages.properties:./src/org/checkerframework/checker/initialization/messages.properties:./src/org/checkerframework/checker/linear/messages.properties:./src/org/checkerframework/checker/regex/messages.properties:${framework.loc}/src/org/checkerframework/common/util/report/messages.properties:./src/org/checkerframework/checker/formatter/messages.properties:${framework.loc}/src/org/checkerframework/common/value/messages.properties:./src/org/checkerframework/checker/guieffects/messages.properties"/>
         </antcall>
-        <!-- TODO: add framework .properties files -->
     </target>
 
     <target name="check-purity"
     </target>
 
 
+<target name="check-tutorial" description="Test to see if the tutorial is working as expected">
+<!--The tutorial build file is written relative to its location, 
+    so useNativeBasedir is required. -->
+      <ant dir="${framework.loc}/../tutorial/tests/" useNativeBasedir="true">
+          <target name="check-tutorial"/>
+      </ant>
+</target>
     <!-- TODO: like for -run-checker this only checks checker/src.
          Improve both. -->
     <!-- Depend on dist-nojdk to make sure everything compiles. -->
         <javac failonerror="true"
                 includeantruntime="false"
                 bootclasspath="${javac.lib}:${java.home}/lib/rt.jar"
-                classpath="${javac.lib}:${framework.lib}:${checker.lib}:${junit.lib}"
+                classpath="${javac.lib}:${checker.lib}:${junit.lib}"
                 srcdir="${src}"
                 includes="**/*.java"
                 excludes="org/checkerframework/checker/nullness/NullnessUtils.java org/checkerframework/checker/regex/RegexUtils.java"
             <compilerarg value="org.checkerframework.common.util.debug.EmptyProcessor"/>
             -->
         </javac>
-        <delete file="${tmpdir}/srcfiles-checker.txt"/>
     </target>
 
 

checker/examples/units-extension/Demo.java

-import checkers.units.quals.*;
+import org.checkerframework.checker.units.qual.*;
 
 public class Demo {
     @Hz int frq;

checker/examples/units-extension/Frequency.java

 import java.lang.annotation.*;
 
+import org.checkerframework.checker.units.qual.UnknownUnits;
+import org.checkerframework.framework.qual.*;
 
 
 /**
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @TypeQualifier
-@SubtypeOf( { Unqualified.class } )
+@SubtypeOf( { UnknownUnits.class } )
 public @interface Frequency {}

checker/examples/units-extension/FrequencyRelations.java

 import javax.annotation.processing.ProcessingEnvironment;
 import javax.lang.model.element.AnnotationMirror;
 
-import checkers.types.AnnotatedTypeMirror;
-import checkers.util.AnnotationUtils;
-import checkers.util.AnnotationBuilder;
-
-import checkers.units.*;
+import org.checkerframework.checker.units.UnitsRelations;
+import org.checkerframework.checker.units.qual.*;
+import org.checkerframework.framework.type.AnnotatedTypeMirror;
+import org.checkerframework.framework.util.AnnotationBuilder;
 
 /** Relations among units of frequency. */
 public class FrequencyRelations implements UnitsRelations {
 
     public UnitsRelations init(ProcessingEnvironment env) {
         AnnotationBuilder builder = new AnnotationBuilder(env, Hz.class);
-        builder.setValue("value", checkers.units.quals.Prefix.one);
+        builder.setValue("value", Prefix.one);
         hz = builder.build();
 
-        builder = new AnnotationBuilder(env, checkers.units.quals.s.class);
-        builder.setValue("value", checkers.units.quals.Prefix.one);
+        builder = new AnnotationBuilder(env,  org.checkerframework.checker.units.qual.s.class);
+        builder.setValue("value", Prefix.one);
         s = builder.build();
 
         return this;

checker/examples/units-extension/Hz.java

 import java.lang.annotation.*;
 
+import org.checkerframework.checker.units.qual.Prefix;
+import org.checkerframework.checker.units.qual.UnitsRelations;
 import org.checkerframework.framework.qual.*;
 
 /**

checker/examples/units-extension/Makefile

-JAVAC?=../../checkers/bin/javac
+JAVAC?=../../bin/javac
 
 FILES=Frequency.java \
   FrequencyRelations.java \

checker/manual/advanced-features.tex

   positive error messages.  See Section~\ref{type-refinement}.
 
   % Type
-  % qualifier refinement is implemented by the \refclass{checker/flow}{Flow} class.
+  % qualifier refinement is implemented by the \refclass{framework/flow}{Flow} class.
 
 \end{enumerate}
 
 fully-qualified, like \code{"org.checkerframework.checker.nullness.qual.NonNull"}.
 The optional second argument indicates where the default
 applies.  If the second argument is omitted, the specified annotation is
-the default in all locations.  See the Javadoc of \refclass{checker/qual}{DefaultQualifier} for details.
+the default in all locations.  See the Javadoc of \refclass{framework/qual}{DefaultQualifier} for details.
 
 For example, using the Nullness type system (Chapter~\ref{nullness-checker}):
 
 \item \refqualclass{checker/nullness/qual}{RequiresNonNull}
 \item \refqualclass{checker/nullness/qual}{EnsuresNonNull}
 \item \refqualclass{checker/nullness/qual}{EnsuresNonNullIf}
-\item \refqualclass{checker/nullness/qual}{EnsuresNonNullIf}
 \end{itemize}
 
 The expression is a subset of legal Java expressions:

checker/manual/annotating-libraries.tex

 
 Section~\ref{stub-creating} describes how to create stub classes.
 Section~\ref{stub-using} describes how to use stub classes.
-These sections illustrate stub classes via the example of creating a \refqualclass{checker/interning/quals}{Interned}-annotated
+These sections illustrate stub classes via the example of creating a \refqualclass{checker/interning/qual}{Interned}-annotated
 version of \code{java.lang.String}.  You don't need to repeat these steps
 to handle \code{java.lang.String} for the Interning Checker,
 but you might do something similar for a different class and/or checker.
 \section{Using distributed annotated JDKs\label{skeleton-using}\label{skeleton}}
 
 The Checker Framework distribution contains two
-annotated JDKs at the paths \<checkers/bin/jdk6.jar> and
-\<checker/dist/jdk7.jar>.
+annotated JDKs at the paths \<checker/bin/jdk7.jar> and
+\<checker/dist/jdk8.jar>.
 The \<javac> that is distributed with the Checker Framework and the command
 \code{java -jar \$CHECKERFRAMEWORK/checker/dist/checker.jar} both use the appropriate jdk6.jar or jdk7.jar
 based on the version of Java used to run them.

checker/manual/checkers-webpage.html

 
 <ul>
   <li>
-    Download: <a href="current/checkers.zip">checkers.zip</a>
+    Download: <a href="current/checker-framework.zip">checker-framework.zip</a>
     version
     <!-- checker-framework-version -->1.7.5, 5 Mar 2014<!-- /checker-framework-version -->
     (includes source, platform-independent binary, tests, and documentation)<br/>
       </li>
 
       <li>
-	<a href="current/changelog-checkers.txt">Changelog</a>
+	<a href="current/changelog-checkerframework.txt">Changelog</a>
       </li>
 
       <li>

checker/manual/creating-a-checker.tex

   expressions, a qualifier should be treated as implicitly present even if a
   programmer did not explicitly write it.  For example, in the Nullness
   type system every literal
-  other than \<null> has a \refqualclass{checker/nullness/quals}{NonNull} type;
+  other than \<null> has a \refqualclass{checker/nullness/qual}{NonNull} type;
   examples of literals include \<"some string"> and \<java.util.Date.class>.
 
 \item{\ref{extending-visitor}}
 \item
   Additional rules that are specific to your particular checker.  For
   example, in the Nullness type system, only references with a
-  \refqualclass{checker/nullness/quals}{NonNull} type may be dereferenced.  You
+  \refqualclass{checker/nullness/qual}{NonNull} type may be dereferenced.  You
   write these additional rules yourself.
 \end{itemize}
 
 \end{Verbatim}
 
 \noindent
-Write the \refqualclass{checker/quals}{TypeQualifier} meta-annotation on the annotation definition
+Write the \refqualclass{framework/qual}{TypeQualifier} meta-annotation on the annotation definition
 to indicate that the annotation represents a type qualifier
 and should be processed by the checker.
 Also write a \<@\sunjavadoc{java/lang/annotation/Target.html}{Target}>
 meta-annotation to indicate where the annotation may be written.
 (An annotation that is written on an annotation
-definition, such as \refqualclass{checker/quals}{TypeQualifier}, is called a \emph{meta-annotation}.)
+definition, such as \refqualclass{framework/qual}{TypeQualifier}, is called a \emph{meta-annotation}.)
 
 % \noindent
 % The \<@TypeQualifier> meta-annotation
 
 The type hierarchy induced by the qualifiers can be defined either
 declaratively via meta-annotations (Section~\ref{declarative-hierarchy}), or procedurally through
-subclassing \refclass{checker/types}{QualifierHierarchy} or
-\refclass{checker/types}{TypeHierarchy} (Section~\ref{procedural-hierarchy}).
+subclassing \refclass{framework/type}{QualifierHierarchy} or
+\refclass{framework/type}{TypeHierarchy} (Section~\ref{procedural-hierarchy}).
 
 
 \subsection{Declaratively defining the qualifier and type hierarchy\label{declarative-hierarchy}}
 
 \begin{itemize}
 
-\item \refqualclass{checker/quals}{SubtypeOf} denotes that a qualifier is a subtype of
+\item \refqualclass{framework/qual}{SubtypeOf} denotes that a qualifier is a subtype of
   another qualifier or qualifiers, specified as an array of class
   literals.  For example, for any type $T$,
-  \refqualclass{checker/nullness/quals}{NonNull} $T$ is a subtype of \refqualclass{checker/nullness/quals}{Nullable} $T$:
+  \refqualclass{checker/nullness/qual}{NonNull} $T$ is a subtype of \refqualclass{checker/nullness/qual}{Nullable} $T$:
 
   \begin{Verbatim}
     @TypeQualifier
     public @interface NonNull { }
   \end{Verbatim}
 
-  % (The actual definition of \refclass{checker/nullness/quals}{NonNull} is slightly more complex.)
+  % (The actual definition of \refclass{checker/nullness/qual}{NonNull} is slightly more complex.)
 
 
   %% True, but a distraction.  Move to Javadoc?
   % (It would be more natural to use Java subtyping among the qualifier
   % annotations, but Java forbids annotations from subtyping one another.)
   %
-  \refqualclass{checker/quals}{SubtypeOf} accepts multiple annotation classes as an argument,
+  \refqualclass{framework/qual}{SubtypeOf} accepts multiple annotation classes as an argument,
   permitting the type hierarchy to be an arbitrary DAG\@.  For example,
-  in the IGJ type system (Section~\ref{igj-annotations}), \refqualclass{checker/igj/quals}{Mutable}
-  and \refqualclass{checker/igj/quals}{Immutable} induce two mutually exclusive subtypes of the
-  \refqualclass{checker/igj/quals}{ReadOnly} qualifier.
+  in the IGJ type system (Section~\ref{igj-annotations}), \refqualclass{checker/igj/qual}{Mutable}
+  and \refqualclass{checker/igj/qual}{Immutable} induce two mutually exclusive subtypes of the
+  \refqualclass{checker/igj/qual}{ReadOnly} qualifier.
 %TODO: In the IGJ hierarchy I didn't find a use of multiple supertypes. Like
 % this the previous paragraph is confusing, as it does not give a correct
 % example.
 
   All type qualifiers, except for polymorphic qualifiers (see below and
   also Section~\ref{qualifier-polymorphism}), need to be
-  properly annotated with \refclass{checker/quals}{SubtypeOf}.
+  properly annotated with \refclass{framework/qual}{SubtypeOf}.
 
   The top qualifier is annotated with
   \<@SubtypeOf( \{ \} )>.  The top qualifier is the qualifier that is
-  a supertype of all other qualifiers.  For example, \refqualclass{checker/nullness/quals}{Nullable}
+  a supertype of all other qualifiers.  For example, \refqualclass{checker/nullness/qual}{Nullable}
   is the top qualifier of the Nullness type system, hence is defined as:
 
   \begin{Verbatim}
     \{ \} )} annotation on the top qualifier is necessary.  For an example, see the
   \<Encrypted> type system of Section~\ref{encrypted-example}.
 
-\item \refqualclass{checker/quals}{PolymorphicQualifier} denotes that a qualifier is a
+\item \refqualclass{framework/qual}{PolymorphicQualifier} denotes that a qualifier is a
   polymorphic qualifier.  For example:
 
   \begin{Verbatim}
 
   For a description of polymorphic qualifiers, see
   Section~\ref{qualifier-polymorphism}.  A polymorphic qualifier needs
-  no \refqualclass{checker/quals}{SubtypeOf} meta-annotation and need not be
-  mentioned in any other \refqualclass{checker/quals}{SubtypeOf}
+  no \refqualclass{framework/qual}{SubtypeOf} meta-annotation and need not be
+  mentioned in any other \refqualclass{framework/qual}{SubtypeOf}
   meta-annotation.
 
 \end{itemize}
 
-\urldef{\isSubtypeURL}\url{api/checkers/util/GraphQualifierHierarchy.html#isSubtype-java.util.Collection-java.util.Collection-}
+\urldef{\isSubtypeURL}\url{api/org/checkerframework/framework/util/GraphQualifierHierarchy.html#isSubtype-java.util.Collection-java.util.Collection-}
 
 The declarative and procedural mechanisms for specifying the hierarchy can
-be used together.  In particular, when using the \refqualclass{checker/quals}{SubtypeOf}
+be used together.  In particular, when using the \refqualclass{framework/qual}{SubtypeOf}
 meta-annotation, further customizations may be
 performed procedurally (Section~\ref{procedural-hierarchy})
 by overriding the \ahref{\isSubtypeURL}{\code{isSubtype}} method in the checker class
 
 
 \subsection{Procedurally defining the qualifier and type hierarchy\label{procedural-hierarchy}}
-\urldef{\createQualifierHierarchyURL}\url{api/checkers/types/AnnotatedTypeFactory.html#createQualifierHierarchy--}
-\urldef{\createTypeHierarchyURL}\url{api/checkers/types/AnnotatedTypeFactory.html#createTypeHierarchy--}
+\urldef{\createQualifierHierarchyURL}\url{api/org/checkerframework/framework/type/AnnotatedTypeFactory.html#createQualifierHierarchy--}
+\urldef{\createTypeHierarchyURL}\url{api/org/checkerframework/framework/type/AnnotatedTypeFactory.html#createTypeHierarchy--}
 
 While the declarative syntax suffices for many cases, more complex
-type hierarchies can be expressed by overriding, in \refclass{checker/basetype}{BaseTypeVisitor},
+type hierarchies can be expressed by overriding, in \refclass{common/basetype}{BaseTypeVisitor},
 either \ahref{\createQualifierHierarchyURL}{\<createQualifierHierarchy>} or \ahref{\createTypeHierarchyURL}{\<createTypeHierarchy>} (typically
 only one of these needs to be overridden).
 For more details, see the Javadoc of those methods and of the classes
-\refclass{checker/types}{QualifierHierarchy} and \refclass{checker/types}{TypeHierarchy}.
+\refclass{framework/type}{QualifierHierarchy} and \refclass{framework/type}{TypeHierarchy}.
 
-The \refclass{checker/types}{QualifierHierarchy} class represents the qualifier hierarchy (not the
-type hierarchy), e.g., \refclass{checker/igj/quals}{Mutable}
-is a subtype of \refclass{checker/igj/quals}{ReadOnly}.  A type-system designer may subclass
-\refclass{checker/types}{QualifierHierarchy} to express customized qualifier
+The \refclass{framework/type}{QualifierHierarchy} class represents the qualifier hierarchy (not the
+type hierarchy), e.g., \refclass{checker/igj/qual}{Mutable}
+is a subtype of \refclass{checker/igj/qual}{ReadOnly}.  A type-system designer may subclass
+\refclass{framework/type}{QualifierHierarchy} to express customized qualifier
 relationships (e.g., relationships based on annotation
 arguments).
 
-The \refclass{checker/types}{TypeHierarchy} class represents the type hierarchy ---
+The \refclass{framework/type}{TypeHierarchy} class represents the type hierarchy ---
 that is, relationships between
 annotated types, rather than merely type qualifiers, e.g., \<@Mutable
-Date> is a subtype of \<@ReadOnly Date>.  The default \refclass{checker/types}{TypeHierarchy} uses
-\refclass{checker/types}{QualifierHierarchy} to determine all subtyping relationships.
-The default \refclass{checker/types}{TypeHierarchy} handles
+Date> is a subtype of \<@ReadOnly Date>.  The default \refclass{framework/type}{TypeHierarchy} uses
+\refclass{framework/type}{QualifierHierarchy} to determine all subtyping relationships.
+The default \refclass{framework/type}{TypeHierarchy} handles
 generic type arguments, array components, type variables, and
 wildcards in a similar manner to the Java standard subtype
 relationship but with taking qualifiers into consideration.  Some type
 
 % This paragraph is out of place.
 
-\urldef{\addAbsoluteDefaultURL}\url{api/checkers/util/QualifierDefaults.html#addAbsoluteDefault-javax.lang.model.element.AnnotationMirror-checkers.quals.DefaultLocation-}
+\urldef{\addAbsoluteDefaultURL}\url{api/org/checkerframework/framework/util/QualifierDefaults.html#addAbsoluteDefault-javax.lang.model.element.AnnotationMirror-org.checkerframework.framework.qual.DefaultLocation-}
 
 A type system designer may set a default annotation.  A user may override
 the default; see Section~\ref{defaults}.
 
 The type system designer may specify a default annotation declaratively,
-using the \refqualclass{checker/quals}{DefaultQualifierInHierarchy}
+using the \refqualclass{framework/qual}{DefaultQualifierInHierarchy}
 meta-annotation.
 Note that the default will apply to any source code that the checker reads,
 including stub libraries, but will not apply to compiled \code{.class}
 \end{Verbatim}
 
 You don't necessarily have to define a new bottom qualifier.  But, You can
-use \<checkers.quals.Bottom> if your type system does not already have an
+use \<org.checkerframework.framework.qual.Bottom> if your type system does not already have an
 appropriate bottom qualifier.
 
 If your type system has a special bottom type that is used \emph{only} for
 % \noindent
 % The interning type system of Section~\ref{interning-checker} also lacks a
 % top qualifier; there is no \<@Uninterned> qualifier that is a supertype of 
-% \refqualclass{checker/interning/quals}{Interned}.
+% \refqualclass{checker/interning/qual}{Interned}.
 
 \noindent
 It can be convenient to use \<@Unqualified> as the top type to avoid
 
 It is best if a type system as an explicit qualifier for every
 possible meaning.  For example,
-the Nullness type system has both \refqualclass{checker/nullness/quals}{Nullable} and
-\refqualclass{checker/nullness/quals}{NonNull}.  Because it has no built-in meaning
+the Nullness type system has both \refqualclass{checker/nullness/qual}{Nullable} and
+\refqualclass{checker/nullness/qual}{NonNull}.  Because it has no built-in meaning
 for unannotated types; a user may specify a default qualifier.  This
 greater flexibility for the user is usually preferable.
 
 The ability to omit the top qualifier is a convenience
 when writing a type system, because it reduces the number of qualifiers
 that must be defined; this is especially convenient when using the Subtyping
-Checker (Section~\ref{subtyping-checker}).
+Checker (Chapter~\ref{subtyping-checker}).
 % TODO: Examples of the following?
 More importantly, omitting the top qualifier restricts the user in ways
 that the type system designer may have intended.
 
 For some types and expressions, a qualifier should be treated as present
 even if a programmer did not explicitly write it.  For example, every
-literal (other than \<null>) has a \refqualclass{checker/nullness/quals}{NonNull} type.
+literal (other than \<null>) has a \refqualclass{checker/nullness/qual}{NonNull} type.
 
 The implicit annotations may be specified declaratively and/or procedurally.
 
 
 \subsection{Declaratively specifying implicit annotations\label{declarative-type-introduction}}
 
-The \refqualclass{checker/quals}{ImplicitFor} meta-annotation indicates implicit annotations.
-When written on a qualifier, \refclass{checker/quals}{ImplicitFor}
+The \refqualclass{framework/qual}{ImplicitFor} meta-annotation indicates implicit annotations.
+When written on a qualifier, \refclass{framework/qual}{ImplicitFor}
 specifies the trees (AST nodes) and types for which the framework should
 automatically add that qualifier.
 
 In short, the types and trees can be
-specified via any combination of five fields in \refclass{checker/quals}{ImplicitFor}:
+specified via any combination of five fields in \refclass{framework/qual}{ImplicitFor}:
 
   \begin{itemize}
   \item \code{trees}: an array of
   \item \code{typeClasses}: an array of class literals for classes
     implementing \code{javax.lang.model.type.TypeMirror}, e.g.,
     \code{javax.lang.model.type.PrimitiveType}.  Often you should use
-    a subclass of \refclass{checker/types}{AnnotatedTypeMirror}.
+    a subclass of \refclass{framework/type}{AnnotatedTypeMirror}.
   \item \code{stringPatterns}: an array of regular expressions that will
     be matched against
     string literals, e.g., \code{"[01]+"} for a binary number.  Useful
     for annotations that indicate the format of a string.
   \end{itemize}
 
-For example, consider the definitions of the \refqualclass{checker/nullness/quals}{NonNull} and \refqualclass{checker/nullness/quals}{Nullable}
+For example, consider the definitions of the \refqualclass{checker/nullness/qual}{NonNull} and \refqualclass{checker/nullness/qual}{Nullable}
 type qualifiers:
 
 %BEGIN LATEX
 \end{smaller}
 %END LATEX
 
-For more details, see the Javadoc for the \refclass{checker/quals}{ImplicitFor}
+For more details, see the Javadoc for the \refclass{framework/qual}{ImplicitFor}
   annotation, and the Javadoc for the javac classes that are linked from
 it.  You only need to understand a small amount about the javac AST, such
 as the
 
 
 The Checker Framework provides a representation of annotated types,
-\refclass{checker/types}{AnnotatedTypeMirror}, that extends the standard \<TypeMirror>
+\refclass{framework/type}{AnnotatedTypeMirror}, that extends the standard \<TypeMirror>
 interface but integrates a representation of the annotations into a
 type representation.  A checker's \emph{type factory} class, given an AST
 node, returns the annotated type of that expression.  The Checker
 Framework's abstract
-\emph{base type factory} class, \refclass{checker/types}{AnnotatedTypeFactory},
+\emph{base type factory} class, \refclass{framework/type}{AnnotatedTypeFactory},
 supplies a uniform, Tree-API-based interface
 for querying the annotations on a program element, regardless of
 whether that element is declared in a source file or in a class file.
 It also handles default annotations, and it optionally performs
 flow-sensitive local type inference.
 
-\refclass{checker/types}{AnnotatedTypeFactory} inserts the qualifiers that the programmer
+\refclass{framework/type}{AnnotatedTypeFactory} inserts the qualifiers that the programmer
 explicitly inserted in the code.  Yet, certain constructs should be
 treated as having a type qualifier even when the programmer has not
 written one.  The type system designer may subclass
-\refclass{checker/types}{AnnotatedTypeFactory} and override
+\refclass{framework/type}{AnnotatedTypeFactory} and override
 \code{annotateImplicit(Tree,AnnotatedTypeMirror)} and
 \code{annotateImplicit(Element,AnnotatedTypeMirror)} to account for
 such constructs.
 in Section~\ref{type-refinement}.
 
 Class
-\refclass{checker/basetype}{BaseAnnotatedTypeFactory}
+\refclass{common/basetype}{BaseAnnotatedTypeFactory}
 provides a 2 parameter constructor that allows subclasses to disable
 flow inference.
 By default the 1 parameter constructor performs flow inference.
 To disable flow inference, call
 \code{super(checker, root, false);}
 in your subtype of
-\refclass{checker/basetype}{BaseAnnotatedTypeFactory}.
+\refclass{common/basetype}{BaseAnnotatedTypeFactory}.
 
 
 \section{Visitor: Type rules\label{extending-visitor}}
 These rules must be defined procedurally, not declaratively.
 
 The Checker Framework provides a \textit{base visitor class},
-\refclass{checker/basetype}{BaseTypeVisitor}, that performs type-checking at each node of a
+\refclass{common/basetype}{BaseTypeVisitor}, that performs type-checking at each node of a
 source file's AST\@.  It uses the visitor design pattern to traverse
 Java syntax trees as provided by Oracle's
 \ahref{\url{http://types.cs.washington.edu/checker-framework/jdk-api/javac/index.html}}{Tree
 
 A checker's visitor overrides one method in the base visitor for each special
 rule in the type qualifier system.  Most type-checkers
-override only a few methods in \refclass{checker/basetype}{BaseTypeVisitor}.  For example, the
+override only a few methods in \refclass{common/basetype}{BaseTypeVisitor}.  For example, the
 visitor for the Nullness type system of Chapter~\ref{nullness-checker}
 contains a single 4-line method that warns if an expression of nullable type
 is dereferenced, as in:
 
 
 
-By default, \refclass{checker/basetype}{BaseTypeVisitor} performs subtyping checks that are
+By default, \refclass{common/basetype}{BaseTypeVisitor} performs subtyping checks that are
 similar to Java subtype rules, but taking the type qualifiers into account.
-\refclass{checker/basetype}{BaseTypeVisitor} issues these errors:
+\refclass{common/basetype}{BaseTypeVisitor} issues these errors:
 
 \begin{itemize}
 
 
 \section{The checker class:  Compiler interface\label{writing-compiler-interface}}
 
-A checker's entry point is a subclass of \refclass{checker/basetype}{BaseTypeChecker}.  This entry
+A checker's entry point is a subclass of \refclass{common/basetype}{BaseTypeChecker}.  This entry
 point, which we call the checker class, serves two
 roles:  an interface to the compiler and a factory for constructing
 type-system classes.
 \end{Verbatim}
 
 
-\urldef{\getSupportedTypeQualifiersURL}{\url}{http://types.cs.washington.edu/checker-framework/current/api/checkers/types/AnnotatedTypeFactory.html#getSupportedTypeQualifiers--}
+\urldef{\getSupportedTypeQualifiersURL}{\url}{http://types.cs.washington.edu/dev/checker-framework/api/org/checkerframework/framework/type/AnnotatedTypeFactory.html#getSupportedTypeQualifiers--}
 
 The checker class must be annotated by
-\refqualclass{checker/quals}{TypeQualifiers}, which lists the annotations
+\refqualclass{framework/qual}{TypeQualifiers}, which lists the annotations
 that make up the type hierarchy for this checker (including
 polymorphic qualifiers), provided as an array of class literals.  Each
 one is a type qualifier whose definition bears the
-\refqualclass{checker/quals}{TypeQualifier} meta-annotation (or is
+\refqualclass{framework/qual}{TypeQualifier} meta-annotation (or is
 returned by the
 \ahref{\getSupportedTypeQualifiersURL}{\<BaseTypeChecker\-.getSupportedTypeQualifiers>}
 method).
 
-\urldef{\reportURL}{\url}{http://types.cs.washington.edu/checker-framework/current/api/checkers/source/SourceChecker.html#report-checkers.source.Result-java.lang.Object-}
+\urldef{\reportURL}{\url}{http://types.cs.washington.edu/dev/checker-framework/api/org/checkerframework/framework/source/SourceChecker.html#report-org.checkerframework.framework.source.Result-java.lang.Object-}
 
 The checker class bridges between the compiler and the rest of the checker.  It
 invokes the type-rule check visitor on every Java source file being
 a type system named Foo, the compiler
 interface (checker), the visitor, and the annotated type factory are
 named as \<FooChecker>, \<FooVisitor>, and \<FooAnnotatedTypeFactory>.
-\refclass{checker/basetype}{BaseTypeChecker} uses the convention to
+\refclass{common/basetype}{BaseTypeChecker} uses the convention to
 reflectively construct the components.  Otherwise, the checker writer
 must specify the component classes for construction.
 
 
 \item
 You can define an aggregate checker class that combines
-multiple checkers.  Extend \refclass{checker/source}{AggregateChecker} and override
+multiple checkers.  Extend \refclass{framework/source}{AggregateChecker} and override
 the \<getSupportedTypeCheckers> method, like the following:
 
 \begin{Verbatim}
 \item \code{-Afilenames}: print the name of each file before type-checking it.
 
 \item \code{-Ashowchecks}: print debugging information for each
-pseudo-assignment check (as performed by \refclass{checker/basetype}{BaseTypeVisitor}; see Section
+pseudo-assignment check (as performed by \refclass{common/basetype}{BaseTypeVisitor}; see Section
 \ref{extending-visitor}.
 
 \end{itemize}
 
 [InterningChecker] InterningExampleWithWarnings.java
  success (line  18): STRING_LITERAL "foo"
-     actual: DECLARED @checkers.interning.quals.Interned java.lang.String
-   expected: DECLARED @checkers.interning.quals.Interned java.lang.String
+     actual: DECLARED @org.checkerframework.checker.interning.qual.Interned java.lang.String
+   expected: DECLARED @org.checkerframework.checker.interning.qual.Interned java.lang.String
  success (line  19): NEW_CLASS new String("bar")
      actual: DECLARED java.lang.String
    expected: DECLARED java.lang.String
     if (foo == bar)
             ^
  success (line  22): STRING_LITERAL "foo == bar"
-     actual: DECLARED @checkers.interning.quals.Interned java.lang.String
+     actual: DECLARED @org.checkerframework.checker.interning.qual.Interned java.lang.String
    expected: DECLARED java.lang.String
 1 error
 \end{Verbatim}
 
 
 
+%%% Rather out of date!
 %% Not relevant to most readers.  Can go in a README file in our repository.
 % \section{Putting your checker in the repository\label{writing-repository}}
 %
 
 \code{TypeMirror} does not represent annotated types though.  A checker
 should use the Checker Framework types API,
-\refclass{checker/types}{AnnotatedTypeMirror}, instead.  \code{AnnotatedTypeMirror}
+\refclass{framework/type}{AnnotatedTypeMirror}, instead.  \code{AnnotatedTypeMirror}
 parallels the \code{TypeMirror} API, but also present the type annotations
 associated with the type.
 
 for a method invocation, and \code{ForEachTree} for an enhanced-for-loop
 statement.
 
-You should limit your use of trees. A checkers uses Trees mainly to
+You should limit your use of trees. A checker uses Trees mainly to
 traverse the source code and retrieve the types/elements corresponding to
 them.  Then, the checker performs any needed checks on the types/elements instead.
 
 \emph{Visitors and Scanners}:
 The compiler and the Checker Framework use the visitor pattern
 extensively. For example, visitors are used to traverse the source tree
-(\refclass{checker/basetype}{BaseTypeVisitor} extends
+(\refclass{common/basetype}{BaseTypeVisitor} extends
 \refTreeclass{util}{TreePathScanner}) and for type
-checking (\refclass{checker/types}{TreeAnnotator} implements
+checking (\refclass{framework/type}{TreeAnnotator} implements
 \refTreeclass{tree}{TreeVisitor}).
 
 \emph{Utility classes}:
 \refTreeclass{util}{Trees}).  The Checker Framework uses a common
 \code{Utils} suffix instead (e.g., \refclass{javacutil}{TypesUtils},
 \refclass{javacutil}{TreeUtils}, \refclass{javacutil}{ElementUtils}), with one
-notable exception: \refclass{checker/util}{AnnotatedTypes}.
+notable exception: \refclass{framework/util}{AnnotatedTypes}.
 
 
 \subsection{How a checker fits in the compiler as an annotation processor}

checker/manual/dataflow-manual/content.tex

 division possibly throw a DivideByZero exception?
 \end{workinprogress}
 
-    \begin{verbatim}class dataflow.cfg.node.*Node\end{verbatim}
+    \begin{verbatim}class org.checkerframework.dataflow.cfg.node.*Node\end{verbatim}
 
 
 \subsubsection{Blocks}
 classes.  The hierarchy is composed of five interfaces, two abstract
 classes, and four concrete classes.
 
-    \begin{verbatim}interface dataflow.cfg.block.Block\end{verbatim}
+    \begin{verbatim}interface org.checkerframework.dataflow.cfg.block.Block\end{verbatim}
 
-    \begin{verbatim}abstract class dataflow.cfg.block.BlockImpl implements Block\end{verbatim}
+    \begin{verbatim}abstract class org.checkerframework.dataflow.cfg.block.BlockImpl implements Block\end{verbatim}
 
-    \begin{verbatim}interface dataflow.cfg.block.SingleSuccessorBlock extends Block\end{verbatim}
+    \begin{verbatim}interface org.checkerframework.dataflow.cfg.block.SingleSuccessorBlock extends Block\end{verbatim}
 
-    \begin{verbatim}abstract class dataflow.cfg.block.SingleSuccessorBlockImpl extends BlockImpl implements
+    \begin{verbatim}abstract class org.checkerframework.dataflow.cfg.block.SingleSuccessorBlockImpl extends BlockImpl implements
         SingleSuccessorBlock\end{verbatim}
 
 A RegularBlock contains no exception-raising operations and has a
 single control-flow successor.
 
-    \begin{verbatim}interface dataflow.cfg.block.RegularBlock extends SingleSuccessorBlock\end{verbatim}
+    \begin{verbatim}interface org.checkerframework.dataflow.cfg.block.RegularBlock extends SingleSuccessorBlock\end{verbatim}
 
-    \begin{verbatim}class dataflow.cfg.block.RegularBlockImpl extends SingleSuccessorBlockImpl implements
+    \begin{verbatim}class org.checkerframework.dataflow.cfg.block.RegularBlockImpl extends SingleSuccessorBlockImpl implements
         RegularBlock\end{verbatim}
 
 An ExceptionBlock contains a single operation that may raise an
 exception, with one or more exceptional successors and a single normal
 control-flow successor.
 
-    \begin{verbatim}interface dataflow.cfg.block.ExceptionBlock extends SingleSuccessorBlock\end{verbatim}
+    \begin{verbatim}interface org.checkerframework.dataflow.cfg.block.ExceptionBlock extends SingleSuccessorBlock\end{verbatim}
 
-    \begin{verbatim}class dataflow.cfg.block.ExceptionBlockImpl extends SingleSuccessorBlockImpl implements
+    \begin{verbatim}class org.checkerframework.dataflow.cfg.block.ExceptionBlockImpl extends SingleSuccessorBlockImpl implements
         ExceptionBlock\end{verbatim}
 
 A SpecialBlock represents method entry or exit, including exceptional
 exit which is represented separately from normal exit.
 
-    \begin{verbatim}interface dataflow.cfg.block.SpecialBlock extends SingleSuccessorBlock\end{verbatim}
+    \begin{verbatim}interface org.checkerframework.dataflow.cfg.block.SpecialBlock extends SingleSuccessorBlock\end{verbatim}
 
-    \begin{verbatim}class dataflow.cfg.block.SpecialBlockImpl extends SingleSuccessorBlockImpl implements
+    \begin{verbatim}class org.checkerframework.dataflow.cfg.block.SpecialBlockImpl extends SingleSuccessorBlockImpl implements
         SpecialBlock\end{verbatim}
 
 A ConditionalBlock contains no operations at all.  It represents a
 control-flow split to either a `then' or an `else' successor based on
 the immediately preceding boolean-valued Node.
 
-    \begin{verbatim}interface dataflow.cfg.block.ConditionalBlock extends Block\end{verbatim}
+    \begin{verbatim}interface org.checkerframework.dataflow.cfg.block.ConditionalBlock extends Block\end{verbatim}
 
-    \begin{verbatim}class dataflow.cfg.block.ConditionalBlockImpl extends BlockImpl implements ConditionalBlock\end{verbatim}
+    \begin{verbatim}class org.checkerframework.dataflow.cfg.block.ConditionalBlockImpl extends BlockImpl implements ConditionalBlock\end{verbatim}
 
 
 
 exceptional exit SpecialBlocks.  ControlFlowGraphs are produced by the
 CFGBuilder classes and are treated as immutable once they are built.
 
-    \begin{verbatim}class dataflow.cfg.ControlFlowGraph\end{verbatim}
+    \begin{verbatim}class org.checkerframework.dataflow.cfg.ControlFlowGraph\end{verbatim}
 
 \subsubsubsection{CFGBuilder}
 \label{sec:cfg_builder_classes}
 The CFGBuilder classes visit an AST and produce a corresponding
 ControlFlowGraph as described in \autoref{sec:ast_to_cfg_translation}.
 
-    \begin{verbatim}class dataflow.cfg.CFGBuilder\end{verbatim}
+    \begin{verbatim}class org.checkerframework.dataflow.cfg.CFGBuilder\end{verbatim}
 
 The Checker Framework derives from CFGBuilder in order to desugar
 enhanced for loops that make explicit use of type annotations provided
 by the checker in use.
 
-    \begin{verbatim}class checkers.flow.CFCFGBuilder extends CFGBuilder\end{verbatim}
+    \begin{verbatim}class org.checkerframework.framework.flow.CFCFGBuilder extends CFGBuilder\end{verbatim}
 
 
 \subsubsection{FlowExpressions}
 array accesses, references to \code{this}, and pure method calls.
 FlowExpressions are keys in the store of abstract values.
 
-    \begin{verbatim}class dataflow.analysis.FlowExpressions\end{verbatim}
+    \begin{verbatim}class org.checkerframework.dataflow.analysis.FlowExpressions\end{verbatim}
 
 Java expressions that appear in method pre- and postconditions are
 parsed into FlowExpressions using helper routines in
-\code{checkers.util.FlowExpressionParseUtil}.
+\code{org.checkerframework.framework.util.FlowExpressionParseUtil}.
 
 
 \subsubsection{AbstractValue}
 share a common feature that one can compute the least upper bound of
 two AbstractValues.
 
-    \begin{verbatim}interface dataflow.analysis.AbstractValue<V extends AbstractValue<V>>\end{verbatim}
+    \begin{verbatim}interface org.checkerframework.dataflow.analysis.AbstractValue<V extends AbstractValue<V>>\end{verbatim}
 
 For the Checker Framework, abstract values are essentially
 AnnotatedTypeMirrors.
 
-    \begin{verbatim}abstract class checkers.flow.CFAbstractValue<V extends CFAbstractValue<V>> implements AbstractValue<V>\end{verbatim}
+    \begin{verbatim}abstract class org.checkerframework.framework.flow.CFAbstractValue<V extends CFAbstractValue<V>> implements AbstractValue<V>\end{verbatim}
 
-    \begin{verbatim}class checkers.flow.CFValue extends CFAbstractValue<CFValue>\end{verbatim}
+    \begin{verbatim}class org.checkerframework.framework.flow.CFValue extends CFAbstractValue<CFValue>\end{verbatim}
 
 For the NullnessCheckers, abstract values additionally track the
 meaning of PolyNull, which may be either Nullable or NonNull.  The
 NullnessChecker tracks the meaning of its poly qualifier using the
 dataflow analysis.
 
-        \begin{verbatim}class checkers.nullness.NullnessValue extends CFAbstractValue<NullnessValue>\end{verbatim}
+        \begin{verbatim}class org.checkerframework.checker.nullness.NullnessValue extends CFAbstractValue<NullnessValue>\end{verbatim}
 
 
 \subsubsection{Store}
 mapping from FlowExpressions to AbstractValues.  As with
 AbstractValues, one can take the least upper bound of two Stores.
 
-    \begin{verbatim}interface dataflow.analysis.Store<S extends Store<S>>\end{verbatim}
+    \begin{verbatim}interface org.checkerframework.dataflow.analysis.Store<S extends Store<S>>\end{verbatim}
 
 The Checker Framework store restricts the type of abstract values it
 may contain.
 
-    \begin{verbatim}abstract class checkers.flow.CFAbstractStore<V extends CFAbstractValue<V>,
+    \begin{verbatim}abstract class org.checkerframework.framework.flow.CFAbstractStore<V extends CFAbstractValue<V>,
         S extends CFAbstractStore<V, S>>
     implements Store<S>\end{verbatim}
 
-    \begin{verbatim}class checkers.flow.CFStore extends CFAbstractStore<CFValue, CFStore>\end{verbatim}
+    \begin{verbatim}class org.checkerframework.framework.flow.CFStore extends CFAbstractStore<CFValue, CFStore>\end{verbatim}
 
 An InitializationStore tracks which fields of the `self' reference
 have been initialized.
 
-    \begin{verbatim}class checkers.initialization.InitializationStore<
+    \begin{verbatim}class org.checkerframework.checker.initialization.InitializationStore<
         V extends CFAbstractValue<V>, S extends InitializationStore<V, S>>
     extends CFAbstractStore<V, S>\end{verbatim}
 
 A NullnessStore additionally tracks the meaning of PolyNull.
 
-    \begin{verbatim}class checkers.nullness.NullnessStore extends
+    \begin{verbatim}class org.checkerframework.checker.nullness.NullnessStore extends
         InitializationStore<NullnessValue, NullnessStore>\end{verbatim}
 
 
 contain a single store, or a pair of `then' and `else' stores when
 following a boolean-valued expression.
 
-    \begin{verbatim}class dataflow.analysis.TransferInput<
+    \begin{verbatim}class org.checkerframework.dataflow.analysis.TransferInput<
         A extends AbstractValue<A>,
         S extends Store<S>>\end{verbatim}
 
 store, while most other Nodes produce a RegularTransferResult with a
 single store.
 
-    \begin{verbatim}abstract class dataflow.analysis.TransferResult<
+    \begin{verbatim}abstract class org.checkerframework.dataflow.analysis.TransferResult<
         A extends AbstractValue<A>,
         S extends Store<S>>\end{verbatim}
 
-    \begin{verbatim}class dataflow.analysis.ConditionalTransferResult<
+    \begin{verbatim}class org.checkerframework.dataflow.analysis.ConditionalTransferResult<
         A extends AbstractValue<A>,
         S extends Store<S>>
     extends TransferResult<A, S>\end{verbatim}
 
-    \begin{verbatim}class dataflow.analysis.RegularTransferResult<
+    \begin{verbatim}class org.checkerframework.dataflow.analysis.RegularTransferResult<
         A extends AbstractValue<A>,
         S extends Store<S>>
     extends TransferResult<A, S>\end{verbatim}
 
 A TransferFunction is a NodeVisitor that takes an input and produces an output.
 
-    \begin{verbatim}interface dataflow.analysis.TransferFunction<
+    \begin{verbatim}interface org.checkerframework.dataflow.analysis.TransferFunction<
         A extends AbstractValue<A>,
         S extends Store<S>>
     extends NodeVisitor<TransferResult<A, S>, TransferInput<A, S>>\end{verbatim}
 of abstract values and it overrides many node visitor methods to
 refine the abstract values in their TransferResults.
 
-    \begin{verbatim}abstract class checkers.flow.CFAbstractTransfer<
+    \begin{verbatim}abstract class org.checkerframework.framework.flow.CFAbstractTransfer<
         V extends CFAbstractValue<V>,
         S extends CFAbstractStore<V, S>,
         T extends CFAbstractTransfer<V, S, T>>
     extends AbstractNodeVisitor<TransferResult<V, S>, TransferInput<V, S>>
     implements TransferFunction<V, S>\end{verbatim}
 
-    \begin{verbatim}class checkers.flow.CFTransfer
+    \begin{verbatim}class org.checkerframework.framework.flow.CFTransfer
         extends CFAbstractTransfer<CFValue, CFStore, CFTransfer>\end{verbatim}
 
 The Initialization Checker's transfer function tracks which fields of
 the `self' reference have been initialized.
 
-    \begin{verbatim}class checkers.initialization.InitializationTransfer<
+    \begin{verbatim}class org.checkerframework.checker.initialization.InitializationTransfer<
         V extends CFAbstractValue<V>,
         T extends InitializationTransfer<V, T, S>,
         S extends InitializationStore<V, S>>
 The Regex Checker's transfer function overrides visitMethodInvocation
 to special case isRegex and asRegex methods.
 
-    \begin{verbatim}class checkers.regex.RegexTransfer
+    \begin{verbatim}class org.checkerframework.checker.regex.RegexTransfer
        extends CFAbstractTransfer<CFValue, CFStore, RegexTransfer>\end{verbatim}
 
 
 graph using a given transfer function.  Currently only forward
 analyses are supported.
 
-    \begin{verbatim}class dataflow.analysis.Analysis<
+    \begin{verbatim}class org.checkerframework.dataflow.analysis.Analysis<
         A extends AbstractValue<A>,
         S extends Store<S>,
         T extends TransferFunction<A, S>>\end{verbatim}
 about the type hierarchy being analyzed and acts as a factory for
 abstract values, stores, and the transfer function.
 
-    \begin{verbatim}abstract class dataflow.analysis.CFAbstractAnalysis<
+    \begin{verbatim}abstract class org.checkerframework.dataflow.analysis.CFAbstractAnalysis<
         V extends CFAbstractValue<V>,
         S extends CFAbstractStore<V, S>,
         T extends CFAbstractTransfer<V, S, T>>
     extends Analysis<V, S, T>\end{verbatim}
 
-    \begin{verbatim}class checkers.flow.CFAnalysis
+    \begin{verbatim}class org.checkerframework.framework.flow.CFAnalysis
     extends CFAbstractAnalysis<CFValue, CFStore, CFTransfer>\end{verbatim}
 
 The Nullness Checkers' analysis overrides the factory methods for
 abstract values, stores, and the transfer function.
 
-    \begin{verbatim}class checkers.nullness.NullnessAnalysis
+    \begin{verbatim}class org.checkerframework.checker.nullness.NullnessAnalysis
     extends CFAbstractAnalysis<NullnessValue, NullnessStore, NullnessTransfer>\end{verbatim}
 
 The RegexChecker's analysis overrides the factory methods for abstract
 values, stores, and the transfer function.
 
-    \begin{verbatim}class checkers.regex.RegexAnalysis
+    \begin{verbatim}class org.checkerframework.checker.regex.RegexAnalysis
     extends CFAbstractAnalysis<CFValue, CFStore, RegexTransfer>\end{verbatim}
 
 
 transfer function to compute Stores that are valid immediately before
 or after any Tree.
 
-    \begin{verbatim}class dataflow.analysis.AnalysisResult<A extends AbstractValue<A>,
+    \begin{verbatim}class org.checkerframework.dataflow.analysis.AnalysisResult<A extends AbstractValue<A>,
                                        S extends Store<S>>\end{verbatim}
 
 
 but they are parameterized by the Dataflow Framework classes that they
 use.
 
-    \begin{verbatim}class checkers.types.AnnotatedTypeFactory
+    \begin{verbatim}class org.checkerframework.framework.type.AnnotatedTypeFactory
     implements AnnotationProvider\end{verbatim}
 
 In the Checker Framework, dataflow analysis is performed on demand,
 one class at a time, the first time that a ClassTree is passed to
 getAnnotatedType.  This is implemented in the abstract class
-AbstractBasicAnnotatedTypeFactory with concrete implementation in
-BasicAnnotatedTypeFactory.
+GenericAnnotatedTypeFactory with concrete implementation in
+BaseAnnotatedTypeFactory.
 
-    \begin{verbatim}abstract class checkers.types.AbstractBasicAnnotatedTypeFactory<
+    \begin{verbatim}abstract class org.checkerframework.framework.type.GenericAnnotatedTypeFactory<
         Checker extends BaseTypeChecker<?>,
         Value extends CFAbstractValue<Value>,
         Store extends CFAbstractStore<Value, Store>,
         FlowAnalysis extends CFAbstractAnalysis<Value, Store, TransferFunction>>
     extends AnnotatedTypeFactory\end{verbatim}
 
-    \begin{verbatim}class checkers.basetype.BaseAnnotatedTypeFactory
-    extends AbstractBasicAnnotatedTypeFactory<CFValue, CFStore, CFTransfer, CFAnalysis>\end{verbatim}
+    \begin{verbatim}class org.checkerframework.common.basetype.BaseAnnotatedTypeFactory
+    extends GenericAnnotatedTypeFactory<CFValue, CFStore, CFTransfer, CFAnalysis>\end{verbatim}
 
 
 
 The store is analysis-dependent, but the framework provides a default
 store implementation which can be reused.  The default implementation
 is
-\begin{verbatim}checkers.flow.CFStore\end{verbatim}
+\begin{verbatim}org.checkerframework.framework.flow.CFStore\end{verbatim}
 
 What information is tracked in the store depends on the analysis to be
  performed.  Some examples of stores include
 \begin{verbatim}
-checkers.initialization.InitializationStore
-checkers.nullness.NullnessStore
+org.checkerframework.checker.initialization.InitializationStore
+org.checkerframework.checker.nullness.NullnessStore
 \end{verbatim}
 
 Every store is associated with a particular point in the control-flow
 
 As a proof-of-concept, I (Stefan) implemented a constant propagation
 analysis for local variables and integer values.  The main class is
-\code{dataflow.cfg.playground.ConstantPropagationPlayground}.  I
+\code{org.checkerframework.dataflow.cfg.playground.ConstantPropagationPlayground}.  I
 describe the most important aspects here.
 
 \textbf{Abstract values.} A class \code{Constant} is used as an
 
 \subsection{Overview}
 
-The default flow-sensitive analysis \code{checkers.flow.CFAnalysis}
+The default flow-sensitive analysis \code{org.checkerframework.framework.flow.CFAnalysis}
 works for the qualifier hierarchy of any checker defined in the
 Checker Framework.  This generality is both a strength and a weakness
 because the default analysis can always run but the facts it can
 %  LocalWords:  CFAbstractAnalysis NullnessTransfer RegexChecker's lp 'c'
 %  LocalWords:  AnalysisResult AnnotatedTypeFactory AnnotatedTypeFactorys
 %  LocalWords:  AnnotationProvider getAnnotatedType BaseTypeChecker 414f
-%  LocalWords:  AbstractBasicAnnotatedTypeFactory FlowAnalysis CFAnalysis
+%  LocalWords:  GenericAnnotatedTypeFactory FlowAnalysis CFAnalysis
 %  LocalWords:  BaseAnnotatedTypeFactory CFGSimple ValueLiteral 1024L txt
 %  LocalWords:  BooleanLiteral CharacterLiteral DoubleLiteral FloatLiteral
 %  LocalWords:  IntegerLiteral LongLiteral NullLiteral ShortLiteral args

checker/manual/external-tools.tex

 
 \item
   Download the latest Checker Framework distribution
-  % (\ahrefurl{http://types.cs.washington.edu/checker-framework/current/checkers.zip})
+  % (\ahrefurl{http://types.cs.washington.edu/checker-framework/current/checker-framework.zip})
   and unzip it.  You can put it anywhere you like by changing the
   definition of environment variable \code{JSR308} below; a standard place
   is in a
   export JSR308=$HOME/jsr308
   mkdir -p ${JSR308}
   cd ${JSR308}
-  # or:  wget http://types.cs.washington.edu/checker-framework/current/checkers.zip
-  curl -O http://types.cs.washington.edu/checker-framework/current/checkers.zip
-  unzip checkers.zip
-  chmod +x checker-framework/checkers/bin/javac
-  checker-framework/checkers/bin/javac -version
+  # or:  wget http://types.cs.washington.edu/checker-framework/current/checker-framework.zip
+  curl -O http://types.cs.washington.edu/checker-framework/current/checker-framework.zip
+  unzip checker-framework.zip
+  chmod +x checker-framework/checker/bin/javac
+  checker-framework/checker/bin/javac -version
 \end{Verbatim}
 
 The output of the last command should be:
 
 \item
   Download the latest Checker Framework distribution
-  % (\ahrefurl{http://types.cs.washington.edu/checker-framework/current/checkers.zip})
+  % (\ahrefurl{http://types.cs.washington.edu/checker-framework/current/checker-framework.zip})
   and unzip it to create a \<checkers> directory.  You can put it anywhere
   you like; a standard place is in a new directory under \<C:\ttbs{}Program
   Files>.
 \begin{enumerate}
 \item
   Save the file
-  \ahrefurl{http://types.cs.washington.edu/checker-framework/current/checkers.zip}
+  \ahrefurl{http://types.cs.washington.edu/checker-framework/current/checker-framework.zip}
   to your Desktop.
 \item
-  Double-click the \<checkers.zip> file on your computer.  Click on
+  Double-click the \<checker-framework.zip> file on your computer.  Click on
   the \<checkers> directory, then Select \<Extract all files>, and use
   \<C:\ttbs{}Program Files> as the destination.  You will obtain a new
   \<C:\ttbs{}Program Files\ttbs{}checker-framework> folder.
         <!-- annotations from the Checker Framework: nullness, interning, locking, ... -->
         <dependency>
             <groupId>org.checkerframework</groupId>
-            <artifactId>checker-quals</artifactId>
+            <artifactId>checker-qual</artifactId>
             <version>\ReleaseVersion{}</version>
         </dependency>
 
     </excludes>
 \end{Verbatim}
 
-By default, an error reported by the Checker Framework Maven plugin will cause your build to fail.  To prevent
-a build from failing and still produce error and warning output, set \code{failOnError} to false.
+By default, an error reported by the Checker Framework Maven plugin will cause your build to fail.
+Maven also occasionally causes a build to fail when it encounters a message it does not recognize,
+even if that message is not an error or a warning. To prevent a build from failing and still produce
+error and warning output, set \code{failOnError} to false.
 
 \begin{Verbatim}
     <failOnError>false</failOnError>

checker/manual/faq.tex

 Each annotation that a programmer writes replaces a sentence or phrase of
 English descriptive text that would otherwise have been written in the
 Javadoc.  So, use of annotations actually reduces the overall size of the
-documentation, at the same time as making it less ambiguous and
-machine-processable.
+documentation, at the same time as making it machine-processable
+and less ambiguous.
 
 
 \subsection{Will using the Checker Framework slow down my program?  Will it slow down the compiler?\label{faq-slowdown}}
 
 \begin{enumerate}
 \item
-Annotate the field type as \refqualclass{checker/nullness/quals}{MonotonicNonNull}.
+Annotate the field type as \refqualclass{checker/nullness/qual}{MonotonicNonNull}.
 \item
-Annotate the method that sets the field as \refqualclass{checker/nullness/quals}{EnsuresNonNull}\<(">\emph{\<myFieldName>}\<")>.
+Annotate the method that sets the field as \refqualclass{checker/nullness/qual}{EnsuresNonNull}\<(">\emph{\<myFieldName>}\<")>.
 (If method \<m1> calls method \<m2>, which actually sets the field, then
 you would probably write this annotation on both \<m1> and \<m2>.)
 \item
 Annotate any method that depends on the field being non-null as
-\refqualclass{checker/nullness/quals}{RequiresNonNull}\<(">\emph{\<myFieldName>}\<")>.
+\refqualclass{checker/nullness/qual}{RequiresNonNull}\<(">\emph{\<myFieldName>}\<")>.
 The type-checker will verify that such a method is only called when the
 field isn't null --- that is, the method is only called after the setting
 method.

checker/manual/fenum-checker.tex

 file \code{\emph{MyFenum}.java}:
 
 \begin{alltt}
-package \textit{myproject}.quals;
+package \textit{myproject}.qual;
 
 import java.lang.annotation.*;
 import org.checkerframework.framework.qual.SubtypeOf;
 You only need to adapt the italicized package, annotation, and file names in the example.
 
 
-\item Use the provided \refqualclass{checker/fenum/quals}{Fenum} annotation, which takes a
+\item Use the provided \refqualclass{checker/fenum/qual}{Fenum} annotation, which takes a
 \code{String} argument to distinguish different fenums.
 For example, \code{@Fenum("A")} and \code{@Fenum("B")} are two distinct fenums.
 \end{enumerate}
 
 \begin{alltt}
   javac -processor org.checkerframework.checker.fenum.FenumChecker
-        \textit{-Aquals=myproject.quals.MyFenum} MyFile.java ...
+        \textit{-Aquals=myproject.qual.MyFenum} MyFile.java ...
 \end{alltt}
 
 
 \item
-If your code uses the \refqualclass{checker/fenum/quals}{Fenum} annotation, you do
+If your code uses the \refqualclass{checker/fenum/qual}{Fenum} annotation, you do
 not need the \code{-Aquals} option:
 
 \begin{Verbatim}

checker/manual/formatter-checker.tex

 % \sunjavadoc{java/io/PrintStream.html#printf(java.lang.String,java.lang.Object...)}{System.out.printf}.
 A format specifier is introduced by a \code{\%} character. For example,
 \code{String.format("The \%s is \%d.","answer",42)} yields
-\code{"The answer is 42."}.  \code{"\%s \%d"} is
+\code{"The answer is 42."}.  \code{"The \%s is \%d."} is
 the format string, \code{"\%s"} and \code{"\%d"} are the format specifiers;
-\code{"hello"} and \code{42} are format arguments.
+\code{"answer"} and \code{42} are format arguments.
 
 
 \section{Format String Checker annotations\label{formatter-annotations}}
 % for example, will fail despite the fact that \code{"\%d"} is valid.
 
 The \refqualclass{checker/formatter/qual}{Format} qualifier is parameterized with
-a list of conversion categories that impose restricts on the format arguments.
+a list of conversion categories that impose restrictions on the format arguments.
 Conversion categories are explained in more detail in
 Section~\ref{formatter-categories}.  The type qualifier for \code{"\%d \%f"} is
 for example \code{@Format(\{INT, FLOAT\})}.
 \refqualclass{checker/formatter/qual}{InvalidFormat} indicates an invalid format
 string --- that is, a string that cannot be used as a format string.  For
 example, the type of \code{"\%y"} is \<@InvalidFormat String>.
-\refqualclass{checker/formatter/quals}{FormatBottom} is the type of the
+\refqualclass{checker/formatter/qual}{FormatBottom} is the type of the
 \code{null} literal.
 \refqualclass{framework/qual}{Unqualified} is the default that is
 applied to strings that are not literals and on which the user has not
 obtained from an external resource, then the string must be trusted or tested.
 
 One way to test a string is to call the
-\refmethod{checker/formatter}{FormatUtil}{asFormat}{-java.lang.String-org.checkerframework.checker.formatter.quals.ConversionCategory...-}
+\refmethod{checker/formatter}{FormatUtil}{asFormat}{-java.lang.String-org.checkerframework.checker.formatter.qual.ConversionCategory...-}
 method to check whether the format string is valid and its format
 specifiers match certain conversion categories.
 If this is not the case, \<asFormat> raises an exception.  Your code should

checker/manual/generics.tex

 \noindent
 Then the following expressions would be legal, inside a given implementation.
 (Compilable source code appears as file
-\<checker-framework/checkers/tests/nullness/GenericsExample.java>.)
+\<checker-framework/checker/tests/nullness/generics/GenericsExample.java>.)
 
 \begin{tabular}{|l|c|c|c|c|} \hline
                         & MyList1 & MyList2 & MyList3 & MyList4 \\ \hline
 
 When a type parameter is used in a read-only way --- that is, when values
 of that type are read but are never assigned --- then it is safe for the
-type to be \emph{covariant} in the type parameter.  Use the \refqualclass{checker/nullness/quals}{Covariant} annotation to indicate
+type to be \emph{covariant} in the type parameter.  Use the \refqualclass{checker/nullness/qual}{Covariant} annotation to indicate
 this.
 When a type parameter is covariant, two instantiations of the class with
 different type arguments have the same subtyping relationship as the type
 Java's rule for resolving overloaded methods.
 
 To \emph{define} a polymorphic qualifier, mark the definition with
-\refqualclass{checker/quals}{PolymorphicQualifier}.  For example,
-\refqualclass{checker/nullness/quals}{PolyNull} is a polymorphic type
+\refqualclass{framework/qual}{PolymorphicQualifier}.  For example,
+\refqualclass{checker/nullness/qual}{PolyNull} is a polymorphic type
 qualifier for the Nullness type system:
 
 \begin{Verbatim}

checker/manual/igj-checker.tex

 
 \begin{description}
 
-\item[\refqualclass{checker/igj/quals}{Immutable}]
+\item[\refqualclass{checker/igj/qual}{Immutable}]
   An immutable reference always refers to an immutable object.  Neither the
   reference, nor any aliasing reference, may modify the object.
 
-\item[\refqualclass{checker/igj/quals}{Mutable}]
+\item[\refqualclass{checker/igj/qual}{Mutable}]
   A mutable reference refers to a mutable object.  The reference, or some
   aliasing mutable reference, may modify the object.
 
-\item[\refqualclass{checker/igj/quals}{ReadOnly}]
+\item[\refqualclass{checker/igj/qual}{ReadOnly}]
   A readonly reference cannot be used to modify its referent.  The referent
   may be an immutable or a mutable object.  In other words, it is possible
   for the referent to change via an aliasing mutable reference, even though
   the referent cannot be changed via the readonly reference.
 
-\item[\refqualclass{checker/igj/quals}{Assignable}]
+\item[\refqualclass{checker/igj/qual}{Assignable}]
   The annotated field may be re-assigned regardless of the
   immutability of the enclosing class or object instance.
 
-\item[\refqualclass{checker/igj/quals}{AssignsFields}]
+\item[\refqualclass{checker/igj/qual}{AssignsFields}]
   is similar to \<@Mutable>, but permits only limited mutation ---
   assignment of fields --- and is intended for use by constructor helper
   methods.  \<@AssignsFields> is assumed to be true of the result of a
   constructor, so it does not need to be written there.
 
-\item[\refqualclass{checker/igj/quals}{I}]
+\item[\refqualclass{checker/igj/qual}{I}]
   simulates mutability overloading or the template behavior of generics.
   It can be applied to classes, methods, and parameters.  See
   Section~\ref{igj-templating}.
 
 The IGJ Checker issues an error whenever mutation happens through a
 readonly reference, when fields of a readonly reference which are not
-explicitly marked with \refqualclass{checker/igj/quals}{Assignable} are
+explicitly marked with \refqualclass{checker/igj/qual}{Assignable} are
 reassigned, or when a readonly reference is assigned to a mutable
 variable.  The checker also emits a warning when casts increase the
 mutability access of a reference.
 not through a combination of generics and annotations.  Use of type
 annotations makes Annotation IGJ backward compatible with Java syntax.
 
-\item Templating over Immutability: The annotation \refqualclass{checker/igj/quals}{I}\<(>\emph{\<id>}\<)> is used to template
+\item Templating over Immutability: The annotation \refqualclass{checker/igj/qual}{I}\<(>\emph{\<id>}\<)> is used to template
 over immutability.  See Section~\ref{igj-templating}.
 
 \end{itemize}
 
 \subsection{Templating Over Immutability: \code{@I}\label{igj-templating}}
 
-\refqualclass{checker/igj/quals}{I} is a template annotation over IGJ Immutability annotations. It acts
+\refqualclass{checker/igj/qual}{I} is a template annotation over IGJ Immutability annotations. It acts
 similarly to type variables in Java's generic types, and the name
-\refqualclass{checker/igj/quals}{I} mimics the standard \code{<I>} type variable name used in code
+\refqualclass{checker/igj/qual}{I} mimics the standard \code{<I>} type variable name used in code
 written in the original IGJ dialect.  The annotation value string is used
-to distinguish between multiple instances of \refqualclass{checker/igj/quals}{I} --- in the
+to distinguish between multiple instances of \refqualclass{checker/igj/qual}{I} --- in the
 generics-based original dialect, these would be expressed as two type
 variables \code{<I>} and \code{<J>}.
 
 \paragraph{Usage on classes\label{igj-usage-on-classes}}
 
-A class declaration annotated with \refqualclass{checker/igj/quals}{I} can then be
+A class declaration annotated with \refqualclass{checker/igj/qual}{I} can then be
 used with any IGJ Immutability annotation.  The actual immutability that
-\refqualclass{checker/igj/quals}{I} is resolved to dictates the immutability type for all the non-static
-appearances of \refqualclass{checker/igj/quals}{I} with the same value as the class declaration.
+\refqualclass{checker/igj/qual}{I} is resolved to dictates the immutability type for all the non-static
+appearances of \refqualclass{checker/igj/qual}{I} with the same value as the class declaration.
 
   Example:
 \begin{Verbatim}
     }
 \end{Verbatim}
 
-In the last example, \refqualclass{checker/igj/quals}{I} was resolved to \refqualclass{checker/igj/quals}{Mutable} for the instance file.
+In the last example, \refqualclass{checker/igj/qual}{I} was resolved to \refqualclass{checker/igj/qual}{Mutable} for the instance file.
 
 \paragraph{Usage on methods\label{igj-usage-on-methods}}
 
 
 For example, the below method \code{getMidpoint} returns a \code{Point} with the same
 immutability type as the passed parameters if \code{p1} and \code{p2} match
-in immutability, otherwise \refqualclass{checker/igj/quals}{I} is resolved to \refqualclass{checker/igj/quals}{ReadOnly}:
+in immutability, otherwise \refqualclass{checker/igj/qual}{I} is resolved to \refqualclass{checker/igj/qual}{ReadOnly}:
 
 \begin{Verbatim}
   static @I Point getMidpoint(@I Point p1, @I Point p2) { ... }
 \end{Verbatim}
 
-The \refqualclass{checker/igj/quals}{I} annotation value distinguishes between \refqualclass{checker/igj/quals}{I}
+The \refqualclass{checker/igj/qual}{I} annotation value distinguishes between \refqualclass{checker/igj/qual}{I}
 declarations.  So, the below method \code{findUnion} returns a collection of the same
 immutability type as the \emph{first} collection parameter:
 

checker/manual/interning-checker.tex

 
 \begin{description}
 
-\item[\refqualclass{checker/interning/quals}{Interned}]
+\item[\refqualclass{checker/interning/qual}{Interned}]
   indicates a type that includes only interned values (no non-interned
   values).
 
-\item[\refqualclass{checker/interning/quals}{PolyInterned}]
+\item[\refqualclass{checker/interning/qual}{PolyInterned}]
   indicates qualifier polymorphism.  For a description of
-  \refqualclass{checker/interning/quals}{PolyInterned}, see
+  \refqualclass{checker/interning/qual}{PolyInterned}, see
   Section~\ref{qualifier-polymorphism}.
 
-\item[\refqualclass{checker/interning/quals}{UsesObjectEquals}]
+\item[\refqualclass{checker/interning/qual}{UsesObjectEquals}]
   is a class (not type) annotation that indicates that this class's
   \<equals> method is the same as that of \<Object>.  In other words,
   neither this class nor any of its superclasses overrides the \<equals>
 \label{fig-interning-hierarchy}
 \end{figure}
 
-In order to perform checking, you must annotate your code with the \refqualclass{checker/interning/quals}{Interned}
+In order to perform checking, you must annotate your code with the \refqualclass{checker/interning/qual}{Interned}
 type annotation, which indicates a type for the canonical representation of an
 object:
 
 appear in your code.
 For example, String literals and the null literal are always considered interned, and
 object creation expressions (using \code{new}) are never considered
-\refqualclass{checker/interning/quals}{Interned} unless they are annotated as such, as in
+\refqualclass{checker/interning/qual}{Interned} unless they are annotated as such, as in
 
 %BEGIN LATEX
 \begin{smaller}
 
 \section{What the Interning Checker checks\label{interning-checks}}
 
-Objects of an \refqualclass{checker/interning/quals}{Interned} type may be safely compared using the ``\code{==}''
+Objects of an \refqualclass{checker/interning/qual}{Interned} type may be safely compared using the ``\code{==}''
 operator.
 
 The checker issues an error in two cases:
 
 \item
   When a reference (in)equality operator (``\code{==}'' or ``\code{!=}'')
-  has an operand of non-\refqualclass{checker/interning/quals}{Interned} type.
+  has an operand of non-\refqualclass{checker/interning/qual}{Interned} type.
 
 \item
-  When a non-\refqualclass{checker/interning/quals}{Interned} type is used where an \refqualclass{checker/interning/quals}{Interned} type
+  When a non-\refqualclass{checker/interning/qual}{Interned} type is used where an \refqualclass{checker/interning/qual}{Interned} type
   is expected.
 
 \end{enumerate}
 This example shows both sorts of problems:
 
 \begin{Verbatim}
-            Object  obj;
-  @Interned Object iobj;
+            Date  date;
+  @Interned Date idate;
   ...
-  if (obj == iobj) { ... }  // error: reference equality test is unsafe
-  iobj = obj;               // error: iobj's referent may no longer be interned
+  if (date == idate) { ... }  // error: reference equality test is unsafe
+  idate = date;               // error: idate's referent may no longer be interned
 \end{Verbatim}
 
 \label{lint-dotequals}
 
 \section{Examples\label{interning-example}}
 
-To try the Interning Checker on a source file that uses the \refqualclass{checker/interning/quals}{Interned} qualifier,
+To try the Interning Checker on a source file that uses the \refqualclass{checker/interning/qual}{Interned} qualifier,
 use the following command (where \code{javac} is the JSR 308 compiler that
 is distributed with the Checker Framework):
 
 
 \noindent
 The compiler will issue an error regarding violation of the semantics of
-\refqualclass{checker/interning/quals}{Interned}.
+\refqualclass{checker/interning/qual}{Interned}.
 % in the \code{InterningExampleWithWarnings.java} file.
 
 
 The Daikon invariant detector
 (\myurl{http://plse.cs.washington.edu/daikon/}) is also annotated with
-\refqualclass{checker/interning/quals}{Interned}.  From directory \code{java},
+\refqualclass{checker/interning/qual}{Interned}.  From directory \code{java},
 run \code{make check-interning}.
 
 
 \end{tabular}
 &
 $\Rightarrow$
-~checkers.interning.quals.Interned~
+~org.checkerframework.checker.interning.qual.Interned~
 \end{tabular}
 \end{center}
 %BEGIN LATEX

checker/manual/introduction.tex

   %BEGIN LATEX
   \\
   %END LATEX
-  \ahrefurl{http://types.cs.washington.edu/checker-framework/current/checkers.zip}
+  \ahrefurl{http://types.cs.washington.edu/checker-framework/current/checker-framework.zip}
 \item 
   Unzip it to create a \code{checker-framework} directory.
 
 is not a concern, a code change may introduce bugs, whereas adding
 annotations does not change the run-time behavior.  It is possible to add
 annotations to existing code, including code you do not maintain or cannot
-change.  It is possible to annotate primitive types without converting them
+change (for code that strictly cannot be changed, it is recommended to add
+annotations in comments --- see Section~\ref{annotations-in-comments}).
+It is possible to annotate primitive types without converting them
 to wrappers, which would make the code both uglier and slower.
 
 Type qualifiers can be applied to any type, including final classes that

checker/manual/linear-checker.tex

 \section{Linear annotations\label{linear-annotations}}
 
 The linear type system uses one user-visible annotation:
-\refqualclass{checker/linear/quals}{Linear}.  The annotation indicates
+\refqualclass{checker/linear/qual}{Linear}.  The annotation indicates
 a type for which each value may only have a single reference ---
 equivalently, may only be used once on the right-hand side of an
 assignment.

checker/manual/lock-checker.tex

 
 \begin{description}
 
-\item[\refqualclass{checker/lock/quals}{GuardedBy}]
+\item[\refqualclass{checker/lock/qual}{GuardedBy}]
   indicates a type whose value may be accessed only when the given lock is
   held.
-  See the \ahref{api/checkers/lock/quals/GuardedBy.html}{GuardedBy
+  See the \ahref{api/org/checkerframework/checker/lock/qual/GuardedBy.html}{GuardedBy
     Javadoc} for an explanation of the argument and other details.  The lock
   acquisition and the value access may be arbitrarily far in the future;
   or, if the value is never accessed, the lock never need be held.
 \end{figure}
 
 
-\item[\refqualclass{checker/lock/quals}{Holding}]
+\item[\refqualclass{checker/lock/qual}{Holding}]
   is a method annotation (not a type qualifier).  It indicates that when
   the method is called, the given lock must be held by the caller.
   In other words, the given lock is already held at the time the method is
 \end{tabular}
 &
 $\Rightarrow$
-~checkers.lock.quals.GuardedBy~
+~org.checkerframework.checker.lock.qual.GuardedBy~
 \end{tabular}
 \end{center}
 %BEGIN LATEX
 \end{itemize}
 
 The Lock Checker renames the method annotation to
-\refqualclass{checker/lock/quals}{Holding}, and it generalizes the 
-\refqualclass{checker/lock/quals}{GuardedBy} annotation into a type qualifier
+\refqualclass{checker/lock/qual}{Holding}, and it generalizes the 
+\refqualclass{checker/lock/qual}{GuardedBy} annotation into a type qualifier
 that can apply not just to a field but to an arbitrary type (including the
 type of a parameter, return value, local variable, generic type parameter,
 etc.).  This makes the annotations more expressive and also more amenable

checker/manual/manual-style.tex

 \def\codesize{\relax}           % for "pslatex"
 %HEVEA \def\codesize{\relax}
 
-%BEGIN LATEX
-\DeclareRobustCommand{\code}[1]{\codesize{\path{#1}}}
-%END LATEX
-%HEVEA \newcommand{\code}[1]{\codesize{\texttt{#1}}}
+\newcommand{\code}[1]{\ifmmode{\mbox{\codesize\ttfamily{#1}}}\else{\codesize\ttfamily #1}\fi}
+%%BEGIN LATEX
+%\DeclareRobustCommand{\code}[1]{\codesize{\path{#1}}}
+%%END LATEX
+%%HEVEA \newcommand{\code}[1]{\codesize{\texttt{#1}}}
 
 % This can't handle a URL with an embedded "#" -- at least at UW CSE
 \newcommand{\myurl}[1]{{\codesize\url{#1}}}
 
 
 % Reference to Checker Framework Javadoc for a class (not a method, etc.).
-% Arg 1: directory under checkers/, including internal "/", but no leading
+% Arg 1: directory under checker/, including internal "/", but no leading