[pull] master from opprop:master

.ci-build-without-test.sh

@@ -13,18 +13,18 @@ else
   export JAVA_HOME=${JAVA_HOME:-$(dirname $(dirname $(readlink -f $(which javac))))}
 fi
 
-if [ -d "/tmp/plume-scripts" ] ; then
-  git -C /tmp/plume-scripts pull -q
+if [ -d "/tmp/git-scripts" ] ; then
+  git -C /tmp/git-scripts pull -q
 else
-  git -C /tmp clone --depth 1 -q https://github.com/plume-lib/plume-scripts.git
+  git -C /tmp clone --depth 1 -q https://github.com/eisop-plume-lib/git-scripts.git
 fi
 
 export AFU="${AFU:-../annotation-tools/annotation-file-utilities}"
 # Don't use `AT=${AFU}/..` which causes a git failure.
 AT=$(dirname "${AFU}")
 
 ## Build annotation-tools (Annotation File Utilities)
-/tmp/plume-scripts/git-clone-related opprop annotation-tools "${AT}"
+/tmp/git-scripts/git-clone-related opprop annotation-tools "${AT}"
 if [ ! -d ../annotation-tools ] ; then
  ln -s "${AT}" ../annotation-tools
 fi
@@ -39,10 +39,10 @@ export CHECKERFRAMEWORK="${CHECKERFRAMEWORK:-$(pwd -P)/../checker-framework}"
 export PATH=$AFU/scripts:$JAVA_HOME/bin:$PATH
 
 ## Build Checker Framework
-/tmp/plume-scripts/git-clone-related opprop checker-framework ${CHECKERFRAMEWORK}
+/tmp/git-scripts/git-clone-related opprop checker-framework ${CHECKERFRAMEWORK}
 
 # This also builds annotation-tools
-(cd $CHECKERFRAMEWORK && checker/bin-devel/build.sh downloadjdk)
+(cd $CHECKERFRAMEWORK && ./gradlew assembleForJavac)
 
 # Finally build checker-framework-inference
 ./gradlew dist && ./gradlew testLibJar

.ci-build.sh

@@ -46,7 +46,7 @@ if [[ "${GROUP}" == downstream* && "${SLUGOWNER}" == "opprop" ]]; then
     clone_downstream () {
         DOWNSTREAM_PROJ="$(pwd -P)/../$1"
         echo "clone downstream to: ${DOWNSTREAM_PROJ}"
-        COMMAND="/tmp/plume-scripts/git-clone-related opprop $1 ${DOWNSTREAM_PROJ}"
+        COMMAND="/tmp/git-scripts/git-clone-related opprop $1 ${DOWNSTREAM_PROJ}"
         echo "Running: ($COMMAND)"
         (eval $COMMAND)
         echo "... done: ($COMMAND)"

.github/workflows/main.yml

@@ -14,30 +14,35 @@ jobs:
       fail-fast: false
       matrix:
         group: [ cfi-tests, downstream-ontology, downstream-security-demo, downstream-universe ]
-        jdk: [ 8, 11 ]
+        jdk: [ 8, 11, 17 ]
     runs-on: ubuntu-latest
     steps:
       - name: Install dependencies
         run: |
           sudo apt update
-          sudo apt install ant cpp gradle jq libcurl3-gnutls make maven mercurial python3-requests unzip wget binutils build-essential
+          sudo apt install ant cpp gradle jq libcurl3-gnutls make mercurial python3-requests unzip wget binutils build-essential
+      - name: Set up Maven
+        uses: stCarolas/setup-maven@v4.5
+        with:
+          maven-version: 3.8.6
       - name: Pull Request Checkout
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
         with:
           ref: ${{github.event.pull_request.head.ref}}
           repository: ${{github.event.pull_request.head.repo.full_name}}
         if: github.head_ref != ''
       - name: Push Checkout
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
         if: github.head_ref == ''
       - name: Set up Python 3
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v4
         with:
           python-version: '3.8'
       - name: Set up Java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v3
         with:
           java-version: ${{ matrix.jdk }}
+          distribution: 'temurin'
       - name: Dump GitHub context
         env:
           GITHUB_CONTEXT: ${{ toJson(github) }}
@@ -46,6 +51,9 @@ jobs:
         run: |
           python3 -m pip install --upgrade pip
           if [ -f requirements.txt ]; then pip install -r requirements.txt; fi
+      - name: Spotless Check
+        if: matrix.jdk == 11 || matrix.jdk == 17
+        run: ./gradlew spotlessCheck
       - name: Build
         run: |
           export JAVA_TOOL_OPTIONS=-Dfile.encoding=UTF8

README.md

@@ -1,11 +1,8 @@
-Continuous integration status of master:
-![CFI status](https://github.com/opprop/checker-framework-inference/workflows/CI/badge.svg)
-
-Checker Framework Inference
+Checker Framework Inference [![Build Status](https://github.com/opprop/checker-framework-inference/workflows/CI/badge.svg)](https://github.com/opprop/checker-framework-inference/actions/workflows/main.yml)
 ===========================
 
 This project is a general type inference framework,
-built upon the [Checker Framework](https://checkerframework.org/).
+built upon the [EISOP Checker Framework](https://eisop.github.io/).
 
 Given a program with no type annotations, Checker Framework Inference produces a program with type annotations.
 
@@ -31,7 +28,7 @@ Configure Eclipse to edit Checker Framework Inference
 
 The instructions here assumes you have cloned this project into a folder called `checker-framework-inference`.
 
-1) Follow the instructions in the [Checker Framework Manual](https://checkerframework.org/manual/#building-eclipse)
+1) Follow the instructions in the [EISOP Checker Framework Manual](https://eisop.github.io/cf/manual/manual.html#eclipse)
 to download, build, and configure Eclipse to edit the Checker Framework. The Checker Framework Inference Eclipse
 project depends on the eclipse projects from Checker Framework.
 
@@ -95,7 +92,7 @@ To test the build:
 Execution
 ---------
 
-Verify you have all of the requirements.
+Verify you have all the requirements.
 
 ````
 ./scripts/inference
@@ -119,7 +116,7 @@ Available options are [INFER, TYPECHECK, ROUNDTRIP, ROUNDTRIP_TYPECHECK]
     Generates and solves the constraints and writes the results to default.jaif file
 
   * `TYPECHECK`:
-    Typechecks the existin code
+    Typechecks the existing code
 
   * `ROUNDTRIP`:
     Generates and solves the constraints and then inserts the results
@@ -146,10 +143,10 @@ The classpath that is required by target program.
 `checkers.inference.solver.PropagationSolver` and `checkers.inference.solver.SolverEngine` are real solvers
 at the moment.
 
-Omiting the solver will create an output that numbers all of the
+Omitting the solver will create an output that numbers all the
 annotation positions in the program.
 
-`checkers.inference.solver.DebugSolver` will output all of the
+`checkers.inference.solver.DebugSolver` will output all the
 constraints generated.
 
 
@@ -178,7 +175,7 @@ Specifies what concrete solver is going to use.
 
   * `LogiQL`: Encodes constraints as statements of LogiQL language and use LogicBlox to solve.
 
-  * `Z3` with bit vector theory: Encodes constraints as Max-SMT problem with bit vectory theory, and use Z3 library to solve.
+  * `Z3` with bit vector theory: Encodes constraints as Max-SMT problem with bit vector theory, and use Z3 library to solve.
 
 
   `MaxSat` solver is used by default.
@@ -187,7 +184,7 @@ Specifies what concrete solver is going to use.
 Specifies whether to separate constraints into multiple components through constraint graph and solve them respectively. The default value is true.
 
 * `solveInParallel`
-If constraints are separated by constraint graph, this arguments indicates whether to solve the components in parallel (multithreading). The default value is true.
+If constraints are separated by constraint graph, this argument indicates whether to solve the components in parallel (multithreading). The default value is true.
 
 * `collectStatistics`
 Specifies whether to collect statistic with respect to timing, size of constraints, size of encoding, etc. The default value is false.