Skip to content

Support of Z3 in Github Actions #539

Support of Z3 in Github Actions

Support of Z3 in Github Actions #539

Workflow file for this run

# This workflow uses actions that are not certified by GitHub.
# They are provided by a third-party and are governed by
# separate terms of service, privacy policy, and support
# documentation.
# This workflow will build a Java project with Gradle and cache/restore any dependencies to improve the workflow execution time
# For more information see: https://docs.github.com/en/actions/automating-builds-and-tests/building-and-testing-java-with-gradle
name: Formal Verification Plugin CI
on:
push:
branches: [ "formal-verification" ]
pull_request:
branches: [ "formal-verification" ]
permissions:
contents: read
checks: write
jobs:
build:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: Setup Z3
id: z3
uses: cda-tum/setup-z3@v1
with:
version: 4.8.7
- name: Setup Z3_EXE
run: export Z3_EXE = ${{ steps.z3.outputs.z3-root }}
- name: Set up JDK 11
uses: actions/setup-java@v3
with:
java-version: '11'
distribution: 'temurin'
- name: Disable required old JDK builds
run: echo kotlin.build.isObsoleteJdkOverrideEnabled=true > ./local.properties
- name: Setup Gradle
uses: gradle/gradle-build-action@v2
- name: Run test without contract
run: ./gradlew :kotlin-formver-compiler-plugin:test --tests org.jetbrains.kotlin.formver.plugin.runners.FirLightTreeFormVerPluginDiagnosticsTestGenerated\$No_contracts
- name: Run test with verifying
run: ./gradlew :kotlin-formver-compiler-plugin:test --tests org.jetbrains.kotlin.formver.plugin.runners.FirLightTreeFormVerPluginDiagnosticsTestGenerated\$Verifies
- name: Run test with verification errors
run: ./gradlew :kotlin-formver-compiler-plugin:test --tests org.jetbrains.kotlin.formver.plugin.runners.FirLightTreeFormVerPluginDiagnosticsTestGenerated\$Bad_contracts
- name: Run test for unique check
run: ./gradlew :kotlin-formver-compiler-plugin:test --tests org.jetbrains.kotlin.formver.plugin.runners.FirLightTreeFormVerPluginDiagnosticsTestGenerated\$Uniqueness
- name: Report failing test results
uses: mikepenz/action-junit-report@v4
if: failure()
with:
report_paths: '**/build/test-results/test/TEST-*.xml'