Merge branch 'master' into memsafety

.github/actions/build-archive/README.md

@@ -24,8 +24,8 @@ Minimal necessary packages for Ubuntu 22.04 LTS:
 ├── lib - contains the native library dependencies
 ├── offset.sh - creates a mapping between statements of two C files
 ├── solvers - contains further dependencies (SMT-solvers), each having their respective licenses 
-├── specification-transformation.bin - binary for transforming various specifications to reachability
-├── specification-transformation.bin.LICENSE - license for `specification-transformation.bin`
+├── specification-transformation - binaries for transforming various specifications to reachability (this includes cpachecker, but we do not use it for verification.)
+├── specification-transformation.LICENSE - license for `specification-transformation`
 ├── theta-smtlib.jar - the jarfile for installing and managing smt solvers (not necessary unless different solver versions are required)
 ├── theta-start.sh - the starting script of TOOL_NAME
 └── theta.jar - the main jarfile of TOOL_NAME

.github/actions/build-archive/action.yml

@@ -58,16 +58,14 @@ runs:
       with:
         name: specification-transformation
         path: ./
-    - name: Move file to overwrite specification-transformation.bin
-      shell: bash
-      run: |
-        mv specification-transformation.bin $GITHUB_ACTION_PATH/specification-transformation.bin
     - name: Copy specification transformation binary and license
       shell: bash
       run: |
-        cp $GITHUB_ACTION_PATH/specification-transformation.bin ${{ inputs.name }}/${{ inputs.name }}/
-        chmod +x ${{ inputs.name }}/${{ inputs.name }}/specification-transformation.bin
-        cp $GITHUB_ACTION_PATH/specification-transformation.bin.LICENSE ${{ inputs.name }}/${{ inputs.name }}/
+        zipfile=$(realpath ./specification-transformation.zip)
+        pushd ${{ inputs.name }}/${{ inputs.name }}/
+        unzip $zipfile
+        popd
+        cp $GITHUB_ACTION_PATH/specification-transformation.LICENSE ${{ inputs.name }}/${{ inputs.name }}/
         cp $GITHUB_ACTION_PATH/offset.sh ${{ inputs.name }}/${{ inputs.name }}/
     - name: ZIP archive
       shell: bash

.github/actions/build-spec-transformation/action.yml

@@ -7,8 +7,8 @@ runs:
     - name: Print file path
       shell: bash
       run: |
-        echo ${{ format('{0}/{1}', github.action_path, 'specification-transformation.bin') }}
-        ls -l ${{ format('{0}/{1}', github.action_path, 'specification-transformation.bin') }} && echo "file_exists=true" >> "$GITHUB_ENV" || echo "file_exists=false" >> "$GITHUB_ENV"
+        echo ${{ format('{0}/{1}', github.action_path, 'specification-transformation.zip') }}
+        ls -l ${{ format('{0}/{1}', github.action_path, 'specification-transformation.zip') }} && echo "file_exists=true" >> "$GITHUB_ENV" || echo "file_exists=false" >> "$GITHUB_ENV"
     - name: Setup java 17
       if: env.file_exists == 'false'
       uses: actions/setup-java@5ffc13f4174014e2d4d4572b3d74c3fa61aeb2c2 # v3.11.0
@@ -37,25 +37,19 @@ runs:
         mv lib/cpachecker/lib/java/runtime/*.jar cpachecker/runtime/
         mv lib/cpachecker/config cpachecker/
         mv lib/cpachecker/cpachecker.jar cpachecker/
-    - name: Install nuitka
+    - name: zip file
       if: env.file_exists == 'false'
       shell: bash
       run: |
-        sudo apt update && sudo apt -y --no-install-recommends install nuitka libfuse2
-    - name: Run nuitka
-      if: env.file_exists == 'false'
-      shell: bash
-      run: |
-        cd specification-transformation
-        bash -c "yes yes || true" | nuitka3 --onefile --standalone --include-data-dir="cpachecker=cpachecker" src/specification-transformation.py 
+        zip specification-transformation.zip specification-transformation/cpachecker specification-transformation/src -r
     - name: Move if exists
       if: env.file_exists == 'true'
       shell: bash
       run: |
         mkdir specification-transformation
-        mv $GITHUB_ACTION_PATH/specification-transformation.bin specification-transformation/
+        mv $GITHUB_ACTION_PATH/specification-transformation.zip ./
     - name: Upload results
       uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v3.1.2
       with:
         name: specification-transformation
-        path: specification-transformation/specification-transformation.bin
+        path: specification-transformation.zip

.github/actions/install-llvm/action.yml

@@ -11,15 +11,15 @@ runs:
       run: |
         # wget https://apt.llvm.org/llvm.sh
         # chmod +x llvm.sh
-        sudo $GITHUB_ACTION_PATH/llvm.sh ${{ inputs.version }}        
+        # sudo $GITHUB_ACTION_PATH/llvm.sh ${{ inputs.version }}        
 
-        sudo ln -sf $(which clang-${{inputs.version}}) /usr/bin/clang
-        sudo ln -sf $(which llvm-config-${{inputs.version}}) /usr/bin/llvm-config
+        # sudo ln -sf $(which clang-${{inputs.version}}) /usr/bin/clang
+        # sudo ln -sf $(which llvm-config-${{inputs.version}}) /usr/bin/llvm-config
 
     - name: Test version
       shell: bash
       run: |
-        ls -l $(which clang)
-        ls -l $(which llvm-config)
-        clang --version
-        llvm-config --version
+        # ls -l $(which clang)
+        # ls -l $(which llvm-config)
+        # clang --version
+        # llvm-config --version

.github/actions/install-llvm/llvm.sh

@@ -20,7 +20,7 @@ usage() {
     exit 1;
 }
 
-CURRENT_LLVM_STABLE=16
+CURRENT_LLVM_STABLE=18
 BASE_URL="http://apt.llvm.org"
 
 # Check for required tools
@@ -125,7 +125,10 @@ LLVM_VERSION_PATTERNS[13]="-13"
 LLVM_VERSION_PATTERNS[14]="-14"
 LLVM_VERSION_PATTERNS[15]="-15"
 LLVM_VERSION_PATTERNS[16]="-16"
-LLVM_VERSION_PATTERNS[17]=""
+LLVM_VERSION_PATTERNS[17]="-17"
+LLVM_VERSION_PATTERNS[18]="-18"
+LLVM_VERSION_PATTERNS[19]="-19"
+LLVM_VERSION_PATTERNS[20]=""
 
 if [ ! ${LLVM_VERSION_PATTERNS[$LLVM_VERSION]+_} ]; then
     echo "This script does not support LLVM version $LLVM_VERSION"
@@ -161,9 +164,15 @@ if [[ -z "`apt-key list 2> /dev/null | grep -i llvm`" ]]; then
     # Delete the key in the old format
     apt-key del AF4F7421
 fi
-add-apt-repository "${REPO_NAME}"
+if [[ "${VERSION_CODENAME}" == "bookworm" ]]; then
+    # add it twice to workaround:
+    # https://github.com/llvm/llvm-project/issues/62475
+    add-apt-repository -y "${REPO_NAME}"
+fi
+
+add-apt-repository -y "${REPO_NAME}"
 apt-get update
-PKG="clang-$LLVM_VERSION" # lldb-$LLVM_VERSION lld-$LLVM_VERSION clangd-$LLVM_VERSION"
+PKG="clang-$LLVM_VERSION lldb-$LLVM_VERSION lld-$LLVM_VERSION clangd-$LLVM_VERSION"
 if [[ $ALL -eq 1 ]]; then
     # same as in test-install.sh
     # No worries if we have dups

.github/workflows/check-copyright.yml

@@ -12,7 +12,7 @@ concurrency:
 
 jobs:
   check-copyright:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3

.github/workflows/check-formatting.yml

@@ -12,7 +12,7 @@ concurrency:
 
 jobs:
   check-formatting:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3

.github/workflows/check-version.yml

@@ -9,7 +9,7 @@ concurrency:
 
 jobs:
   check-version:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Set java home to java 17
         run: |

.github/workflows/linux-build-test-deploy.yml

@@ -18,7 +18,7 @@ concurrency:
 
 jobs:
   build:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -64,7 +64,7 @@ jobs:
             portfolio: BOUNDED
           - tool: Thorn_SV-COMP
             portfolio: HORN
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     needs: create-archives
     steps:
       - name: Checkout repository
@@ -78,23 +78,23 @@ jobs:
 
   collect-results:
     needs: test-benchexec
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
       - name: Generate report
         uses: ./.github/actions/benchexec-report
 
   create-spec-transformation:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
       - name: Create spec-transformation
         uses: ./.github/actions/build-spec-transformation
 
   create-archives:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     needs: [build, create-spec-transformation]
     strategy:
       matrix:
@@ -118,7 +118,7 @@ jobs:
 
   javadoc:
     needs: build
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -129,7 +129,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-latest]
+        os: [ubuntu-24.04]
     needs: build
     runs-on: ${{ matrix.os }}
     steps:
@@ -142,15 +142,15 @@ jobs:
       - name: Run tests
         uses: ./.github/actions/test-action
       - name: Positive outcome badge
-        if: ${{ matrix.os == 'ubuntu-latest' }}
+        if: ${{ matrix.os == 'ubuntu-24.04' }}
         uses: ./.github/actions/badge-creation
         with:
           label: "${{ runner.os }} test"
           status: "Success"
           color: "green"
           path: "badges/test-${{ runner.os }}"
       - name: Negative outcome badge
-        if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+        if: ${{ failure() && matrix.os == 'ubuntu-24.04' }}
         uses: ./.github/actions/badge-creation
         with:
           label: "${{ runner.os }} test"
@@ -162,7 +162,7 @@ jobs:
   deploy-release:
     needs: [test-linux, create-archives]
     if: "${{ github.event.inputs.message != '' &&  github.ref == 'refs/heads/master' && github.event_name != 'pull_request' }}"
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Set java home to java 17
         run: |
@@ -177,7 +177,7 @@ jobs:
   deploy-maven:
     # needs: test-linux
     if: "${{ github.event.inputs.message != '' && github.ref == 'refs/heads/master' && github.event_name != 'pull_request' }}"
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -194,7 +194,7 @@ jobs:
     strategy:
       matrix:
         dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli", "theta-xcfa-cli"]
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Set java home to java 17
         run: |
@@ -231,7 +231,7 @@ jobs:
     strategy:
       matrix:
         dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli", "theta-xcfa-cli"]
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Set java home to java 17
         run: |
@@ -269,7 +269,7 @@ jobs:
           repository: ftsrg/${{ matrix.dockerprojects }}
 
   deploy-docs:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3

.github/workflows/reformat-code.yml

@@ -10,7 +10,7 @@ on:
 
 jobs:
   reformat:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
     - uses: tibdex/github-app-token@b62528385c34dbc9f38e5f4225ac829252d1ea92
       id: generate-token

.github/workflows/sonar.yml

@@ -13,7 +13,7 @@ concurrency:
 
 jobs:
   run-sonar:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3

.github/workflows/version-bump.yml

@@ -15,7 +15,7 @@ on:
 
 jobs:
   version-bump:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
     - name: Set java home to java 17
       run: |

scripts/theta-start.sh

@@ -43,13 +43,13 @@ else
     if [ "$(basename "$property")" == "termination.prp" ]; then
         transformed_property=$(dirname "$property")/unreach-call.prp
         echo "Mapping property '$property' to '$transformed_property'"
-        "$scriptdir"/specification-transformation.bin --from-property termination --to-property reachability --algorithm InstrumentationOperator $IN
+        python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property termination --to-property reachability --algorithm InstrumentationOperator $IN
         "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
         IN="output/transformed_program.c"
     elif [ "$(basename "$property")" == "no-overflow.prp" ]; then
         transformed_property=$(dirname "$property")/unreach-call.prp
         echo "Mapping property '$property' to '$transformed_property'"
-        "$scriptdir"/specification-transformation.bin --from-property no-overflow --to-property reachability --algorithm InstrumentationOperator $IN
+        python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property no-overflow --to-property reachability --algorithm InstrumentationOperator $IN
         "$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
         IN="output/transformed_program.c"
     else