Merge branch fix_diff_build into reuse

Author: PhilippWendler

.gitlab-ci.yml

@@ -115,6 +115,15 @@ java:
   tags:
     - privileged
 
+java-format:
+  stage: checks
+  image: openjdk:11
+  script: "java/check-format.sh"
+  cache:
+    key: "$CI_JOB_NAME"
+    paths:
+      - "java/*.jar"
+
 .build-docker:
   image:
     name: gcr.io/kaniko-project/executor:debug

.travis.yml

@@ -11,11 +11,12 @@ if: type = pull_request
 language: c
 env:
   matrix:
-    - NAME="Sanity checks" DOCKER_IMAGE=sanity-checks COMMAND="c/check.py"
-    - NAME="Preprocessing consistency checks" DOCKER_IMAGE=preprocessing-consistency COMMAND="cd c; ./diff_ci.sh './compare.py --keep-going --skip-large --directory'"
-    - NAME="gcc-5" DOCKER_IMAGE=gcc:5 COMMAND="gcc-5 -v --version; cd c; ./diff_ci.sh 'make -j2 CC=gcc-5 -C'"
-    - NAME="clang-3.9" DOCKER_IMAGE=clang:3.9 COMMAND="clang-3.9 -v --version; cd c; ./diff_ci.sh 'make -j2 CC=clang-3.9 -C'"
-    - NAME="java" DOCKER_IMAGE=java COMMAND="java/check-compile.sh"
+    - NAME="Sanity checks" DOCKER_IMAGE=registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/sanity-checks COMMAND="c/check.py"
+    - NAME="Preprocessing consistency checks" DOCKER_IMAGE=registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/preprocessing-consistency COMMAND="cd c; ./diff_ci.sh './compare.py --keep-going --skip-large --directory'"
+    - NAME="gcc-5" DOCKER_IMAGE=registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/gcc:5 COMMAND="gcc-5 -v --version; cd c; ./diff_ci.sh 'make -j2 CC=gcc-5 -C'"
+    - NAME="clang-3.9" DOCKER_IMAGE=registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/clang:3.9 COMMAND="clang-3.9 -v --version; cd c; ./diff_ci.sh 'make -j2 CC=clang-3.9 -C'"
+    - NAME="java" DOCKER_IMAGE=registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/java COMMAND="java/check-compile.sh"
+    - NAME="java-format" DOCKER_IMAGE=openjdk:11 COMMAND="java/check-format.sh"
 
 # Hint to TravisCI that we want to use their container infrastructure
 sudo: required
@@ -27,7 +28,7 @@ git:
   depth: 3
 
 before_install:
-  - docker pull registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/${DOCKER_IMAGE}
+  - docker pull ${DOCKER_IMAGE}
 
 script:
-  - docker run --privileged --tty --volume "$(pwd):$(pwd)" registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/${DOCKER_IMAGE} /bin/sh -c "cd $(pwd); ${COMMAND}"
+  - docker run --privileged --tty --volume "$(pwd):$(pwd)" ${DOCKER_IMAGE} /bin/sh -c "cd $(pwd); ${COMMAND}"

c/NoDataRace-Main.set

@@ -4,3 +4,4 @@ pthread/*.yml
 pthread-atomic/*.yml
 pthread-ext/*.yml
 pthread-lit/*.yml
+goblint-regression/*.yml

c/diff_ci.sh

@@ -39,7 +39,7 @@ find_parent_with_Makefile() {
 relevant_diff=`git diff --name-only --diff-filter=d origin/master... -- './*.i' './*.c' './*.h'`
 [ -z "$relevant_diff" ] && echo "Found nothing to build!!" && exit
 # dirs is the list of directories from the changed files
-dirs=`echo $relevant_diff | xargs dirname | cut -d/ -f2- | sort | uniq`
+dirs=`echo $relevant_diff | xargs dirname | cut -d/ -f2- -s | sort | uniq`
 
 printf "Selected following directories for diff build: \n$dirs \n"
 for d in $dirs

c/goblint-regression/00-sanity_09-include.c

@@ -0,0 +1,19 @@
+#include <stdlib.h>
+#include <pthread.h>
+
+int glob;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex);
+  glob++; // RACE!
+  pthread_mutex_unlock(&mutex);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  glob++; // RACE!
+  return 0;
+}