// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// Example from Firecracker micro_http request handling
// https://github.com/firecracker-microvm/firecracker/commit/22908c9fb0cd5fb20febc5d18ff1284caa5f3a53

// Should return a nondet string of up to n characters
// Currently Kani does not support strings
fn any_string(n: u32) -> String {
    unimplemented!()
}

// from 4e905f741
fn bug(n: u32) {
    let request_uri: String = kani::any_string(n);
    let _path_tokens: Vec<&str> = request_uri[1..].split_terminator('/').collect();
    //                                        ^ slice of empty string panics
}

// from 22908c9fb
fn fix(n: u32) {
    let request_uri: String = kani::any_string(n);
    let _path_tokens: Vec<&str> =
        request_uri.trim_start_matches('/').split_terminator('/').collect();
}

#[kani::proof]
fn main() {
    let n: u32 = kani::any();
    bug(n);
    fix(n);
}