Testing CI

.github/workflows/test-action.yml

@@ -12,10 +12,63 @@ jobs:
       # you must check out the repository
       - name: Checkout
         uses: actions/checkout@v3
-      - name: Run Kani
+
+      - name: Run Kani with invalid version
+        id: set_error
+        uses: ./
+        with:
+          working-directory: tests/cargo-kani/simple-lib
+          kani-version: '0.1.10'
+        continue-on-error: true
+
+      - name: Check previous step outcome
+        id: get_error
+        run: |
+          # Check the outcome of "Run Kani with invalid version"
+          if [[ "${{ steps.set_error.outcome }}" == "failure" ]]; then
+            echo "Running Kani with invalid version "0.1.10" failed."
+          else
+            echo "::error::Running Kani with invalid version succeeded incorrectly or was skipped."
+            exit 1
+          fi
+
+      - name: Run Kani with older version
+        uses: ./ # Uses the action in the root directory
+        with:
+          working-directory: tests/cargo-kani/simple-lib
+          kani-version: '0.33.0'
+
+      - name: Test run Kani with older version
+        run: |
+          installed_version=$(kani --version | awk '{print $2}')
+          expected_version='0.33.0'
+
+          if [[ "$installed_version" == "$expected_version" ]]; then
+            echo "The installed version ($installed_version) matches the expected version ($expected_version)."
+          else
+            echo "::error::The installed version ($installed_version) does not match the expected version ($expected_version)."
+            exit 1
+          fi
+
+      - name: Run Kani with latest version
         uses: ./ # Uses the action in the root directory
         with:
           working-directory: tests/cargo-kani/simple-lib
+
+      - name: Test run Kani with latest version
+        run: |
+          installed_version=$(kani --version | awk '{print $2}')
+          expected_version=$(cargo search kani-verifier | grep -m 1 "kani" | awk '{print $3}' | sed 's/"//g')
+
+          echo "version online is $(cargo search kani-verifier | grep -m 1 "kani" | awk '{print $3}' | sed 's/"//g')."
+
+          if [[ "$installed_version" == "$expected_version" ]]; then
+            echo "The installed version ($installed_version) matches the latest version ($expected_version)"
+          else
+            echo "::error::The installed version ($installed_version) does not match the latest version ($expected_version)."
+            exit 1
+          fi
+
       - name: Test ProfProof within Kani Action
         uses: ./
         with:

README.md

@@ -2,6 +2,65 @@
 
 This repository provides a GitHub Action for running the [Kani Rust Verifier](https://github.com/model-checking/kani) in CI.
 
+## GitHub Action Parameters
+
+The following parameters can be used to configure and customize the behavior of this GitHub Action:
+
+NOTE: All the fields provided are optional and have default behaviors when not specified.
+
+`kani-version`
+
+- **Description**: Specifies the Kani version number to use.
+- **Default**: 'latest'
+- **Usage**: You can provide a specific version of Kani to use. If omitted, the latest version will be installed and used.
+
+`command`
+
+- **Description**: Specifies the command to run Kani.
+- **Default**: 'cargo-kani'
+- **Usage**: You can set a custom command to run Kani. For example, this allows you to use a different binary or script for Kani, if needed.
+
+`working-directory`
+
+- **Description**: Specifies the directory in which Kani should be run.
+- **Default**: '.'
+- **Usage**: Kani will be executed within this directory.
+
+`args`
+
+- **Description**: Specifies additional arguments to pass to Kani.
+- **Default**: ''
+- **Usage**: You can provide any additional command-line arguments to Kani using this parameter. These arguments will be appended to the Kani command.
+
+`enable-propproof`
+
+- **Description**: Experimental feature that allows Kani to verify proptest harnesses using the PropProof feature.
+- **Default**: false
+- **Usage**: If set to `true`, Kani will enable the experimental PropProof feature for verifying proptest harnesses.
+
+## Kani-version default behavior
+
+Please note that since providing `kani-version` is optional, if the user doesn't provide the version, the action will install the latest version of `Kani` on `crates.io`.
+
+## Example usage in a workflow YAML file:
+
+Here is an example of a workflow YAML file for the Kani Github Action
+
+```yaml
+jobs:
+  kani:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Run Kani
+        uses: model-checking/kani-github-action@v0.37
+        with:
+          kani-version: '0.35.0'
+          command: 'cargo-kani'
+          working-directory: './path/to/project'
+          args: '--tests'
+          enable-propproof: true
+```
+
 ## Security
 
 See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information.
@@ -10,4 +69,3 @@ See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more inform
 
 This code is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
 See [LICENSE-APACHE](LICENSE-APACHE) and [LICENSE-MIT](LICENSE-MIT) for details.
-

action.yml

@@ -10,6 +10,10 @@ branding:
   color: 'orange'
 
 inputs:
+  kani-version:
+    description: 'Kani Version number'
+    required: false
+    default: 'latest'
   command:
     description: 'Command to run.'
     required: false
@@ -34,11 +38,8 @@ runs:
       uses: dtolnay/rust-toolchain@stable
 
     - name: Install Kani
+      run: ${{ github.action_path }}/src/install-kani.sh ${{ inputs.kani-version }}
       shell: bash
-      run: |
-        export KANI_VERSION="0.36.0";
-        cargo install --version $KANI_VERSION --locked kani-verifier;
-        cargo-kani setup;
 
     - name: Install PropProof
       if: ${{ inputs.enable-propproof == 'true' }}

src/install-kani.sh

@@ -0,0 +1,39 @@
+#!/bin/bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# If version is latest, install directly from cargo
+if [ "$1" == "latest" ]; then
+    cargo install --locked kani-verifier;
+else
+    VERSION=$1
+    cargo install --version $VERSION --locked kani-verifier;
+fi
+
+# Check exit status for error handling
+if [ $? -eq 0 ]; then
+    echo "Installed Kani $VERSION successfully"
+else
+    echo "::error::Could not install Kani. Please check if the provided version is correct"
+    exit 1
+fi
+
+# Setup kani in ci
+cargo-kani setup;
+
+# Get the current installed version of kani and check it against the latest version
+installed_version=$(kani --version | awk '{print $2}')
+
+if [$? -eq 0]; then
+    if [ "$1" == "latest" ]; then
+        # Cargo search returns version number as string
+        requested_version=$(cargo search kani-verifier | grep -m 1 "^kani-verifier " | awk '{print $3}')
+    else
+        requested_version=$1
+    fi
+
+    if ["$installed_version" != "$requested_version"]; then
+        echo "::error::The version of Kani installed was different than the one requested"
+        exit 1
+    fi
+fi