test xml

.cirrus.yml

@@ -1,18 +1,17 @@
 task:
   freebsd_instance:
     matrix:
-      - image_family: freebsd-12-2-snap
-      - image_family: freebsd-13-0-snap
+      - image_family: freebsd-15-0-snap
   deps_script:
     - sed -i.bak -e 's/quarterly/latest/' /etc/pkg/FreeBSD.conf
     - env ASSUME_ALWAYS_YES=yes pkg update -f
-    - env ASSUME_ALWAYS_YES=yes pkg install -y llvm90 gmake z3 cmake pkgconf google-perftools python3 py38-sqlite3 py38-tabulate
+    - env ASSUME_ALWAYS_YES=yes pkg install -y llvm13 gmake z3 cmake pkgconf google-perftools python311 py311-sqlite3 py311-tabulate
   build_script:
     - mkdir build
     - cd build
-    - cmake -DLLVM_CONFIG_BINARY=/usr/local/bin/llvm-config90 -DMAKE_BINARY=/usr/local/bin/gmake -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON ..
+    - cmake -DLLVM_DIR=/usr/local/llvm11 -DMAKE_BINARY=/usr/local/bin/gmake -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON ..
     - gmake
   test_script:
-    - sed -i.bak -e 's/lit\./lit90\./' test/lit.cfg
+    - sed -i.bak -e 's/lit\./lit13\./' test/lit.cfg
     - cd build
     - gmake check

.clang-format

@@ -1,4 +1,4 @@
 ---
-BasedOnStyle:  LLVM
-Standard: Cpp11
+BasedOnStyle: LLVM
+Standard: c++17
 ...

.codecov.yml

@@ -2,21 +2,22 @@ codecov:
   disable_default_path_fixes: true
 
 coverage:
+  range: 70...90
+  precision: 2
+  round: down
   status:
     project: no
     patch: yes
     changes: no
-  precision: 2
-  round: down
-  range: "70...100"
 
 fixes:
   - "/tmp/klee_src::"
+
 ignore:
-  - "usr/"
   - "test/"
   - "unittests"
   - "**/test-utils"
+
 comment:
   layout: "header, diff, changes, uncovered, tree"
   behavior: default

.github/ISSUE_TEMPLATE/question.md

@@ -8,8 +8,8 @@ assignees: ''
 ---
 
 To ask a question about KLEE:
-1. Please first check the documentation at http://klee.github.io/docs/
+1. Please first check the documentation at https://klee-se.org/docs/
 2. Then check the [searchable mailing list archive](https://www.mail-archive.com/[email protected]/)
-3. If this still doesn’t answer your questions then please send an email to the [klee-dev mailing list](http://klee.github.io/klee-dev/)
+3. If this still doesn’t answer your questions then please send an email to the [klee-dev mailing list](https://klee-se.org/klee-dev/)
 
 **We will normally not answer questions asked on GitHub.**

.github/pull_request_template.md

@@ -1,7 +1,7 @@
 <!--
 Thank you for contributing to KLEE. We are looking forward to reviewing your PR. However, given the small number of active reviewers and our limited time, it might take a while to do so. We aim to get back to each PR within one month, and often do so within one week.
 
-To review your PR, please add a summary of the proposed changes and ensure all items are fulfilled in the checklist above, by placing an "x" inside each applicable pair of brackets. More details about each item can be found in the [Developer's Guide](https://klee.github.io/docs/developers-guide/#pull-requests).
+To review your PR, please add a summary of the proposed changes and ensure all items are fulfilled in the checklist above, by placing an "x" inside each applicable pair of brackets. More details about each item can be found in the [Developer's Guide](https://klee-se.org/docs/developers-guide/#pull-requests).
 -->
 
 ## Summary: 

.github/workflows/build.yaml

@@ -1,3 +1,4 @@
+---
 name: CI
 
 on:
@@ -8,113 +9,101 @@ on:
 
 # Defaults for building KLEE
 env:
-  BASE_IMAGE: ubuntu:bionic-20200807
-  REPOSITORY: klee
+  BASE_IMAGE: ubuntu:jammy-20230126
+  REPOSITORY: ghcr.io/klee
   COVERAGE: 0
   DISABLE_ASSERTIONS: 0
   ENABLE_DOXYGEN: 0
   ENABLE_OPTIMIZED: 1
   ENABLE_DEBUG: 1
   GTEST_VERSION: 1.11.0
   KLEE_RUNTIME_BUILD: "Debug+Asserts"
-  LLVM_VERSION: 9
-  METASMT_VERSION: qf_abv
+  LLVM_VERSION: 13
   MINISAT_VERSION: "master"
   REQUIRES_RTTI: 0
   SOLVERS: STP:Z3
   STP_VERSION: 2.3.3
-  TCMALLOC_VERSION: 2.7
-  UCLIBC_VERSION: klee_uclibc_v1.2
+  TCMALLOC_VERSION: 2.9.1
+  UCLIBC_VERSION: klee_uclibc_v1.4
   USE_TCMALLOC: 1
   USE_LIBCXX: 1
-  Z3_VERSION: 4.8.14
+  Z3_VERSION: 4.8.15
+  SQLITE_VERSION: 3400100
 
 jobs:
   Linux:
     runs-on: ubuntu-latest
     strategy:
       matrix:
         name: [
-                "LLVM 13",
-                "LLVM 12",
-                "LLVM 11, Doxygen",
-                "LLVM 10",
-                "LLVM 9",
-                "LLVM 8",
-                "LLVM 7",
-                "LLVM 6",
-                "ASan",
-                "UBSan",
-                "MSan",
-                "Z3 only",
-                "metaSMT STP",
-                "metaSMT Boolector",
-                "STP master",
-                "Latest klee-uclibc",
-                "Asserts enabled",
-                "No TCMalloc, optimised runtime",
-            ]
+          "LLVM 16",
+          "LLVM 15",
+          "LLVM 14",
+          "LLVM 13, Doxygen",
+          "LLVM 12",
+          "LLVM 11",
+          "ASan",
+          "UBSan",
+          "MSan",
+          "Z3 only",
+          "metaSMT",
+          "STP master",
+          "Latest klee-uclibc",
+          "Asserts disabled",
+          "No TCMalloc, optimised runtime",
+        ]
         include:
-          - name: "LLVM 13"
+          - name: "LLVM 16"
+            env:
+              LLVM_VERSION: 16
+          - name: "LLVM 15"
+            env:
+              LLVM_VERSION: 15
+          - name: "LLVM 14"
+            env:
+              LLVM_VERSION: 14
+          - name: "LLVM 13, Doxygen"
             env:
               LLVM_VERSION: 13
+              ENABLE_DOXYGEN: 1
           - name: "LLVM 12"
             env:
               LLVM_VERSION: 12
-          - name: "LLVM 11, Doxygen"
+          - name: "LLVM 11"
             env:
               LLVM_VERSION: 11
-              ENABLE_DOXYGEN: 1
-          - name: "LLVM 10"
-            env:
-              LLVM_VERSION: 10
-          - name: "LLVM 9"
-            env:
-              LLVM_VERSION: 9
-          - name: "LLVM 8"
-            env:
-              LLVM_VERSION: 8
-          - name: "LLVM 7"
-            env:
-              LLVM_VERSION: 7
-          - name: "LLVM 6"
-            env:
-              LLVM_VERSION: "6.0"
-          # Sanitizer builds. Do unoptimized build otherwise the optimizer might remove problematic code
+          # Sanitizer builds. Do unoptimized build otherwise the optimizer
+          # might remove problematic code
           - name: "ASan"
             env:
               SANITIZER_BUILD: address
               ENABLE_OPTIMIZED: 0
               USE_TCMALLOC: 0
-              SANITIZER_LLVM_VERSION: 11
+              SANITIZER_LLVM_VERSION: 13
           - name: "UBSan"
             env:
               SANITIZER_BUILD: undefined
               ENABLE_OPTIMIZED: 0
               USE_TCMALLOC: 0
-              SANITIZER_LLVM_VERSION: 11
+              SANITIZER_LLVM_VERSION: 13
           - name: "MSan"
             env:
               SANITIZER_BUILD: memory
               ENABLE_OPTIMIZED: 0
               USE_TCMALLOC: 0
               SOLVERS: STP
-              SANITIZER_LLVM_VERSION: 11
-            # Test just using Z3 only
+              SANITIZER_LLVM_VERSION: 14
+          # Test just using Z3 only
           - name: "Z3 only"
             env:
               SOLVERS: Z3
           # Test just using metaSMT
-          - name: "metaSMT STP"
+          - name: "metaSMT"
             env:
+              METASMT_VERSION: qf_abv
               SOLVERS: metaSMT
               METASMT_DEFAULT: STP
               REQUIRES_RTTI: 1
-          - name: "metaSMT Boolector"
-            env:
-              SOLVERS: metaSMT
-              METASMT_DEFAULT: BTOR
-              REQUIRES_RTTI: 1
           # Test we can build against STP master
           - name: "STP master"
             env:
@@ -125,7 +114,7 @@ jobs:
             env:
               UCLIBC_VERSION: klee_0_9_29
           # Check at least one build with Asserts disabled.
-          - name: "Asserts enabled"
+          - name: "Asserts disabled"
             env:
               SOLVERS: STP
               DISABLE_ASSERTIONS: 1
@@ -136,16 +125,19 @@ jobs:
               KLEE_RUNTIME_BUILD: "Release+Debug+Asserts"
     steps:
       - name: Checkout KLEE source code
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
       - name: Build KLEE
         env: ${{ matrix.env }}
         run: scripts/build/build.sh klee --docker --create-final-image
       - name: Run tests
-        run: scripts/build/run-tests.sh --run-docker --debug
+        run: | # XXX: Workaround for https://github.com/llvm/llvm-project/issues/78354
+             sudo sysctl vm.mmap_rnd_bits=28
+             scripts/build/run-tests.sh --run-docker --debug
 
   macOS:
     runs-on: macos-latest
     env:
+      LLVM_VERSION: 14
       BASE: /tmp
       SOLVERS: STP
       UCLIBC_VERSION: 0
@@ -155,7 +147,7 @@ jobs:
       - name: Install newer version of Bash
         run: brew install bash
       - name: Checkout KLEE source code
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
       - name: Build KLEE
         run: scripts/build/build.sh klee --debug --install-system-deps
       - name: Run tests
@@ -165,19 +157,38 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout KLEE Code
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
       - name: Build Docker image
         run: docker build .
 
   Coverage:
     runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        name: [
+          "STP",
+          "Z3",
+        ]
+        include:
+          - name: "STP"
+            env:
+              SOLVERS: STP:Z3
+          - name: "Z3"
+            env:
+              SOLVERS: Z3
     env:
       ENABLE_OPTIMIZED: 0
       COVERAGE: 1
     steps:
       - name: Checkout KLEE source code
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
+        with:
+          # Codecov may run into "Issue detecting commit SHA. Please run
+          # actions/checkout with fetch-depth > 1 or set to 0" when uploading.
+          # See also https://github.com/codecov/codecov-action/issues/190
+          fetch-depth: 2
       - name: Build KLEE
+        env: ${{ matrix.env }}
         run: scripts/build/build.sh klee --docker --create-final-image
       - name: Run tests
         run: scripts/build/run-tests.sh --coverage --upload-coverage --run-docker --debug

.github/workflows/differential-shellcheck.yml

@@ -0,0 +1,32 @@
+# Doc: https://github.com/redhat-plumbers-in-action/differential-shellcheck#usage
+---
+
+name: Differential ShellCheck
+on:
+  push:
+    branches: [master]
+  pull_request:
+    branches: [master]
+
+permissions:
+  contents: read
+
+jobs:
+  lint:
+    runs-on: ubuntu-latest
+
+    permissions:
+      security-events: write
+
+    steps:
+      - name: Repository checkout
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Differential ShellCheck
+        uses: redhat-plumbers-in-action/differential-shellcheck@v5
+        with:
+          severity: warning
+          include-path: scripts/**.inc
+          token: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/docker_release_push.yml

@@ -0,0 +1,34 @@
+name: Publish Docker Image for Release Builds
+
+on:
+  release:
+    types: [published]
+
+jobs:
+  push_to_registry:
+    name: Push Docker Image to Docker Hub
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check out the repo
+        uses: actions/checkout@v4
+
+      - name: Log in to Docker Hub
+        uses: docker/login-action@f4ef78c080cd8ba55a85445d5b36e214a81df20a
+        with:
+          username: ${{ secrets.DOCKER_USERNAME }}
+          password: ${{ secrets.DOCKER_PASSWORD }}
+
+      - name: Extract metadata (tags, labels) for Docker
+        id: meta
+        uses: docker/metadata-action@9ec57ed1fcdbf14dcef7dfbe97b2010124a938b7
+        with:
+          images: klee/klee
+
+      - name: Build and push Docker image
+        uses: docker/build-push-action@3b5e8027fcad23fda98b2e3ac259d8d67585f671
+        with:
+          context: .
+          file: ./Dockerfile
+          push: true
+          tags: ${{ steps.meta.outputs.tags }}
+          labels: ${{ steps.meta.outputs.labels }}

.shellcheckrc

@@ -0,0 +1,3 @@
+# Tell ShellCheck to use bash when checking scripts
+# This is alternative for disable=SC2148
+shell=bash