Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/main' into issue-2383-toolchain
Browse files Browse the repository at this point in the history
 Conflicts:
    cprover_bindings/src/goto_program/expr.rs
    kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
    kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
    library/kani/src/lib.rs
    tests/ui/cbmc_checks/signed-overflow/expected
    tests/ui/cbmc_checks/unsigned-overflow/expected
  • Loading branch information
celinval committed May 1, 2023
2 parents 095e38e + 24c7076 commit 07e2d21
Show file tree
Hide file tree
Showing 73 changed files with 1,058 additions and 202 deletions.
43 changes: 41 additions & 2 deletions .github/workflows/kani.yml
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,29 @@ jobs:
KANI_ENABLE_WRITE_JSON_SYMTAB: 1
run: ./scripts/kani-regression.sh

benchcomp-tests:
runs-on: ubuntu-20.04
steps:
- name: Checkout Kani
uses: actions/checkout@v3

- name: Install benchcomp dependencies
run: |
sudo apt-get update
sudo apt-get install -y python3-pip
pushd tools/benchcomp && pip3 install -r requirements.txt
- name: Setup Kani Dependencies
uses: ./.github/actions/setup
with:
os: ubuntu-20.04

- name: Build Kani using release mode
run: cargo build-dev -- --release

- name: Run benchcomp unit and regression tests
run: pushd tools/benchcomp && PATH=$(realpath ../../scripts):$PATH test/run

perf:
runs-on: ubuntu-20.04
steps:
Expand Down Expand Up @@ -109,7 +132,7 @@ jobs:
# When we're pushed to main branch, only then actually publish the docs.
- name: Publish Documentation
if: ${{ github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }}
uses: JamesIves/github-pages-deploy-action@v4.3.3
uses: JamesIves/github-pages-deploy-action@v4
with:
branch: gh-pages
folder: docs/book/
Expand Down Expand Up @@ -283,4 +306,20 @@ jobs:
- name: Run benchcomp
run: |
new/tools/benchcomp/bin/benchcomp \
--config new/tools/benchcomp/configs/perf-regression.yaml
--config new/tools/benchcomp/configs/perf-regression.yaml \
run
new/tools/benchcomp/bin/benchcomp \
--config new/tools/benchcomp/configs/perf-regression.yaml \
collate
- name: Perf Regression Results Table
run: |
new/tools/benchcomp/bin/benchcomp \
--config new/tools/benchcomp/configs/perf-regression.yaml \
visualize --only dump_markdown_results_table >> "$GITHUB_STEP_SUMMARY"
- name: Run other visualizations
run: |
new/tools/benchcomp/bin/benchcomp \
--config new/tools/benchcomp/configs/perf-regression.yaml \
visualize --except dump_markdown_results_table
14 changes: 13 additions & 1 deletion CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,21 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)

This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.

## [0.26.0]

### What's Changed

* The Kani reference now includes an ["Attributes"](https://model-checking.github.io/kani/reference/attributes.html) section that describes each of the attributes available in Kani ([pull request](https://github.com/model-checking/kani/pull/2359) by @adpaco-aws)
* Users' choice of SAT solver, specified by the `solver` attribute, is now propagated to the loop-contract synthesizer ([pull request](https://github.com/model-checking/kani/pull/2320) by @qinheping)
* Unit tests generated by the concrete playback feature now compile correctly when using `RUSTFLAGS="--cfg=kani"` ([pull request](https://github.com/model-checking/kani/pull/2353) by @jaisnan)
* The Rust toolchain is updated to 2023-02-18 ([pull request](https://github.com/model-checking/kani/pull/2384) by @tautschnig)

**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.25.0...kani-0.26.0


## [0.25.0]

## What's Changed
### What's Changed

* Add implementation for the `#[kani::should_panic]` attribute by @adpaco-aws in https://github.com/model-checking/kani/pull/2315
* Upgrade Rust toolchain to nightly-2023-02-04 by @tautschnig in https://github.com/model-checking/kani/pull/2324
Expand Down
Loading

0 comments on commit 07e2d21

Please sign in to comment.