test.yml

# This Source Code Form is subject to the terms of the Mozilla Public
# License, v. 2.0. If a copy of the MPL was not distributed with this
# file, You can obtain one at http://mozilla.org/MPL/2.0/.
#
# Copyright (c) 2011-2022 ETH Zurich.

name: test

on:
  push: # run this workflow on every push
  pull_request: # run this workflow on every pull_request

jobs:
  setup-and-test:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout Project
        uses: actions/checkout@v3
      - name: Verify Gobra files (files mode)
        uses: ./
        with:
          files: 'test/files_test/file1.go test/files_test/file2.gobra'
          includePaths: 'test/include_path'
          timeout: 2m
      - name: Verify Gobra files with conditionalizePermissions (files mode)
        uses: ./
        with:
          files: 'test/files_test/file1.go test/files_test/file2.gobra'
          includePaths: 'test/include_path'
          timeout: 2m
          conditionalizePermissions: '1'
            # disableNL: '1'
      - name: Verify chopped Gobra files
        uses: ./
        with:
          files: 'test/files_test/file1.go@11 test/files_test/file2.gobra'
          includePaths: 'test/include_path'
          timeout: 2m
          overflow: 1
      - name: Verify Gobra files with the Z3 API
        uses: ./
        with:
          files: 'test/files_test/file1.go test/files_test/file2.gobra'
          includePaths: 'test/include_path'
          timeout: 2m
          # useZ3API: '1'
      - name: Verify Gobra files (package mode)
        uses: ./
        with:
          packages: 'test/packages_test/test1/'
          timeout: 2m
      - name: Verify Gobra files (recursive mode)
        uses: ./
        with:
          projectLocation: 'gobra-action/test/'
          excludePackages: 'main timeout_test'
          recursive: '1'
          timeout: 2m
          checkConsistency: '1'
      - name: Verify Gobra files (recursive and headerOnly mode)
        uses: ./
        with:
          projectLocation: 'gobra-action/test/'
          excludePackages: 'main'
          recursive: '1'
          headerOnly: '1'
          timeout: 2m
          statsFile: '/stats/'
      - name: Verify Gobra files without moreCompleteExhale and with parallelizeBranches
        uses: ./
        with:
          packages: 'test/packages_test/test1/'
          timeout: 2m
          mceMde: 'off'
          parallelizeBranches: 1
      - name: Test that timeout reports an error
        continue-on-error: true
        uses: ./
        with:
          files: 'test/timeout_test/matching_loop.gobra'
          timeout: 10s
      - name: Upload statistics report
        uses: actions/upload-artifact@v2
        with:
          name: stats
          path: /stats/stats.json
          if-no-files-found: error # could also be 'warn' or 'ignore'