diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index ad2e339f19e1..36aee463061a 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -272,7 +272,7 @@ jobs: - name: Run tests # TODO: Customize compiletest to run custom kani. For now, just run a few cargo kani tests. run: | - for dir in simple-lib simple-visualize build-rs-works simple-kissat; do + for dir in simple-lib build-rs-works simple-kissat; do >&2 echo "Running test $dir" pushd tests/cargo-kani/$dir cargo kani @@ -312,7 +312,7 @@ jobs: - name: Run installed tests run: | - for dir in simple-lib simple-visualize build-rs-works simple-kissat; do + for dir in simple-lib build-rs-works simple-kissat; do >&2 echo "Running test $dir" docker run -v /var/run/docker.sock:/var/run/docker.sock \ -w /tmp/kani/tests/cargo-kani/$dir kani-18-04 cargo kani diff --git a/docs/src/build-from-source.md b/docs/src/build-from-source.md index 01860f5f37e4..253fcf351073 100644 --- a/docs/src/build-from-source.md +++ b/docs/src/build-from-source.md @@ -12,8 +12,7 @@ In general, the following dependencies are required to build Kani from source. 1. Cargo installed via [rustup](https://rustup.rs/) 2. [CBMC](https://github.com/diffblue/cbmc) (latest release) -3. [CBMC Viewer](https://github.com/awslabs/aws-viewer-for-cbmc) (latest release) -4. [Kissat](https://github.com/arminbiere/kissat) (Release 3.1.1) +3. [Kissat](https://github.com/arminbiere/kissat) (Release 3.1.1) Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##install-dependencies-on-macos) platforms. diff --git a/docs/src/install-guide.md b/docs/src/install-guide.md index 776209987ba1..d64ad3c89ce0 100644 --- a/docs/src/install-guide.md +++ b/docs/src/install-guide.md @@ -16,7 +16,6 @@ The following must already be installed: * **Python version 3.7 or newer** and the package installer `pip`. * Rust 1.58 or newer installed via `rustup`. -* `ctags` is required for Kani's `--visualize` option to work correctly. [Universal ctags](https://ctags.io/) is recommended. ## Installing the latest version diff --git a/docs/src/usage.md b/docs/src/usage.md index aaa5d3fa234c..60592aa56c9a 100644 --- a/docs/src/usage.md +++ b/docs/src/usage.md @@ -28,8 +28,6 @@ Common to both `kani` and `cargo kani` are many command-line flags: If used with `print`, Kani will only print the unit test to stdout. If used with `inplace`, Kani will automatically add the unit test to the user's source code, next to the proof harness. For more detailed instructions, see the [concrete playback](./experimental/concrete-playback.md) section. - * `--visualize`: _Experimental_, `--enable-unstable` feature that generates an HTML report providing traces (i.e., counterexamples) for each failure found by Kani. - * `--tests`: Build in "[test mode](https://doc.rust-lang.org/rustc/tests/index.html)", i.e. with `cfg(test)` set and `dev-dependencies` available (when using `cargo kani`). * `--harness `: By default, Kani checks all proof harnesses it finds. diff --git a/kani-dependencies b/kani-dependencies index ac6b353733a2..1f4428827e4e 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -2,9 +2,4 @@ CBMC_MAJOR="6" CBMC_MINOR="4" CBMC_VERSION="6.4.0" -# If you update this version number, remember to bump it in `src/setup.rs` too -CBMC_VIEWER_MAJOR="3" -CBMC_VIEWER_MINOR="10" -CBMC_VIEWER_VERSION="3.10" - KISSAT_VERSION="3.1.1" diff --git a/scripts/check-cbmc-viewer-version.py b/scripts/check-cbmc-viewer-version.py deleted file mode 100755 index 88c0f7ed31cb..000000000000 --- a/scripts/check-cbmc-viewer-version.py +++ /dev/null @@ -1,56 +0,0 @@ -#!/usr/bin/env python3 -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -import argparse -import re -import sys -import subprocess -from subprocess import PIPE - - -EXIT_CODE_SUCCESS = 0 -EXIT_CODE_MISMATCH = 1 -EXIT_CODE_FAIL = 2 - - -def cbmc_viewer_version(): - cmd = ["cbmc-viewer", "--version"] - try: - version = subprocess.run(cmd, stdout=PIPE, stderr=PIPE, check=True, - universal_newlines=True) - except (OSError, subprocess.SubprocessError) as error: - print(error) - print(f"Can't run command '{' '.join(cmd)}'") - sys.exit(EXIT_CODE_FAIL) - - match = re.match("CBMC viewer ([0-9]+).([0-9]+)", version.stdout) - if not match: - print(f"Can't parse CBMC-viewer version string: '{version.stdout.strip()}'") - sys.exit(EXIT_CODE_FAIL) - - return match.groups() - -def complete_version(*version): - numbers = [int(num) if num else 0 for num in version] - return (numbers + [0, 0])[:2] - -def main(): - parser = argparse.ArgumentParser( - description='Check CBMC-viewer version matches major/minor') - parser.add_argument('--major', required=True) - parser.add_argument('--minor', required=True) - args = parser.parse_args() - - current_version = complete_version(*cbmc_viewer_version()) - desired_version = complete_version(args.major, args.minor) - - if desired_version > current_version: - version_string = '.'.join([str(num) for num in current_version]) - desired_version_string = '.'.join([str(num) for num in desired_version]) - print(f'ERROR: CBMC-viewer version is {version_string}, expected at least {desired_version_string}') - sys.exit(EXIT_CODE_MISMATCH) - - -if __name__ == "__main__": - main() diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 728129d784b6..88215bdf0317 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -23,11 +23,8 @@ source "${KANI_DIR}/kani-dependencies" # Sanity check dependencies values. [[ "${CBMC_MAJOR}.${CBMC_MINOR}" == "${CBMC_VERSION%.*}" ]] || \ (echo "Conflicting CBMC versions"; exit 1) -[[ "${CBMC_VIEWER_MAJOR}.${CBMC_VIEWER_MINOR}" == "${CBMC_VIEWER_VERSION}" ]] || \ - (echo "Conflicting CBMC viewer versions"; exit 1) # Check if installed versions are correct. check-cbmc-version.py --major ${CBMC_MAJOR} --minor ${CBMC_MINOR} -check-cbmc-viewer-version.py --major ${CBMC_VIEWER_MAJOR} --minor ${CBMC_VIEWER_MINOR} check_kissat_version.sh # Formatting check diff --git a/scripts/setup/al2/install_deps.sh b/scripts/setup/al2/install_deps.sh index ce901ab8afa5..648715e9b055 100755 --- a/scripts/setup/al2/install_deps.sh +++ b/scripts/setup/al2/install_deps.sh @@ -31,7 +31,6 @@ python3 -m pip install autopep8 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" ${SCRIPT_DIR}/install_cbmc.sh -${SCRIPT_DIR}/install_viewer.sh # The Kissat installation script is platform-independent, so is placed one level up ${SCRIPT_DIR}/../install_kissat.sh ${SCRIPT_DIR}/../install_rustup.sh diff --git a/scripts/setup/al2/install_viewer.sh b/scripts/setup/al2/install_viewer.sh deleted file mode 100755 index c8ba7b7b838e..000000000000 --- a/scripts/setup/al2/install_viewer.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/bin/bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set -eu - -# Install cbmc-viewer - -# Source kani-dependencies to get CBMC_VIEWER_VERSION -source kani-dependencies - -if [ -z "${CBMC_VIEWER_VERSION:-}" ]; then - echo "$0: Error: CBMC_VIEWER_VERSION is not specified" - exit 1 -fi - -set -x - -python3 -m pip install cbmc-viewer==$CBMC_VIEWER_VERSION diff --git a/scripts/setup/macos/install_deps.sh b/scripts/setup/macos/install_deps.sh index 179bf8c1237f..112e34680b11 100755 --- a/scripts/setup/macos/install_deps.sh +++ b/scripts/setup/macos/install_deps.sh @@ -21,6 +21,5 @@ brew install universal-ctags wget jq SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" ${SCRIPT_DIR}/install_cbmc.sh -${SCRIPT_DIR}/install_viewer.sh # The Kissat installation script is platform-independent, so is placed one level up ${SCRIPT_DIR}/../install_kissat.sh diff --git a/scripts/setup/macos/install_viewer.sh b/scripts/setup/macos/install_viewer.sh deleted file mode 100755 index b55eca370d82..000000000000 --- a/scripts/setup/macos/install_viewer.sh +++ /dev/null @@ -1,25 +0,0 @@ -#!/bin/bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set -eu - -# Install cbmc-viewer - -# Source kani-dependencies to get CBMC_VIEWER_VERSION -source kani-dependencies - -if [ -z "${CBMC_VIEWER_VERSION:-}" ]; then - echo "$0: Error: CBMC_VIEWER_VERSION is not specified" - exit 1 -fi - -set -x - -# brew doesn't recognize specific versions of viewer -# Build from source, since there's only a macos-12 bottle which doesn't seem to work. -# Install Python 3.12 first while ignoring errors: the system may provide this -# version, which will hinder brew from installing symlinks -brew install python@3.12 || true -brew install -s aws/tap/cbmc-viewer -echo "Installed: $(cbmc-viewer --version)" diff --git a/scripts/setup/ubuntu/install_deps.sh b/scripts/setup/ubuntu/install_deps.sh index b93602691222..2633607744c5 100755 --- a/scripts/setup/ubuntu/install_deps.sh +++ b/scripts/setup/ubuntu/install_deps.sh @@ -57,6 +57,5 @@ fi SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" ${SCRIPT_DIR}/install_cbmc.sh -${SCRIPT_DIR}/install_viewer.sh # The Kissat installation script is platform-independent, so is placed one level up ${SCRIPT_DIR}/../install_kissat.sh diff --git a/scripts/setup/ubuntu/install_viewer.sh b/scripts/setup/ubuntu/install_viewer.sh deleted file mode 100755 index c8ba7b7b838e..000000000000 --- a/scripts/setup/ubuntu/install_viewer.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/bin/bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set -eu - -# Install cbmc-viewer - -# Source kani-dependencies to get CBMC_VIEWER_VERSION -source kani-dependencies - -if [ -z "${CBMC_VIEWER_VERSION:-}" ]; then - echo "$0: Error: CBMC_VIEWER_VERSION is not specified" - exit 1 -fi - -set -x - -python3 -m pip install cbmc-viewer==$CBMC_VIEWER_VERSION diff --git a/src/lib.rs b/src/lib.rs index f24163d3213c..5b79ec504d4c 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -140,7 +140,7 @@ fn exec(bin: &str) -> Result<()> { // Allow python scripts to find dependencies under our pyroot let pythonpath = prepend_search_path(&[pyroot], env::var_os("PYTHONPATH"))?; - // Add: kani, cbmc, viewer (pyroot), and our rust toolchain directly to our PATH + // Add: kani, cbmc, and our rust toolchain directly to our PATH let path = prepend_search_path(&[bin_kani, bin_pyroot], env::var_os("PATH"))?; // Ensure our environment variables for linker search paths won't cause failures, before we execute: diff --git a/src/setup.rs b/src/setup.rs index 0901de9a8b00..96daf82e4a27 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -86,8 +86,6 @@ pub fn setup( setup_rust_toolchain(&kani_dir, use_local_toolchain)?; - setup_python_deps(&kani_dir)?; - os_hacks::setup_os_hacks(&kani_dir, &os)?; println!("[5/5] Successfully completed Kani first-time setup."); @@ -183,23 +181,6 @@ fn setup_rust_toolchain(kani_dir: &Path, use_local_toolchain: Option) Ok(toolchain_version) } -/// Install into the pyroot the python dependencies we need -fn setup_python_deps(kani_dir: &Path) -> Result<()> { - println!("[4/5] Installing Kani python dependencies..."); - let pyroot = kani_dir.join("pyroot"); - - // TODO: this is a repetition of versions from kani/kani-dependencies - let pkg_versions = &["cbmc-viewer==3.10"]; - - Command::new("python3") - .args(["-m", "pip", "install", "--target"]) - .arg(&pyroot) - .args(pkg_versions) - .run()?; - - Ok(()) -} - // This ends the setup steps above. // // Just putting a bit of space between that and the helper functions below. diff --git a/tests/cargo-kani/rectangle-example/README.md b/tests/cargo-kani/rectangle-example/README.md index b07c61a96c9c..b16c1d464881 100644 --- a/tests/cargo-kani/rectangle-example/README.md +++ b/tests/cargo-kani/rectangle-example/README.md @@ -31,17 +31,14 @@ $ cargo kani --harness stretched_rectangle_can_hold_original --output-format ter VERIFICATION:- FAILED ``` -In order to view a trace (a step-by-step execution of the program) use the `--visualize` flag: +In order to view a counterexample use the `--concrete-playback` flag: ```bash -$ cargo kani --harness stretched_rectangle_can_hold_original --output-format terse --visualize +$ cargo kani --harness stretched_rectangle_can_hold_original --output-format terse -Zconcrete-playback --concrete-playback=print # --snip-- VERIFICATION:- FAILED -# and generates a html report in target/report/html/index.html ``` -And open the report in a browser. - After fixing the problem we can re-run Kani (on the proof harness `stretched_rectangle_can_hold_original_fixed`). This time we expect verification success: ```bash diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/see b/tests/expected/function-contract/interior-mutability/whole-struct/see new file mode 100644 index 000000000000..70b23cd1cc9c --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/see @@ -0,0 +1,997 @@ +Kani Rust Verifier 0.56.0 (standalone) +warning: Found the following unsupported constructs: + - caller_location (1) + - foreign function (1) + + Verification will fail if one or more of these constructs is reachable. + See https://model-checking.github.io/kani/rust-feature-support.html for more details. + +warning: 1 warning emitted + +Checking harness harness_for_modify... +CBMC 6.3.1 (cbmc-6.3.1) +CBMC version 6.3.1 (cbmc-6.3.1) 64-bit x86_64 linux +Reading GOTO program from file /home/ubuntu/git/kani/tests/expected/function-contract/interior-mutability/whole-struct/refcell__RNvCsfAnD8LB58jB_7refcell18harness_for_modify.out +Generating GOTO Program +Adding CPROVER library (x86_64) +Removal of function pointers and virtual functions +Generic Property Instrumentation +Running with 16 object bits, 48 offset bits (user-specified) +Starting Bounded Model Checking +Runtime Symex: 0.0773892s +size of program expression: 2181 steps +slicing removed 1354 assignments +Generated 195 VCC(s), 37 remaining after simplification +Runtime Postprocess Equation: 0.000353808s +Passing problem to propositional reduction +converting SSA +Runtime Convert SSA: 19.0731s +Running propositional reduction +Post-processing +Runtime Post-process: 6.2e-06s +Solving with CaDiCaL 2.0.0 +16918466 variables, 42087481 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 4.70032s +Runtime decision procedure: 23.9866s +Running propositional reduction +Solving with CaDiCaL 2.0.0 +16918467 variables, 42087482 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 0.645725s +Runtime decision procedure: 0.860385s +Running propositional reduction +Solving with CaDiCaL 2.0.0 +16918468 variables, 42087483 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 0.643113s +Runtime decision procedure: 0.859491s +Running propositional reduction +Solving with CaDiCaL 2.0.0 +16918469 variables, 42087484 clauses +SAT checker: instance is UNSATISFIABLE +Runtime Solver: 0.000550312s +Runtime decision procedure: 0.175352s + +RESULTS: +Check 1: as std::ops::Drop>::drop.assertion.1 + - Status: SUCCESS + - Description: "attempt to add with overflow" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1807:25 in function as std::ops::Drop>::drop + +Check 2: __CPROVER_contracts_car_set_insert.assertion.1 + - Status: SUCCESS + - Description: "ptr NULL or writable up to size" + - Location: :161 in function __CPROVER_contracts_car_set_insert + +Check 3: __CPROVER_contracts_car_set_insert.assertion.2 + - Status: SUCCESS + - Description: "CAR size is less than __CPROVER_max_malloc_size" + - Location: :164 in function __CPROVER_contracts_car_set_insert + +Check 4: __CPROVER_contracts_car_set_insert.assertion.3 + - Status: SUCCESS + - Description: "no offset bits overflow on CAR upper bound computation" + - Location: :168 in function __CPROVER_contracts_car_set_insert + +Check 5: __CPROVER_contracts_write_set_check_assignment.assertion.1 + - Status: SUCCESS + - Description: "ptr NULL or writable up to size" + - Location: :775 in function __CPROVER_contracts_write_set_check_assignment + +Check 6: __CPROVER_contracts_write_set_check_assignment.assertion.2 + - Status: SUCCESS + - Description: "CAR size is less than __CPROVER_max_malloc_size" + - Location: :792 in function __CPROVER_contracts_write_set_check_assignment + +Check 7: __CPROVER_contracts_write_set_check_assignment.assertion.3 + - Status: SUCCESS + - Description: "no offset bits overflow on CAR upper bound computation" + - Location: :798 in function __CPROVER_contracts_write_set_check_assignment + +Check 8: __CPROVER_contracts_write_set_check_assignment.unwind.1 + - Status: SUCCESS + - Description: "unwinding assertion loop 0" + - Location: :807 in function __CPROVER_contracts_write_set_check_assignment + +Check 9: std::rt::panic_fmt.unsupported_construct.1 + - Status: SUCCESS + - Description: "call to foreign "Rust" function `rust_begin_unwind` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panicking.rs:63:9 in function std::rt::panic_fmt + +Check 10: modify::{closure#3}.assertion.1 + - Status: SUCCESS + - Description: "misaligned pointer dereference: address must be a multiple of its type's alignment" + - Location: refcell.rs:13:25 in function modify::{closure#3} + +Check 11: modify::{closure#3}.assertion.2 + - Status: SUCCESS + - Description: "|_| unsafe{ *im.x.as_ptr() } < 101" + - Location: refcell.rs:15:1 in function modify::{closure#3} + +Check 12: __CPROVER_contracts_write_set_record_deallocated.unwind.1 + - Status: SUCCESS + - Description: "unwinding assertion loop 0" + - Location: :710 in function __CPROVER_contracts_write_set_record_deallocated + +Check 13: modify::{closure#1}.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: refcell.rs:13:1 in function modify::{closure#1} + +Check 14: std::ptr::write::.assigns.1 + - Status: SUCCESS + - Description: "Check that *dst is assignable" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 15: modify::{closure#0}.assertion.1 + - Status: UNREACHABLE + - Description: "attempt to add with overflow" + - Location: refcell.rs:18:34 in function modify::{closure#0} + +Check 16: refcell::modify::{closure#3}::{closure#1}.single_top_level_call.1 + - Status: SUCCESS + - Description: "Only a single top-level call to function _RNCNCNvCsfAnD8LB58jB_7refcell6modifys1_0s_0B5_ when checking contract _RNCNCNvCsfAnD8LB58jB_7refcell6modifys1_0s_0B5_" + - Location: refcell.rs:14:1 in function refcell::modify::{closure#3}::{closure#1} + +Check 17: refcell::modify::{closure#3}::{closure#1}.no_alloc_dealloc_in_requires.1 + - Status: SUCCESS + - Description: "Check that requires do not allocate or deallocate memory" + - Location: refcell.rs:14:1 in function refcell::modify::{closure#3}::{closure#1} + +Check 18: refcell::modify::{closure#3}::{closure#1}.no_alloc_dealloc_in_ensures.1 + - Status: SUCCESS + - Description: "Check that ensures do not allocate or deallocate memory" + - Location: refcell.rs:14:1 in function refcell::modify::{closure#3}::{closure#1} + +Check 19: refcell::modify::{closure#3}::{closure#1}.no_recursive_call.1 + - Status: SUCCESS + - Description: "No recursive call to function _RNCNCNvCsfAnD8LB58jB_7refcell6modifys1_0s_0B5_ when checking contract _RNCNCNvCsfAnD8LB58jB_7refcell6modifys1_0s_0B5_" + - Location: refcell.rs:14:1 in function refcell::modify::{closure#3}::{closure#1} + +Check 20: free.frees.1 + - Status: SUCCESS + - Description: "Check that ptr is freeable" + - Location: :43 in function free + +Check 21: std::ptr::NonNull::::as_mut::<'_>.safety_check.1 + - Status: SUCCESS + - Description: "misaligned pointer to reference cast: address must be a multiple of its type's alignment" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs:421:18 in function std::ptr::NonNull::::as_mut::<'_> + +Check 22: std::ptr::NonNull::::as_mut::<'_>.safety_check.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs:421:18 in function std::ptr::NonNull::::as_mut::<'_> + +Check 23: std::fmt::Arguments::<'_>::new_const::<1>.assigns.1 + - Status: SUCCESS + - Description: "Check that *((unsigned char **)&temp_0) is assignable" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs:339:34 in function std::fmt::Arguments::<'_>::new_const::<1> + +Check 24: std::ptr::drop_in_place::>.safety_check.1 + - Status: SUCCESS + - Description: "misaligned pointer to reference cast: address must be a multiple of its type's alignment" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:574:1 in function std::ptr::drop_in_place::> + +Check 25: std::ptr::drop_in_place::>.safety_check.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:574:1 in function std::ptr::drop_in_place::> + +Check 26: std::cell::BorrowRefMut::<'_>::new.assigns.1 + - Status: SUCCESS + - Description: "Check that *((unsigned char **)&temp_0) is assignable" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1823:18 in function std::cell::BorrowRefMut::<'_>::new + +Check 27: std::cell::BorrowRefMut::<'_>::new.assertion.1 + - Status: SUCCESS + - Description: "attempt to subtract with overflow" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1820:28 in function std::cell::BorrowRefMut::<'_>::new + +Check 28: std::cell::Cell::::replace.safety_check.1 + - Status: SUCCESS + - Description: "misaligned pointer to reference cast: address must be a multiple of its type's alignment" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:502:31 in function std::cell::Cell::::replace + +Check 29: std::cell::Cell::::replace.safety_check.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:502:31 in function std::cell::Cell::::replace + +Check 30: modify::{closure#2}.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: refcell.rs:13:1 in function modify::{closure#2} + +Check 31: modify::{closure#3}::{closure#0}.assertion.1 + - Status: SUCCESS + - Description: "misaligned pointer dereference: address must be a multiple of its type's alignment" + - Location: refcell.rs:15:28 in function modify::{closure#3}::{closure#0} + +Check 32: std::fmt::Arguments::<'_>::new_v1::<1, 1>.assigns.1 + - Status: SUCCESS + - Description: "Check that *((unsigned char **)&temp_0) is assignable" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs:350:34 in function std::fmt::Arguments::<'_>::new_v1::<1, 1> + +Check 33: modify::{closure#3}::{closure#1}::{closure#0}.assertion.1 + - Status: SUCCESS + - Description: "attempt to add with overflow" + - Location: refcell.rs:18:34 in function modify::{closure#3}::{closure#1}::{closure#0} + +Check 34: std::cell::panic_already_borrowed.assertion.1 + - Status: SUCCESS + - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:796:5 in function std::cell::panic_already_borrowed + +Check 35: std::cell::RefCell::::borrow_mut.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1086:15 in function std::cell::RefCell::::borrow_mut + +Check 36: std::panic::Location::<'_>::caller.unsupported_construct.1 + - Status: SUCCESS + - Description: "caller_location is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/374" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/panic/location.rs:89:9 in function std::panic::Location::<'_>::caller + +Check 37: std::ptr::write::.assigns.1 + - Status: SUCCESS + - Description: "Check that *dst is assignable" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 38: std::cell::RefCell::::try_borrow_mut.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1118:15 in function std::cell::RefCell::::try_borrow_mut + +Check 39: std::cell::RefCell::::try_borrow_mut.assigns.1 + - Status: SUCCESS + - Description: "Check that *((unsigned char **)&temp_1) is assignable" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1129:21 in function std::cell::RefCell::::try_borrow_mut + +Check 40: __CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.1 + - Status: SUCCESS + - Description: "count leading zeros is undefined for value zero" + - Location: :251 in function __CPROVER_contracts_obj_set_create_indexed_by_object_id + +Check 41: __CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.2 + - Status: SUCCESS + - Description: "count leading zeros is undefined for value zero" + - Location: :251 in function __CPROVER_contracts_obj_set_create_indexed_by_object_id + +Check 42: __CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.3 + - Status: SUCCESS + - Description: "count leading zeros is undefined for value zero" + - Location: :251 in function __CPROVER_contracts_obj_set_create_indexed_by_object_id + +Check 43: __CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.4 + - Status: SUCCESS + - Description: "count leading zeros is undefined for value zero" + - Location: :251 in function __CPROVER_contracts_obj_set_create_indexed_by_object_id + +Check 44: std::fmt::Arguments::<'_>::new_const::<1>.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs:339:34 in function std::fmt::Arguments::<'_>::new_const::<1> + +Check 45: std::ptr::NonNull::::as_mut::<'_>.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs:421:24 in function std::ptr::NonNull::::as_mut::<'_> + +Check 46: std::ptr::NonNull::::as_mut::<'_>.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs:421:24 in function std::ptr::NonNull::::as_mut::<'_> + +Check 47: std::ptr::NonNull::::as_mut::<'_>.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs:421:24 in function std::ptr::NonNull::::as_mut::<'_> + +Check 48: std::ptr::NonNull::::as_mut::<'_>.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs:421:24 in function std::ptr::NonNull::::as_mut::<'_> + +Check 49: std::ptr::NonNull::::as_mut::<'_>.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs:421:24 in function std::ptr::NonNull::::as_mut::<'_> + +Check 50: std::ptr::NonNull::::as_mut::<'_>.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs:421:24 in function std::ptr::NonNull::::as_mut::<'_> + +Check 51: modify::{closure#0}.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:18:29 in function modify::{closure#0} + +Check 52: modify::{closure#0}.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:18:29 in function modify::{closure#0} + +Check 53: modify::{closure#0}.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:18:29 in function modify::{closure#0} + +Check 54: modify::{closure#0}.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:18:29 in function modify::{closure#0} + +Check 55: modify::{closure#0}.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:18:29 in function modify::{closure#0} + +Check 56: modify::{closure#0}.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:18:29 in function modify::{closure#0} + +Check 57: std::ptr::write::.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 58: std::ptr::write::.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 59: std::ptr::write::.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 60: std::ptr::write::.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 61: std::ptr::write::.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 62: std::ptr::write::.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 63: as std::ops::Drop>::drop.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1805:22 in function as std::ops::Drop>::drop + +Check 64: as std::ops::Drop>::drop.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1805:22 in function as std::ops::Drop>::drop + +Check 65: as std::ops::Drop>::drop.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1805:22 in function as std::ops::Drop>::drop + +Check 66: as std::ops::Drop>::drop.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1805:22 in function as std::ops::Drop>::drop + +Check 67: as std::ops::Drop>::drop.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1805:22 in function as std::ops::Drop>::drop + +Check 68: as std::ops::Drop>::drop.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1805:22 in function as std::ops::Drop>::drop + +Check 69: as std::ops::Drop>::drop.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1807:9 in function as std::ops::Drop>::drop + +Check 70: as std::ops::Drop>::drop.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1807:9 in function as std::ops::Drop>::drop + +Check 71: as std::ops::Drop>::drop.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1807:9 in function as std::ops::Drop>::drop + +Check 72: as std::ops::Drop>::drop.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1807:9 in function as std::ops::Drop>::drop + +Check 73: as std::ops::Drop>::drop.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1807:9 in function as std::ops::Drop>::drop + +Check 74: as std::ops::Drop>::drop.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1807:9 in function as std::ops::Drop>::drop + +Check 75: std::ptr::read::.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1438:9 in function std::ptr::read:: + +Check 76: std::ptr::read::.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1438:9 in function std::ptr::read:: + +Check 77: std::ptr::read::.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1438:9 in function std::ptr::read:: + +Check 78: std::ptr::read::.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1438:9 in function std::ptr::read:: + +Check 79: std::ptr::read::.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1438:9 in function std::ptr::read:: + +Check 80: std::ptr::read::.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1438:9 in function std::ptr::read:: + +Check 81: modify::{closure#3}::{closure#0}.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:15:29 in function modify::{closure#3}::{closure#0} + +Check 82: modify::{closure#3}::{closure#0}.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:15:29 in function modify::{closure#3}::{closure#0} + +Check 83: modify::{closure#3}::{closure#0}.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:15:29 in function modify::{closure#3}::{closure#0} + +Check 84: modify::{closure#3}::{closure#0}.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:15:29 in function modify::{closure#3}::{closure#0} + +Check 85: modify::{closure#3}::{closure#0}.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:15:29 in function modify::{closure#3}::{closure#0} + +Check 86: modify::{closure#3}::{closure#0}.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:15:29 in function modify::{closure#3}::{closure#0} + +Check 87: modify::{closure#3}::{closure#0}.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:15:29 in function modify::{closure#3}::{closure#0} + +Check 88: modify::{closure#3}::{closure#0}.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:15:29 in function modify::{closure#3}::{closure#0} + +Check 89: modify::{closure#3}::{closure#0}.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:15:29 in function modify::{closure#3}::{closure#0} + +Check 90: modify::{closure#3}::{closure#0}.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:15:29 in function modify::{closure#3}::{closure#0} + +Check 91: modify::{closure#3}::{closure#0}.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:15:29 in function modify::{closure#3}::{closure#0} + +Check 92: modify::{closure#3}::{closure#0}.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:15:29 in function modify::{closure#3}::{closure#0} + +Check 93: modify::{closure#3}::{closure#0}.pointer_dereference.13 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:15:28 in function modify::{closure#3}::{closure#0} + +Check 94: modify::{closure#3}::{closure#0}.pointer_dereference.14 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:15:28 in function modify::{closure#3}::{closure#0} + +Check 95: modify::{closure#3}::{closure#0}.pointer_dereference.15 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:15:28 in function modify::{closure#3}::{closure#0} + +Check 96: modify::{closure#3}::{closure#0}.pointer_dereference.16 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:15:28 in function modify::{closure#3}::{closure#0} + +Check 97: modify::{closure#3}::{closure#0}.pointer_dereference.17 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:15:28 in function modify::{closure#3}::{closure#0} + +Check 98: modify::{closure#3}::{closure#0}.pointer_dereference.18 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:15:28 in function modify::{closure#3}::{closure#0} + +Check 99: harness_for_modify.precondition_instance.1 + - Status: SUCCESS + - Description: "free argument must be NULL or valid pointer" + - Location: refcell.rs:21:1 in function harness_for_modify + +Check 100: harness_for_modify.precondition_instance.2 + - Status: SUCCESS + - Description: "free argument must be dynamic object" + - Location: refcell.rs:21:1 in function harness_for_modify + +Check 101: harness_for_modify.precondition_instance.3 + - Status: SUCCESS + - Description: "free argument has offset zero" + - Location: refcell.rs:21:1 in function harness_for_modify + +Check 102: harness_for_modify.precondition_instance.4 + - Status: SUCCESS + - Description: "double free" + - Location: refcell.rs:21:1 in function harness_for_modify + +Check 103: harness_for_modify.precondition_instance.5 + - Status: SUCCESS + - Description: "free called for new[] object" + - Location: refcell.rs:21:1 in function harness_for_modify + +Check 104: harness_for_modify.precondition_instance.6 + - Status: SUCCESS + - Description: "free called for stack-allocated object" + - Location: refcell.rs:21:1 in function harness_for_modify + +Check 105: modify::{closure#3}.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:13:26 in function modify::{closure#3} + +Check 106: modify::{closure#3}.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:13:26 in function modify::{closure#3} + +Check 107: modify::{closure#3}.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:13:26 in function modify::{closure#3} + +Check 108: modify::{closure#3}.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:13:26 in function modify::{closure#3} + +Check 109: modify::{closure#3}.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:13:26 in function modify::{closure#3} + +Check 110: modify::{closure#3}.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:13:26 in function modify::{closure#3} + +Check 111: modify::{closure#3}.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:13:26 in function modify::{closure#3} + +Check 112: modify::{closure#3}.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:13:26 in function modify::{closure#3} + +Check 113: modify::{closure#3}.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:13:26 in function modify::{closure#3} + +Check 114: modify::{closure#3}.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:13:26 in function modify::{closure#3} + +Check 115: modify::{closure#3}.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:13:26 in function modify::{closure#3} + +Check 116: modify::{closure#3}.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:13:26 in function modify::{closure#3} + +Check 117: modify::{closure#3}.pointer_dereference.13 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:13:25 in function modify::{closure#3} + +Check 118: modify::{closure#3}.pointer_dereference.14 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:13:25 in function modify::{closure#3} + +Check 119: modify::{closure#3}.pointer_dereference.15 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:13:25 in function modify::{closure#3} + +Check 120: modify::{closure#3}.pointer_dereference.16 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:13:25 in function modify::{closure#3} + +Check 121: modify::{closure#3}.pointer_dereference.17 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:13:25 in function modify::{closure#3} + +Check 122: modify::{closure#3}.pointer_dereference.18 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:13:25 in function modify::{closure#3} + +Check 123: modify::{closure#3}.pointer_dereference.19 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:14:18 in function modify::{closure#3} + +Check 124: modify::{closure#3}.pointer_dereference.20 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:14:18 in function modify::{closure#3} + +Check 125: modify::{closure#3}.pointer_dereference.21 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:14:18 in function modify::{closure#3} + +Check 126: modify::{closure#3}.pointer_dereference.22 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:14:18 in function modify::{closure#3} + +Check 127: modify::{closure#3}.pointer_dereference.23 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:14:18 in function modify::{closure#3} + +Check 128: modify::{closure#3}.pointer_dereference.24 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:14:18 in function modify::{closure#3} + +Check 129: modify::{closure#3}.pointer_dereference.25 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:14:18 in function modify::{closure#3} + +Check 130: modify::{closure#3}.pointer_dereference.26 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:14:18 in function modify::{closure#3} + +Check 131: modify::{closure#3}.pointer_dereference.27 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:14:18 in function modify::{closure#3} + +Check 132: modify::{closure#3}.pointer_dereference.28 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:14:18 in function modify::{closure#3} + +Check 133: modify::{closure#3}.pointer_dereference.29 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:14:18 in function modify::{closure#3} + +Check 134: modify::{closure#3}.pointer_dereference.30 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:14:18 in function modify::{closure#3} + +Check 135: modify::{closure#3}.pointer_dereference.31 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:14:1 in function modify::{closure#3} + +Check 136: modify::{closure#3}.pointer_dereference.32 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:14:1 in function modify::{closure#3} + +Check 137: modify::{closure#3}.pointer_dereference.33 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:14:1 in function modify::{closure#3} + +Check 138: modify::{closure#3}.pointer_dereference.34 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:14:1 in function modify::{closure#3} + +Check 139: modify::{closure#3}.pointer_dereference.35 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:14:1 in function modify::{closure#3} + +Check 140: modify::{closure#3}.pointer_dereference.36 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:14:1 in function modify::{closure#3} + +Check 141: modify::{closure#3}.pointer_dereference.37 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:14:1 in function modify::{closure#3} + +Check 142: modify::{closure#3}.pointer_dereference.38 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:15:17 in function modify::{closure#3} + +Check 143: modify::{closure#3}.pointer_dereference.39 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:15:17 in function modify::{closure#3} + +Check 144: modify::{closure#3}.pointer_dereference.40 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:15:17 in function modify::{closure#3} + +Check 145: modify::{closure#3}.pointer_dereference.41 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:15:17 in function modify::{closure#3} + +Check 146: modify::{closure#3}.pointer_dereference.42 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:15:17 in function modify::{closure#3} + +Check 147: modify::{closure#3}.pointer_dereference.43 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:15:17 in function modify::{closure#3} + +Check 148: std::cell::BorrowRefMut::<'_>::new.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1823:18 in function std::cell::BorrowRefMut::<'_>::new + +Check 149: modify::{closure#3}::{closure#1}::{closure#0}.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:18:29 in function modify::{closure#3}::{closure#1}::{closure#0} + +Check 150: modify::{closure#3}::{closure#1}::{closure#0}.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:18:29 in function modify::{closure#3}::{closure#1}::{closure#0} + +Check 151: modify::{closure#3}::{closure#1}::{closure#0}.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:18:29 in function modify::{closure#3}::{closure#1}::{closure#0} + +Check 152: modify::{closure#3}::{closure#1}::{closure#0}.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:18:29 in function modify::{closure#3}::{closure#1}::{closure#0} + +Check 153: modify::{closure#3}::{closure#1}::{closure#0}.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:18:29 in function modify::{closure#3}::{closure#1}::{closure#0} + +Check 154: modify::{closure#3}::{closure#1}::{closure#0}.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:18:29 in function modify::{closure#3}::{closure#1}::{closure#0} + +Check 155: modify::{closure#3}::{closure#1}.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: refcell.rs:18:5 in function modify::{closure#3}::{closure#1} + +Check 156: modify::{closure#3}::{closure#1}.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: refcell.rs:18:5 in function modify::{closure#3}::{closure#1} + +Check 157: modify::{closure#3}::{closure#1}.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: refcell.rs:18:5 in function modify::{closure#3}::{closure#1} + +Check 158: modify::{closure#3}::{closure#1}.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: refcell.rs:18:5 in function modify::{closure#3}::{closure#1} + +Check 159: modify::{closure#3}::{closure#1}.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: refcell.rs:18:5 in function modify::{closure#3}::{closure#1} + +Check 160: modify::{closure#3}::{closure#1}.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: refcell.rs:18:5 in function modify::{closure#3}::{closure#1} + +Check 161: std::fmt::Arguments::<'_>::new_v1::<1, 1>.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs:350:34 in function std::fmt::Arguments::<'_>::new_v1::<1, 1> + +Check 162: std::cell::Cell::::get.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:543:18 in function std::cell::Cell::::get + +Check 163: std::cell::Cell::::get.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:543:18 in function std::cell::Cell::::get + +Check 164: std::cell::Cell::::get.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:543:18 in function std::cell::Cell::::get + +Check 165: std::cell::Cell::::get.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:543:18 in function std::cell::Cell::::get + +Check 166: std::cell::Cell::::get.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:543:18 in function std::cell::Cell::::get + +Check 167: std::cell::Cell::::get.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:543:18 in function std::cell::Cell::::get + +Check 168: std::ptr::read::.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1438:9 in function std::ptr::read:: + +Check 169: std::ptr::read::.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1438:9 in function std::ptr::read:: + +Check 170: std::ptr::read::.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1438:9 in function std::ptr::read:: + +Check 171: std::ptr::read::.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1438:9 in function std::ptr::read:: + +Check 172: std::ptr::read::.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1438:9 in function std::ptr::read:: + +Check 173: std::ptr::read::.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1438:9 in function std::ptr::read:: + +Check 174: std::cell::RefCell::::borrow_mut.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1086:15 in function std::cell::RefCell::::borrow_mut + +Check 175: std::ptr::write::.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 176: std::ptr::write::.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 177: std::ptr::write::.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 178: std::ptr::write::.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 179: std::ptr::write::.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 180: std::ptr::write::.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:1643:9 in function std::ptr::write:: + +Check 181: std::cell::RefCell::::try_borrow_mut.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1118:15 in function std::cell::RefCell::::try_borrow_mut + +Check 182: std::cell::RefCell::::try_borrow_mut.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../../../.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:1129:21 in function std::cell::RefCell::::try_borrow_mut + + +SUMMARY: + ** 0 of 182 failed (1 unreachable) + +VERIFICATION:- SUCCESSFUL +Verification Time: 30.182495s + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. + Command being timed: "kani refcell.rs -Zfunction-contracts" + User time (seconds): 25.33 + System time (seconds): 8.08 + Percent of CPU this job got: 101% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:33.07 + Average shared text size (kbytes): 0 + Average unshared data size (kbytes): 0 + Average stack size (kbytes): 0 + Average total size (kbytes): 0 + Maximum resident set size (kbytes): 9200340 + Average resident set size (kbytes): 0 + Major (requiring I/O) page faults: 0 + Minor (reclaiming a frame) page faults: 3457986 + Voluntary context switches: 1824 + Involuntary context switches: 99 + Swaps: 0 + File system inputs: 0 + File system outputs: 5496 + Socket messages sent: 0 + Socket messages received: 0 + Signals delivered: 0 + Page size (bytes): 4096 + Exit status: 0 diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/see2 b/tests/expected/function-contract/interior-mutability/whole-struct/see2 new file mode 100644 index 000000000000..9dd5f9224749 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/see2 @@ -0,0 +1,43 @@ +Kani Rust Verifier 0.56.0 (standalone) +error[E0369]: cannot add `{integer}` to `std::cell::RefCell` + --> refcell.rs:20:28 + | +20 | im.x.replace(old_value + 1); + | --------- ^ - {integer} + | | + | std::cell::RefCell + | +note: the foreign item type `std::cell::RefCell` doesn't implement `std::ops::Add<{integer}>` + --> /home/ubuntu/.rustup/toolchains/nightly-2024-10-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cell.rs:726:1 + | +726 | pub struct RefCell { + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ not implement `std::ops::Add<{integer}>` + +error: aborting due to 1 previous error + +For more information about this error, try `rustc --explain E0369`. +error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 101 +Command exited with non-zero status 1 + Command being timed: "kani refcell.rs -Zfunction-contracts" + User time (seconds): 0.02 + System time (seconds): 0.05 + Percent of CPU this job got: 69% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.11 + Average shared text size (kbytes): 0 + Average unshared data size (kbytes): 0 + Average stack size (kbytes): 0 + Average total size (kbytes): 0 + Maximum resident set size (kbytes): 102168 + Average resident set size (kbytes): 0 + Major (requiring I/O) page faults: 40 + Minor (reclaiming a frame) page faults: 6296 + Voluntary context switches: 56 + Involuntary context switches: 0 + Swaps: 0 + File system inputs: 8960 + File system outputs: 8 + Socket messages sent: 0 + Socket messages received: 0 + Signals delivered: 0 + Page size (bytes): 4096 + Exit status: 1 diff --git a/tests/expected/llbc/basic0/TestRNvCs5jAuZAZg7Qa4test4main.symtab.lean b/tests/expected/llbc/basic0/TestRNvCs5jAuZAZg7Qa4test4main.symtab.lean new file mode 100644 index 000000000000..ed03fe8e7351 --- /dev/null +++ b/tests/expected/llbc/basic0/TestRNvCs5jAuZAZg7Qa4test4main.symtab.lean @@ -0,0 +1,23 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [test] +import Base +open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false + +namespace test + +/- [test::is_zero]: + Source: 'test.rs', lines 8:1-8:27 -/ +def is_zero (i : I32) : Result Bool := + Result.ok (i = 0#i32) + +/- [test::main]: + Source: 'test.rs', lines 13:1-13:10 -/ +def main : Result Unit := + do + let _ ← is_zero 0#i32 + Result.ok () + +end test diff --git a/tests/expected/llbc/basic0/see1 b/tests/expected/llbc/basic0/see1 new file mode 100644 index 000000000000..c68d33291c81 --- /dev/null +++ b/tests/expected/llbc/basic0/see1 @@ -0,0 +1,75 @@ +Kani Rust Verifier 0.56.0 (standalone) +2024-11-05T21:46:17.513907Z DEBUG kani_driver::project: build compile krate="test" input="test.rs" rlib_path="/home/ubuntu/git/kani/tests/expected/llbc/basic0/libtest.rlib" +[Kani] Running: `/home/ubuntu/git/kani/target/kani/bin/kani-compiler "-Cllvm-args=--check-version=0.56.0 --log-level=debug --assertion-reach-checks -Z lean --reachability=harnesses --backend=llbc" -C overflow-checks=on -Z unstable-options -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -Z always-encode-mir --cfg=kani -Z crate-attr=feature(register_tool) -Z crate-attr=register_tool(kanitool) --sysroot /home/ubuntu/git/kani/target/kani -L /home/ubuntu/git/kani/target/kani/lib --extern kani --extern noprelude:std=/home/ubuntu/git/kani/target/kani/lib/libstd.rlib -C panic=abort -C symbol-mangling-version=v0 -Z panic_abort_tests=yes -Z mir-enable-passes=-RemoveStorageMarkers --check-cfg=cfg(kani) --kani-compiler test.rs --out-dir /home/ubuntu/git/kani/tests/expected/llbc/basic0 --crate-name test --crate-type lib` +DEBUG kani_compiler::kani_compiler config end, queries=QueryDb { args: Some(Arguments { check_assertion_reachability: true, check_coverage: false, emit_vtable_restrictions: false, output_pretty_json: false, ignore_global_asm: false, write_json_symtab: false, reachability_analysis: Harnesses, stubbing_enabled: false, unstable_features: ["lean"], build_std: false, log_level: Some(Directive { in_span: None, fields: [], target: None, level: LevelFilter::DEBUG }), json_output: false, color_output: false, check_version: Some("0.56.0"), ub_check: [], backend: Llbc, print_llbc: false }) } +DEBUG kani_compiler::kani_middle::provide run_mir_passes, def_id=DefId(0:3 ~ test[3deb]::is_zero) +DEBUG kani_compiler::kani_middle::provide Run Kani transformation passes, def_id=DefId(0:3 ~ test[3deb]::is_zero) +DEBUG kani_compiler::kani_middle::provide run_mir_passes, def_id=DefId(0:4 ~ test[3deb]::main) +DEBUG kani_compiler::kani_middle::provide Run Kani transformation passes, def_id=DefId(0:4 ~ test[3deb]::main) +DEBUG kani_compiler::kani_middle::codegen_units CodegenUnits::new, units=[CodegenUnit { harnesses: [Instance { kind: Item, def: "_RNvCs5jAuZAZg7Qa_4test4main", args: GenericArgs([]) }], stubs: {} }] +DEBUG kani_compiler::kani_middle::reachability collect, root=Fn(Instance { kind: Item, def: "_RNvCs5jAuZAZg7Qa_4test4main", args: GenericArgs([]) }) +┐kani_compiler::kani_middle::reachability::visit_fn function=Instance { kind: Item, def: "_RNvCs5jAuZAZg7Qa_4test4main", args: GenericArgs([]) } +├─── DEBUG kani_compiler::kani_middle::reachability visit_constant, constant=ConstOperand { span: Span { id: 0, repr: "test.rs:14:13: 14:20" }, user_ty: None, const_: MirConst { kind: ZeroSized, ty: Ty { id: 0, kind: RigidTy(FnDef(FnDef(DefId { id: 0, name: "is_zero" }), GenericArgs([]))) }, id: MirConstId(0) } }, location=Location(Span { id: 2, repr: "test.rs:14:13: 14:23" }), literal=MirConst { kind: ZeroSized, ty: Ty { id: 0, kind: RigidTy(FnDef(FnDef(DefId { id: 0, name: "is_zero" }), GenericArgs([]))) }, id: MirConstId(0) } +├─── DEBUG kani_compiler::kani_middle::reachability visit_constant, constant=ConstOperand { span: Span { id: 1, repr: "test.rs:14:21: 14:22" }, user_ty: None, const_: MirConst { kind: Allocated(Allocation { bytes: [Some(0), Some(0), Some(0), Some(0)], provenance: ProvenanceMap { ptrs: [] }, align: 4, mutability: Mut }), ty: Ty { id: 1, kind: RigidTy(Int(I32)) }, id: MirConstId(1) } }, location=Location(Span { id: 2, repr: "test.rs:14:13: 14:23" }), literal=MirConst { kind: Allocated(Allocation { bytes: [Some(0), Some(0), Some(0), Some(0)], provenance: ProvenanceMap { ptrs: [] }, align: 4, mutability: Mut }), ty: Ty { id: 1, kind: RigidTy(Int(I32)) }, id: MirConstId(1) } +├─── DEBUG kani_compiler::kani_middle::reachability collect_allocation, alloc=Allocation { bytes: [Some(0), Some(0), Some(0), Some(0)], provenance: ProvenanceMap { ptrs: [] }, align: 4, mutability: Mut } +┘kani_compiler::kani_middle::reachability::visit_fn function=Instance { kind: Item, def: "_RNvCs5jAuZAZg7Qa_4test4main", args: GenericArgs([]) } +┐kani_compiler::kani_middle::reachability::visit_fn function=Instance { kind: Item, def: "_RNvCs5jAuZAZg7Qa_4test7is_zero", args: GenericArgs([]) } +├─── DEBUG kani_compiler::kani_middle::reachability visit_constant, constant=ConstOperand { span: Span { id: 8, repr: "test.rs:9:10: 9:11" }, user_ty: None, const_: MirConst { kind: Allocated(Allocation { bytes: [Some(0), Some(0), Some(0), Some(0)], provenance: ProvenanceMap { ptrs: [] }, align: 4, mutability: Mut }), ty: Ty { id: 1, kind: RigidTy(Int(I32)) }, id: MirConstId(1) } }, location=Location(Span { id: 9, repr: "test.rs:9:5: 9:11" }), literal=MirConst { kind: Allocated(Allocation { bytes: [Some(0), Some(0), Some(0), Some(0)], provenance: ProvenanceMap { ptrs: [] }, align: 4, mutability: Mut }), ty: Ty { id: 1, kind: RigidTy(Int(I32)) }, id: MirConstId(1) } +├─── DEBUG kani_compiler::kani_middle::reachability collect_allocation, alloc=Allocation { bytes: [Some(0), Some(0), Some(0), Some(0)], provenance: ProvenanceMap { ptrs: [] }, align: 4, mutability: Mut } +┘kani_compiler::kani_middle::reachability::visit_fn function=Instance { kind: Item, def: "_RNvCs5jAuZAZg7Qa_4test7is_zero", args: GenericArgs([]) } +INFO kani_compiler::codegen_aeneas_llbc::compiler_interface Finished codegen reachability analysis in 0.000655156s +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc register_fun_decl_id: DefId { id: 0, name: "is_zero" } +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc ***Not found! +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc register_fun_decl_id: {DefId { id: 0, name: "is_zero" }: Fun(0)} +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc fn_typ, idx=0, arg_abi=ArgAbi { ty: Ty { id: 1, kind: RigidTy(Int(I32)) }, layout: Layout(0), mode: Direct(ArgAttributes { regular: NoUndef, arg_ext: None, pointee_size: Size(0 bytes), pointee_align: None }) } +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc translate_rigid_ty: Int(I32) +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc function_type, args=[Ty(HashConsed(Literal(Integer(I32))))], fn_abi=FnAbi { args: [ArgAbi { ty: Ty { id: 1, kind: RigidTy(Int(I32)) }, layout: Layout(0), mode: Direct(ArgAttributes { regular: NoUndef, arg_ext: None, pointee_size: Size(0 bytes), pointee_align: None }) }], ret: ArgAbi { ty: Ty { id: 3, kind: RigidTy(Bool) }, layout: Layout(1), mode: Direct(ArgAttributes { regular: NoUndef, arg_ext: Zext, pointee_size: Size(0 bytes), pointee_align: None }) }, fixed_count: 1, conv: Rust, c_variadic: false } +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc translate_rigid_ty: Bool +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc translate_rigid_ty: Bool +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc translate_rigid_ty: Int(I32) +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc translate_rigid_ty: Int(I32) +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc register_fun_decl_id: DefId { id: 1, name: "main" } +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc ***Not found! +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc register_fun_decl_id: {DefId { id: 0, name: "is_zero" }: Fun(0), DefId { id: 1, name: "main" }: Fun(1)} +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc function_type, args=[], fn_abi=FnAbi { args: [], ret: ArgAbi { ty: Ty { id: 2, kind: RigidTy(Tuple([])) }, layout: Layout(2), mode: Ignore }, fixed_count: 0, conv: Rust, c_variadic: false } +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc translate_rigid_ty: Tuple([]) +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc translate_rigid_ty: Tuple([]) +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc translate_rigid_ty: Bool +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc translate_call: Constant(ConstOperand { span: Span { id: 0, repr: "test.rs:14:13: 14:20" }, user_ty: None, const_: MirConst { kind: ZeroSized, ty: Ty { id: 0, kind: RigidTy(FnDef(FnDef(DefId { id: 0, name: "is_zero" }), GenericArgs([]))) }, id: MirConstId(0) } }) [Constant(ConstOperand { span: Span { id: 1, repr: "test.rs:14:21: 14:22" }, user_ty: None, const_: MirConst { kind: Allocated(Allocation { bytes: [Some(0), Some(0), Some(0), Some(0)], provenance: ProvenanceMap { ptrs: [] }, align: 4, mutability: Mut }), ty: Ty { id: 1, kind: RigidTy(Int(I32)) }, id: MirConstId(1) } })] _1 Some(1) +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc register_fun_decl_id: DefId { id: 0, name: "is_zero" } +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc register_fun_decl_id: {DefId { id: 0, name: "is_zero" }: Fun(0), DefId { id: 1, name: "main" }: Fun(1)} +DEBUG kani_compiler::codegen_aeneas_llbc::mir_to_ullbc translate_rigid_ty: Int(I32) +DEBUG kani_compiler::codegen_aeneas_llbc::compiler_interface # Final LLBC before serialization: + +fn test::is_zero(@1: i32) -> bool +{ + let @0: bool; // return + let i@1: i32; // arg #1 + + @0 := copy (i@1) == const (0 : i32) + return +} + +fn test::main() +{ + let @0: (); // return + let @1: bool; // anonymous local + + @1 := @Fun0(const (0 : i32)) + drop @1 + @0 := () + return +} + + + +Writing LLBC file to /home/ubuntu/git/kani/tests/expected/llbc/basic0/test__RNvCs5jAuZAZg7Qa_4test4main.symtab.llbc +INFO charon_lib::export in serialize_to_file at charon/charon/src/export.rs:69: Generated the file: /home/ubuntu/git/kani/tests/expected/llbc/basic0/test__RNvCs5jAuZAZg7Qa_4test4main.symtab.llbc +DEBUG kani_compiler::kani_middle::codegen_units store_metadata, filename="/home/ubuntu/git/kani/tests/expected/llbc/basic0/test.kani-metadata.json" +DEBUG kani_compiler::codegen_aeneas_llbc::compiler_interface link, crate_type=Rlib, out_path="/home/ubuntu/git/kani/tests/expected/llbc/basic0/libtest.rlib" +Finished /home/ubuntu/git/kani/target/kani/bin/kani-compiler in 0.05194078s +2024-11-05T21:46:17.566373Z DEBUG kani_driver: main_failure error=Failed to process /home/ubuntu/git/kani/tests/expected/llbc/basic0/test__RNvCs5jAuZAZg7Qa_4test4main.symtab.out + +Caused by: + No such file or directory (os error 2) +error: Failed to process /home/ubuntu/git/kani/tests/expected/llbc/basic0/test__RNvCs5jAuZAZg7Qa_4test4main.symtab.out: No such file or directory (os error 2) diff --git a/tests/expected/llbc/basic1/TestRNvCs5jAuZAZg7Qa4test4main.symtab.lean b/tests/expected/llbc/basic1/TestRNvCs5jAuZAZg7Qa4test4main.symtab.lean new file mode 100644 index 000000000000..e9731570d6b4 --- /dev/null +++ b/tests/expected/llbc/basic1/TestRNvCs5jAuZAZg7Qa4test4main.symtab.lean @@ -0,0 +1,25 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [test] +import Base +open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false + +namespace test + +/- [test::select]: + Source: 'test.rs', lines 8:1-8:42 -/ +def select (s : Bool) (x : I32) (y : I32) : Result I32 := + if s + then Result.ok x + else Result.ok y + +/- [test::main]: + Source: 'test.rs', lines 13:1-13:10 -/ +def main : Result Unit := + do + let _ ← select true 3#i32 7#i32 + Result.ok () + +end test diff --git a/tools/build-kani/license-notes.txt b/tools/build-kani/license-notes.txt index 6e717c98012b..04070480ccd0 100644 --- a/tools/build-kani/license-notes.txt +++ b/tools/build-kani/license-notes.txt @@ -17,9 +17,6 @@ Acknowledgement: Computer Science Department, University of Oxford Computer Science Department, Carnegie Mellon University -cbmc-viewer: https://github.com/model-checking/cbmc-viewer -License: Apache-2.0 - ## Notable Python dependencies voluptuous: https://github.com/alecthomas/voluptuous diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs index 8f36f4598e88..c45e9a72b189 100644 --- a/tools/build-kani/src/main.rs +++ b/tools/build-kani/src/main.rs @@ -43,7 +43,6 @@ fn main() -> Result<()> { bundle_kani(dir)?; bundle_cbmc(dir)?; bundle_kissat(dir)?; - // cbmc-viewer isn't bundled, it's pip install'd on first-time setup create_release_bundle(dir, &bundle_name)?; @@ -140,7 +139,6 @@ fn bundle_cbmc(dir: &Path) -> Result<()> { cp(&which::which("goto-instrument")?, &bin)?; cp(&which::which("goto-cc")?, &bin)?; cp(&which::which("symtab2gb")?, &bin)?; - // cbmc-viewer invokes this cp(&which::which("goto-analyzer")?, &bin)?; Ok(())