Tags: gmh5225/kani
Tags
Bump Kani version to 0.55.0 (model-checking#3486) These are the auto-generated release notes: ## What's Changed * Update CBMC build instructions for Amazon Linux 2 by @tautschnig in model-checking#3431 * Handle intrinsics systematically by @artemagvanian in model-checking#3422 * Bump tests/perf/s2n-quic from `445f73b` to `ab9723a` by @dependabot in model-checking#3434 * Automatic cargo update to 2024-08-12 by @github-actions in model-checking#3433 * Actually apply CBMC patch by @tautschnig in model-checking#3436 * Update features/verify-rust-std branch by @feliperodri in model-checking#3435 * Add test related to issue 3432 by @celinval in model-checking#3439 * Implement memory initialization state copy functionality by @artemagvanian in model-checking#3350 * Bump tests/perf/s2n-quic from `ab9723a` to `80b93a7` by @dependabot in model-checking#3453 * Make points-to analysis handle all intrinsics explicitly by @artemagvanian in model-checking#3452 * Automatic cargo update to 2024-08-19 by @github-actions in model-checking#3450 * Add loop scanner to tool-scanner by @qinheping in model-checking#3443 * Avoid corner-cases by grouping instrumentation into basic blocks and using backward iteration by @artemagvanian in model-checking#3438 * Re-enabled hierarchical logs in the compiler by @celinval in model-checking#3449 * Fix ICE due to mishandling of Aggregate rvalue for raw pointers to `str` by @celinval in model-checking#3448 * Automatic cargo update to 2024-08-26 by @github-actions in model-checking#3459 * Bump tests/perf/s2n-quic from `80b93a7` to `8f7c04b` by @dependabot in model-checking#3460 * Update deny action by @zhassan-aws in model-checking#3461 * Basic support for memory initialization checks for unions by @artemagvanian in model-checking#3444 * Adjust test patterns so as not to check for trivial properties by @tautschnig in model-checking#3464 * Clarify comment in RFC Template by @carolynzech in model-checking#3462 * RFC: Source-based code coverage by @adpaco-aws in model-checking#3143 * Adopt Rust's source-based code coverage instrumentation by @adpaco-aws in model-checking#3119 * Upgrade toolchain to 08/28 by @jaisnan in model-checking#3454 * Extra tests and bug fixes to the delayed UB instrumentation by @artemagvanian in model-checking#3419 * Upgrade Toolchain to 8/29 by @carolynzech in model-checking#3468 * Automatic toolchain upgrade to nightly-2024-08-30 by @github-actions in model-checking#3469 * Extend name resolution to support qualified paths (Partial Fix) by @celinval in model-checking#3457 * Partially integrate uninit memory checks into `verify_std` by @artemagvanian in model-checking#3470 * Update Toolchain to 9/1 by @carolynzech in model-checking#3478 * Automatic cargo update to 2024-09-02 by @github-actions in model-checking#3480 * Bump tests/perf/s2n-quic from `8f7c04b` to `1ff3a9c` by @dependabot in model-checking#3481 * Automatic toolchain upgrade to nightly-2024-09-02 by @github-actions in model-checking#3479 * Automatic toolchain upgrade to nightly-2024-09-03 by @github-actions in model-checking#3482 * RFC for List Subcommand by @carolynzech in model-checking#3463 * Add tests for fixed issues. by @carolynzech in model-checking#3484 **Full Changelog**: model-checking/kani@kani-0.54.0...kani-0.55.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Bump Kani version to 0.54.0 (model-checking#3430) ## 0.54.0 ### Major Changes * We added support for slices in the `#[kani::modifies(...)]` clauses when using function contracts. * We introduce an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros. * We enabled support for concrete playback for harness that contains stubs or function contracts. * We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs. ### Breaking Changes * The `-Z ptr-to-ref-cast-checks` option has been removed, and pointer validity checks when casting raw pointers to references are now run by default. ## What's Changed * Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in model-checking#3332 * Fix visibility of some Kani intrinsics by @artemagvanian in model-checking#3323 * Function Contracts: Modify Slices by @pi314mm in model-checking#3295 * Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in model-checking#3344 * Add support for global transformations by @artemagvanian in model-checking#3348 * Enable an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros by @adpaco-aws in model-checking#3283 * Fix contract handling of promoted constants and constant static by @celinval in model-checking#3305 * Bump CBMC Viewer to 3.9 by @tautschnig in model-checking#3373 * Update to CBMC version 6.1.1 by @tautschnig in model-checking#2995 * Define a struct-level `#[safety_constraint(...)]` attribute by @adpaco-aws in model-checking#3270 * Enable concrete playback for contract and stubs by @celinval in model-checking#3389 * Add code scanner tool by @celinval in model-checking#3120 * Enable contracts in associated functions by @celinval in model-checking#3363 * Enable log2*, log10* intrinsics by @tautschnig in model-checking#3001 * Enable powif* intrinsics by @tautschnig in model-checking#2999 * Enable fma* intrinsics by @tautschnig in model-checking#3002 * Enable sqrt* intrinsics by @tautschnig in model-checking#3000 * Remove assigns clause for ZST pointers by @carolynzech in model-checking#3417 * Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in model-checking#3374 * Unify kani library and kani core logic by @jaisnan in model-checking#3333 * Stabilize pointer-to-reference cast validity checks by @artemagvanian in model-checking#3426 * Rust toolchain upgraded to `nightly-2024-08-07` by @jaisnan @qinheping @tautschnig @feliperodri ## New Contributors * @carolynzech made their first contribution in model-checking#3387 **Full Changelog**: model-checking/kani@kani-0.53.0...kani-0.54.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Bump Kani version to 0.53.0 (model-checking#3317) Bump Kani version to 0.53.0 and add notes for the upcoming release.
Bump Kani version to 0.52.0 (model-checking#3224) Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.51.0"/version = "0.52.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Bump tests/perf/s2n-quic from `6dd41e0` to `bd37960` by @dependabot in model-checking#3178 * Automatic cargo update to 2024-05-13 by @github-actions in model-checking#3177 * Upgrade toolchain to 2024-04-22 by @zhassan-aws in model-checking#3171 * Upgrade toolchain to 2024-05-14 by @zhassan-aws in model-checking#3183 * Automatic toolchain upgrade to nightly-2024-05-15 by @github-actions in model-checking#3185 * Include `--check-cfg=cfg(kani)` in the rust flags to avoid a warning about an unknown `cfg`. by @zhassan-aws in model-checking#3187 * Automatic toolchain upgrade to nightly-2024-05-16 by @github-actions in model-checking#3189 * Perform cargo update because of yanked libc version by @zhassan-aws in model-checking#3192 * Automatic toolchain upgrade to nightly-2024-05-17 by @github-actions in model-checking#3191 * Automatic cargo update to 2024-05-20 by @github-actions in model-checking#3195 * Bump tests/perf/s2n-quic from `bd37960` to `f5d9d74` by @dependabot in model-checking#3196 * New section about linter configuraton checking in the doc. by @remi-delmas-3000 in model-checking#3198 * Automatic cargo update to 2024-05-27 by @github-actions in model-checking#3201 * Bump tests/perf/s2n-quic from `f5d9d74` to `d03cc47` by @dependabot in model-checking#3202 * Update Rust toolchain from nightly-2024-05-17 to nightly-2024-05-23 by @remi-delmas-3000 in model-checking#3199 * Fix `{,e}println!()` by @GrigorenkoPV in model-checking#3209 * Contracts for a few core functions by @celinval in model-checking#3107 * Don't crash benchcomp when rounding non-numeric values by @karkhaz in model-checking#3211 * Update Rust toolchain nightly-2024-05-24 by @qinheping in model-checking#3212 * Upgrade Rust toolchain nightly-2024-05-27 by @qinheping in model-checking#3215 * Automatic toolchain upgrade to nightly-2024-05-28 by @github-actions in model-checking#3217 * Automatic cargo update to 2024-06-03 by @github-actions in model-checking#3220 * Bump tests/perf/s2n-quic from `d03cc47` to `d90729d` by @dependabot in model-checking#3222 * Add simple API for shadow memory by @zhassan-aws in model-checking#3200 ## New Contributors * @GrigorenkoPV made their first contribution in model-checking#3209 **Full Changelog**: model-checking/kani@kani-0.51.0...kani-0.52.0
Bump Kani version to 0.51.0 (model-checking#3176) For reference, here is the auto-generated changelog ## What's Changed * Upgrade toolchain to 2024-04-18 and improve toolchain workflow by @celinval in model-checking#3149 * Automatic toolchain upgrade to nightly-2024-04-19 by @github-actions in model-checking#3150 * Stabilize cover statement and update contracts RFC by @celinval in model-checking#3091 * Automatic toolchain upgrade to nightly-2024-04-20 by @github-actions in model-checking#3154 * Bump tests/perf/s2n-quic from `2d5e891` to `5f88e54` by @dependabot in model-checking#3140 * Automatic cargo update to 2024-04-22 by @github-actions in model-checking#3157 * Automatic toolchain upgrade to nightly-2024-04-21 by @github-actions in model-checking#3158 * Bump tests/perf/s2n-quic from `5f88e54` to `9730578` by @dependabot in model-checking#3159 * Fix cargo audit error by @jaisnan in model-checking#3160 * Fix cbmc-update CI job by @tautschnig in model-checking#3156 * Automatic cargo update to 2024-04-29 by @github-actions in model-checking#3165 * Bump tests/perf/s2n-quic from `9730578` to `1436af7` by @dependabot in model-checking#3166 * Do not assume that ZST-typed symbols refer to unique objects by @tautschnig in model-checking#3134 * Fix copyright check for `expected` tests by @adpaco-aws in model-checking#3170 * Remove kani::Arbitrary from the modifies contract instrumentation by @feliperodri in model-checking#3169 * Automatic cargo update to 2024-05-06 by @github-actions in model-checking#3172 * Bump tests/perf/s2n-quic from `1436af7` to `6dd41e0` by @dependabot in model-checking#3174 * Avoid unnecessary uses of Location::none() by @tautschnig in model-checking#3173 **Full Changelog**: model-checking/kani@kani-0.50.0...kani-0.51.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Bump dependencies and Kani's version to 0.50.0 (model-checking#3148) Release notes are the following: ### Major Changes * Fix compilation issue with proc_macro2 (v1.0.80+) and Kani v0.49.0 (model-checking#3138). ### What's Changed * Implement valid value check for `write_bytes` by @celinval in model-checking#3108 * Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval **Full Changelog**: model-checking/kani@kani-0.49.0...kani-0.50.0
Bump Kani version to 0.49.0 (model-checking#3126) Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.48.0"/version = "0.49.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Upgrade Rust toolchain to 2024-03-14 by @zhassan-aws in model-checking#3081 * Disable removal of storage markers by @zhassan-aws in model-checking#3083 * Automatic cargo update to 2024-03-18 by @github-actions in model-checking#3086 * Bump tests/perf/s2n-quic from `1a7faa8` to `9e39ca0` by @dependabot in model-checking#3087 * Upgrade toolchain to nightly-2024-03-15 by @celinval in model-checking#3084 * Add optional scatterplot to benchcomp output by @tautschnig in model-checking#3077 * Benchcomp scatterplots: quote axis labels by @tautschnig in model-checking#3097 * Expand ${var} in benchcomp variant `env` by @karkhaz in model-checking#3090 * Add test for model-checking#3099 by @zhassan-aws in model-checking#3100 * Automatic cargo update to 2024-03-25 by @github-actions in model-checking#3103 * Bump tests/perf/s2n-quic from `1a7faa8` to `0a60ec1` by @dependabot in model-checking#3104 * Implement validity checks by @celinval in model-checking#3085 * Add `benchcomp filter` command by @karkhaz in model-checking#3105 * Add CI test for --use-local-toolchain by @jaisnan in model-checking#3074 * Upgrade Rust toolchain to `nightly-2024-03-21` by @adpaco-aws in model-checking#3102 * Use `intrinsic_name` to get the intrinsic name by @adpaco-aws in model-checking#3114 * Bump tests/perf/s2n-quic from `0a60ec1` to `2d5e891` by @dependabot in model-checking#3118 * Allow modifies clause for verification only by @feliperodri in model-checking#3098 * Automatic cargo update to 2024-04-01 by @github-actions in model-checking#3117 * Automatic cargo update to 2024-04-04 by @github-actions in model-checking#3122 * Remove bookrunner by @tautschnig in model-checking#3123 * Upgrade Rust toolchain to nightly-2024-03-29 by @feliperodri in model-checking#3116 * Remove unnecessary build step for some workflows by @zhassan-aws in model-checking#3124 * Ensure storage markers are kept in std code by @zhassan-aws in model-checking#3080 **Full Changelog**: model-checking/kani@kani-0.48.0...kani-0.49.0
Revert clap from arg parsing during setup (model-checking#3078) `--help` and `--version` commands were being overriden by clap, so we are going back to the simple parsing with the added logic for `use-local-toolchain`. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Bump Kani version to 0.47.0 (model-checking#3039) ## What's Changed * Upgrade toolchain to 2024-02-14 by @zhassan-aws in model-checking#3036 **Full Changelog**: model-checking/kani@kani-0.46.0...kani-0.47.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Automatic toolchain upgrade to nightly-2024-01-25 (model-checking#3011) Update Rust toolchain from nightly-2024-01-24 to nightly-2024-01-25 without any other source changes. This is an automatically generated pull request. If any of the CI checks fail, manual intervention is required. In such a case, review the changes at https://github.com/rust-lang/rust from rust-lang/rust@5d3d347 up to rust-lang/rust@7ffc697.
PreviousNext