Skip to content

goto-cc crash when there are two quantifers in one proof #4020

Open
@qinheping

Description

@qinheping

I tried this code:

// SPDX-License-Identifier: Apache-2.0 OR MIT

use std::mem;

extern crate kani;
use kani::{kani_exists, kani_forall};

#[kani::proof]
fn main() {
    let original_v = vec![kani::any::<u32>(); 3];
    let v = original_v.clone();
    let v_len = v.len();
    let v_ptr = v.as_ptr();
    unsafe {
        kani::assume(
            kani::forall!(|i in (0,v_len) | *v_ptr.wrapping_byte_offset(4*i as isize) < 5),
        );
    }

    // Prevent running `v`'s destructor so we are in complete control
    // of the allocation.
    let mut v = mem::ManuallyDrop::new(v);

    // Pull out the various important pieces of information about `v`
    let p = v.as_mut_ptr();
    let len = v.len();
    let cap = v.capacity();

    unsafe {
        // Overwrite memory
        for i in 0..len {
            *p.add(i) += 1;
            if i == 1 {
                *p.add(i) = 0;
            }
        }

        // Put everything back together into a Vec
        let rebuilt = Vec::from_raw_parts(p, len, cap);
        let rebuilt_ptr = v.as_ptr();
        assert!(
            kani::exists!(| i in (0, len) | *rebuilt_ptr.wrapping_byte_offset(4*i as isize) == 0)
        );
    }
}

using the following command line invocation:

kani from_raw_parts.rs

with Kani version: #3993

I expected to see this happen: Proof success.

Instead, this happened:

error: goto-cc exited with status signal: 11 (SIGSEGV) (core dumped)

Metadata

Metadata

Assignees

Labels

T-CBMCIssue related to an existing CBMC issue[C] BugThis is a bug. Something isn't working.

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions