// indirect.rs
extern crate kani;

use std::convert::TryFrom;

/// Constrain `val` to be a valid character.
#[kani::requires(u32::from(_char) == val)]
#[kani::ensures(|res| *res == _char)]
pub fn indirect_assumption(val: u32, _char: char) -> char {
    char::try_from(val).unwrap()
}

mod verify {
    use super::*;
    use kani::Arbitrary;

    #[kani::proof_for_contract(indirect_assumption)]
    fn check_indirect_contract() {
        indirect_assumption(kani::any(), kani::any());
    }

    /// This harness that encodes the pre-condition using`kani::assume` succeeds
    #[kani::proof]
    fn check_indirect() {
        let val = kani::any();
        let c = kani::any();
        kani::assume(u32::from(c) == val);
        indirect_assumption(val, c);
    }
}