diff --git a/CHANGELOG.md b/CHANGELOG.md index e35af4c8fa24..f63acca901b3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,27 @@ 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.56.0] + +### Breaking Changes + +* Remove obsolete linker options (`--mir-linker` and `--legacy-linker`) by @zhassan-aws in https://github.com/model-checking/kani/pull/3559 + +### What's Changed + +* Enable stubbing and function contracts for primitive types by @celinval in https://github.com/model-checking/kani/pull/3496 +* Reduce object-bits for test to avoid OOM by @zhassan-aws in https://github.com/model-checking/kani/pull/3511 +* Instrument validity checks for pointer to reference casts for slices and str's by @zhassan-aws in https://github.com/model-checking/kani/pull/3513 +* Fail compilation if `proof_for_contract` is added to generic function by @carolynzech in https://github.com/model-checking/kani/pull/3522 +* Fix storing coverage data in cargo projects by @adpaco-aws in https://github.com/model-checking/kani/pull/3527 +* Add experimental API to generate arbitrary pointers by @celinval in https://github.com/model-checking/kani/pull/3538 +* Running `verify-std` no longer changes Cargo files by @celinval in https://github.com/model-checking/kani/pull/3577 +* Add an LLBC backend by @zhassan-aws in https://github.com/model-checking/kani/pull/3514 +* Rust toolchain upgraded to nightly-2024-10-03 by @qinheping @tautschnig @celinval in https://github.com/model-checking/kani/pull/3488 +* CBMC upgraded to 6.3.1 by @tautschnig in https://github.com/model-checking/kani/pull/3537 + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.55.0...kani-0.56.0 + ## [0.55.0] ### Major/Breaking Changes diff --git a/Cargo.lock b/Cargo.lock index 41fb02073f6a..21997d7bc332 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,21 +2,6 @@ # It is not intended for manual editing. version = 4 -[[package]] -name = "addr2line" -version = "0.24.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dfbe277e56a376000877090da837660b4427aad530e3028d44e0bffe4f89a1c1" -dependencies = [ - "gimli", -] - -[[package]] -name = "adler2" -version = "2.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627" - [[package]] name = "ahash" version = "0.8.11" @@ -39,15 +24,6 @@ dependencies = [ "memchr", ] -[[package]] -name = "ansi_term" -version = "0.12.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2" -dependencies = [ - "winapi", -] - [[package]] name = "anstream" version = "0.6.15" @@ -131,59 +107,12 @@ dependencies = [ "wait-timeout", ] -[[package]] -name = "assert_tokens_eq" -version = "0.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6b21f4c5ba5c8b55031306325f196df925939bcc2bd7188ce68fabd93fb4f149" -dependencies = [ - "ansi_term", - "ctor", - "difference", - "output_vt100", - "snafu", -] - [[package]] name = "autocfg" version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" -[[package]] -name = "backtrace" -version = "0.3.74" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8d82cb332cdfaed17ae235a638438ac4d4839913cc2af585c3c6746e8f8bee1a" -dependencies = [ - "addr2line", - "cfg-if", - "libc", - "miniz_oxide", - "object", - "rustc-demangle", - "windows-targets 0.52.6", -] - -[[package]] -name = "bincode" -version = "2.0.0-rc.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f11ea1a0346b94ef188834a65c068a03aec181c94896d481d7a0a40d85b0ce95" -dependencies = [ - "bincode_derive", - "serde", -] - -[[package]] -name = "bincode_derive" -version = "2.0.0-rc.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7e30759b3b99a1b802a7a3aa21c85c3ded5c28e1c83170d82d70f08bbf7f3e4c" -dependencies = [ - "virtue", -] - [[package]] name = "bitflags" version = "2.6.0" @@ -221,7 +150,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.55.0" +version = "0.56.0" dependencies = [ "anyhow", "cargo_metadata", @@ -295,14 +224,11 @@ dependencies = [ "derive-visitor", "env_logger", "hashlink", - "hax-frontend-exporter", - "ignore", "im", "index_vec", "indoc", "itertools 0.13.0", "lazy_static", - "libtest-mimic", "log", "macros", "nom", @@ -315,15 +241,12 @@ dependencies = [ "serde-map-to-array", "serde_json", "serde_stacker", - "snapbox", "stacker", "take_mut", - "tempfile", "toml", "tracing", "tracing-subscriber", "tracing-tree 0.3.1", - "walkdir", "which", ] @@ -356,8 +279,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4ac6a0c7b1a9e9a5186361f67dfa1b88213572f427fb9ab038efb2bd8c582dab" dependencies = [ "heck", - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] @@ -442,7 +365,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.55.0" +version = "0.56.0" dependencies = [ "lazy_static", "linear-map", @@ -523,16 +446,6 @@ dependencies = [ "memchr", ] -[[package]] -name = "ctor" -version = "0.1.26" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6d2301688392eb071b0bf1a37be05c469d3cc4dbbd95df672fe28ab021e6a096" -dependencies = [ - "quote 1.0.37", - "syn 1.0.109", -] - [[package]] name = "deranged" version = "0.3.11" @@ -548,8 +461,8 @@ version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 1.0.109", ] @@ -570,17 +483,11 @@ checksum = "427b39a85fecafea16b1a5f3f50437151022e35eb4fe038107f08adbf7f8def6" dependencies = [ "convert_case 0.4.0", "itertools 0.10.5", - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 1.0.109", ] -[[package]] -name = "difference" -version = "2.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "524cbf6897b527295dff137cec09ecf3a05f4fddffd7dfcd1585403449e74198" - [[package]] name = "difflib" version = "0.4.0" @@ -593,12 +500,6 @@ version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fea41bba32d969b513997752735605054bc0dfa92b4c56bf1189f2e174be7a10" -[[package]] -name = "dyn-clone" -version = "1.0.17" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0d6ef0072f8a535281e4876be788938b528e9a1d43900b82c2569af7da799125" - [[package]] name = "either" version = "1.13.0" @@ -650,41 +551,6 @@ dependencies = [ "windows-sys 0.52.0", ] -[[package]] -name = "escape8259" -version = "0.5.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5692dd7b5a1978a5aeb0ce83b7655c58ca8efdcb79d21036ea249da95afec2c6" - -[[package]] -name = "ext-trait" -version = "1.0.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d772df1c1a777963712fb68e014235e80863d6a91a85c4e06ba2d16243a310e5" -dependencies = [ - "ext-trait-proc_macros", -] - -[[package]] -name = "ext-trait-proc_macros" -version = "1.0.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ab7934152eaf26aa5aa9f7371408ad5af4c31357073c9e84c3b9d7f11ad639a" -dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", - "syn 1.0.109", -] - -[[package]] -name = "extension-traits" -version = "1.0.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a296e5a895621edf9fa8329c83aa1cb69a964643e36cf54d8d7a69b789089537" -dependencies = [ - "ext-trait", -] - [[package]] name = "fastrand" version = "2.1.1" @@ -717,31 +583,12 @@ dependencies = [ "wasi", ] -[[package]] -name = "gimli" -version = "0.31.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f" - [[package]] name = "glob" version = "0.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" -[[package]] -name = "globset" -version = "0.4.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "15f1ce686646e7f1e19bf7d5533fe443a45dbfb990e00629110797578b42fb19" -dependencies = [ - "aho-corasick", - "bstr", - "log", - "regex-automata 0.4.8", - "regex-syntax 0.8.5", -] - [[package]] name = "graph-cycles" version = "0.1.0" @@ -778,59 +625,12 @@ dependencies = [ "serde", ] -[[package]] -name = "hax-adt-into" -version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax?branch=main#496e381186de242f46ee2fd2b4b8971c70aa07a4" -dependencies = [ - "itertools 0.11.0", - "proc-macro2 1.0.86", - "quote 1.0.37", - "syn 1.0.109", -] - -[[package]] -name = "hax-frontend-exporter" -version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax?branch=main#496e381186de242f46ee2fd2b4b8971c70aa07a4" -dependencies = [ - "bincode", - "extension-traits", - "hax-adt-into", - "hax-frontend-exporter-options", - "itertools 0.11.0", - "lazy_static", - "paste", - "schemars", - "serde", - "serde_json", - "tracing", -] - -[[package]] -name = "hax-frontend-exporter-options" -version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax?branch=main#496e381186de242f46ee2fd2b4b8971c70aa07a4" -dependencies = [ - "bincode", - "hax-adt-into", - "schemars", - "serde", - "serde_json", -] - [[package]] name = "heck" version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" -[[package]] -name = "hermit-abi" -version = "0.3.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024" - [[package]] name = "home" version = "0.5.9" @@ -846,22 +646,6 @@ version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" -[[package]] -name = "ignore" -version = "0.4.23" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6d89fd380afde86567dfba715db065673989d6253f42b88179abd3eae47bda4b" -dependencies = [ - "crossbeam-deque", - "globset", - "log", - "memchr", - "regex-automata 0.4.8", - "same-file", - "walkdir", - "winapi-util", -] - [[package]] name = "im" version = "15.1.0" @@ -922,15 +706,6 @@ dependencies = [ "either", ] -[[package]] -name = "itertools" -version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57" -dependencies = [ - "either", -] - [[package]] name = "itertools" version = "0.13.0" @@ -954,7 +729,7 @@ checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5" [[package]] name = "kani" -version = "0.55.0" +version = "0.56.0" dependencies = [ "kani_core", "kani_macros", @@ -962,7 +737,7 @@ dependencies = [ [[package]] name = "kani-compiler" -version = "0.55.0" +version = "0.56.0" dependencies = [ "charon", "clap", @@ -972,7 +747,7 @@ dependencies = [ "kani_metadata", "lazy_static", "num", - "quote 1.0.37", + "quote", "regex", "serde", "serde_json", @@ -987,7 +762,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.55.0" +version = "0.56.0" dependencies = [ "anyhow", "cargo_metadata", @@ -1016,7 +791,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.55.0" +version = "0.56.0" dependencies = [ "anyhow", "home", @@ -1025,24 +800,24 @@ dependencies = [ [[package]] name = "kani_core" -version = "0.55.0" +version = "0.56.0" dependencies = [ "kani_macros", ] [[package]] name = "kani_macros" -version = "0.55.0" +version = "0.56.0" dependencies = [ "proc-macro-error2", - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] [[package]] name = "kani_metadata" -version = "0.55.0" +version = "0.56.0" dependencies = [ "clap", "cprover_bindings", @@ -1063,18 +838,6 @@ version = "0.2.159" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "561d97a539a36e26a9a5fad1ea11a3039a67714694aaa379433e580854bc3dc5" -[[package]] -name = "libtest-mimic" -version = "0.7.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cc0bda45ed5b3a2904262c1bb91e526127aa70e7ef3758aba2ef93cf896b9b58" -dependencies = [ - "clap", - "escape8259", - "termcolor", - "threadpool", -] - [[package]] name = "linear-map" version = "1.2.0" @@ -1111,9 +874,8 @@ checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24" name = "macros" version = "0.1.0" dependencies = [ - "assert_tokens_eq", - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] @@ -1144,15 +906,6 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" -[[package]] -name = "miniz_oxide" -version = "0.8.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1" -dependencies = [ - "adler2", -] - [[package]] name = "nom" version = "7.1.3" @@ -1176,12 +929,6 @@ dependencies = [ "nom", ] -[[package]] -name = "normalize-line-endings" -version = "0.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61807f77802ff30975e01f4f071c8ba10c022052f98b3294119f3e615d13e5be" - [[package]] name = "nu-ansi-term" version = "0.46.0" @@ -1280,25 +1027,6 @@ dependencies = [ "autocfg", ] -[[package]] -name = "num_cpus" -version = "1.16.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4161fcb6d602d4d2081af7c3a45852d875a03dd337a6bfdd6e06407b61342a43" -dependencies = [ - "hermit-abi", - "libc", -] - -[[package]] -name = "object" -version = "0.36.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e" -dependencies = [ - "memchr", -] - [[package]] name = "once_cell" version = "1.20.2" @@ -1315,15 +1043,6 @@ dependencies = [ "windows-sys 0.52.0", ] -[[package]] -name = "output_vt100" -version = "0.1.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "628223faebab4e3e40667ee0b2336d34a5b960ff60ea743ddfdbcf7770bcfb66" -dependencies = [ - "winapi", -] - [[package]] name = "overload" version = "0.1.1" @@ -1353,12 +1072,6 @@ dependencies = [ "windows-targets 0.52.6", ] -[[package]] -name = "paste" -version = "1.0.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" - [[package]] name = "pathdiff" version = "0.2.1" @@ -1440,8 +1153,8 @@ version = "2.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", ] [[package]] @@ -1451,20 +1164,11 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802" dependencies = [ "proc-macro-error-attr2", - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] -[[package]] -name = "proc-macro2" -version = "0.4.30" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cf3d2011ab5c909338f7887f4fc896d35932e29146c12c8d01da6b22a80ba759" -dependencies = [ - "unicode-xid", -] - [[package]] name = "proc-macro2" version = "1.0.86" @@ -1483,22 +1187,13 @@ dependencies = [ "cc", ] -[[package]] -name = "quote" -version = "0.6.13" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ce23b6b870e8f94f81fb0a363d65d86675884b34a09043c81e5562f11c1f8e1" -dependencies = [ - "proc-macro2 0.4.30", -] - [[package]] name = "quote" version = "1.0.37" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" dependencies = [ - "proc-macro2 1.0.86", + "proc-macro2", ] [[package]] @@ -1674,30 +1369,6 @@ dependencies = [ "strum_macros", ] -[[package]] -name = "schemars" -version = "0.8.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09c024468a378b7e36765cd36702b7a90cc3cba11654f6685c8f233408e89e92" -dependencies = [ - "dyn-clone", - "schemars_derive", - "serde", - "serde_json", -] - -[[package]] -name = "schemars_derive" -version = "0.8.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b1eee588578aff73f856ab961cd2f79e36bc45d7ded33a7562adba4667aecc0e" -dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", - "serde_derive_internals", - "syn 2.0.79", -] - [[package]] name = "scopeguard" version = "1.2.0" @@ -1737,19 +1408,8 @@ version = "1.0.210" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", - "syn 2.0.79", -] - -[[package]] -name = "serde_derive_internals" -version = "0.29.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "18d26a20a969b9e3fdf2fc2d9f21eda6c40e2de84c9408bb5d3b05d499aae711" -dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] @@ -1827,12 +1487,6 @@ version = "1.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" -[[package]] -name = "similar" -version = "2.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1de1d4f81173b03af4c0cbed3c898f6bff5b870e4a7f5d6f4057d62a7a4b686e" - [[package]] name = "sized-chunks" version = "0.6.5" @@ -1849,50 +1503,6 @@ version = "1.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" -[[package]] -name = "snafu" -version = "0.4.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b028158eb06caa8345bee10cccfb25fa632beccf0ef5308832b4fd4b78a7db48" -dependencies = [ - "backtrace", - "doc-comment", - "snafu-derive", -] - -[[package]] -name = "snafu-derive" -version = "0.4.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bf50aaef500c248a590e2696e8bf8c7620ca2235b9bb90a70363d82dd1abec6a" -dependencies = [ - "proc-macro2 0.4.30", - "quote 0.6.13", - "syn 0.15.44", -] - -[[package]] -name = "snapbox" -version = "0.6.18" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7ba434818a8a9b1b106404288d6bd75a94348aae8fc9a518b211b609a36a54bc" -dependencies = [ - "anstream", - "anstyle", - "normalize-line-endings", - "similar", - "snapbox-macros", -] - -[[package]] -name = "snapbox-macros" -version = "0.3.10" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "16569f53ca23a41bb6f62e0a5084aa1661f4814a67fa33696a79073e03a664af" -dependencies = [ - "anstream", -] - [[package]] name = "stacker" version = "0.1.17" @@ -1908,7 +1518,7 @@ dependencies = [ [[package]] name = "std" -version = "0.55.0" +version = "0.56.0" dependencies = [ "kani", ] @@ -1943,31 +1553,20 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4c6bee85a5a24955dc440386795aa378cd9cf82acd5f764469152d2270e581be" dependencies = [ "heck", - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "rustversion", "syn 2.0.79", ] -[[package]] -name = "syn" -version = "0.15.44" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9ca4b3b69a77cbe1ffc9e198781b7acb0c7365a883670e8f1c1bc66fba79a5c5" -dependencies = [ - "proc-macro2 0.4.30", - "quote 0.6.13", - "unicode-xid", -] - [[package]] name = "syn" version = "1.0.109" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "unicode-ident", ] @@ -1977,8 +1576,8 @@ version = "2.0.79" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "unicode-ident", ] @@ -2001,15 +1600,6 @@ dependencies = [ "windows-sys 0.59.0", ] -[[package]] -name = "termcolor" -version = "1.4.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755" -dependencies = [ - "winapi-util", -] - [[package]] name = "termtree" version = "0.4.1" @@ -2031,8 +1621,8 @@ version = "1.0.64" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "08904e7672f5eb876eaaf87e0ce17857500934f4981c4a0ab2b4aa98baac7fc3" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] @@ -2046,15 +1636,6 @@ dependencies = [ "once_cell", ] -[[package]] -name = "threadpool" -version = "1.8.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d050e60b33d41c19108b32cea32164033a9013fe3b46cbd4457559bfbf77afaa" -dependencies = [ - "num_cpus", -] - [[package]] name = "time" version = "0.3.36" @@ -2137,8 +1718,8 @@ version = "0.1.27" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] @@ -2249,12 +1830,6 @@ version = "0.1.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af" -[[package]] -name = "unicode-xid" -version = "0.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fc72304796d0818e357ead4e000d19c9c174ab23dc11093ac919054d20a6a7fc" - [[package]] name = "unsafe-libyaml" version = "0.2.11" @@ -2279,12 +1854,6 @@ version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" -[[package]] -name = "virtue" -version = "0.0.13" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9dcc60c0624df774c82a0ef104151231d37da4962957d691c011c852b2473314" - [[package]] name = "wait-timeout" version = "0.2.0" @@ -2532,7 +2101,7 @@ version = "0.7.35" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] diff --git a/Cargo.toml b/Cargo.toml index ee9848b578dc..42c6f2c722b6 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.55.0" +version = "0.56.0" edition = "2021" description = "A bit-precise model checker for Rust." readme = "README.md" @@ -56,6 +56,7 @@ default-members = [ exclude = [ "build", + "charon", "target", # dependency tests have their own workspace "tests/kani-dependency-test/dependency3", diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index 008c81aef2ad..e26f23d5c081 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 0360763f9068..7b17e6073bb3 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 7485d2279ad6..555534959474 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.55.0" +version = "0.56.0" edition = "2021" description = "Build a project with Kani and run all proof harnesses" license = "MIT OR Apache-2.0" diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index 18eadc4095ed..2a0a03401c40 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index fa50783516f4..3ad1b286ebe6 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index 447cd0b3f298..df55e6278282 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_core" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 6930366b84fc..a7876176adb2 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 12c923e9b655..e1e353704723 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -5,7 +5,7 @@ # Note: this package is intentionally named std to make sure the names of # standard library symbols are preserved name = "std" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index 41095f1d7c3c..25e022e70d3f 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.55.0" +version = "0.56.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0"