cc_contract.rs

#![no_std]
#![feature(core_intrinsics)]

#[macro_use]
extern crate klee;
use klee::kassume;

use core::ptr;
use core::intrinsics::unchecked_div;

fn main() {
    f1_check();
    f2_check();
    f2_f1_check();
}

// contract f1
fn f1_pre(u: u8) -> bool {
    true
}

fn f1_post(u: u8) -> bool {
    u > 0
}

// check pre-post f1
fn f1_check() {
    let u = ksymbol!("u");
    kassume(f1_pre(u));
    let r = f1(u);
    kassert!(f1_post(r));
}

fn f1(u: u8) -> u8 {
    u.checked_add(1).unwrap_or(u)
}

// contract f2
fn f2_pre(u: u8) -> bool {
    u != 0
}

fn f2_post(u: u8) -> bool {
    true
}

// check pre-post f2
fn f2_check() {
    let u = ksymbol!("u");
    kassume(f2_pre(u));
    let r = f2(u);
    kassert!(f2_post(r));
}

fn f2(u: u8) -> u8 {
    unsafe { unchecked_div(100, u) }
}

// check f2_f1 composition
fn f2_f1_check() {
    let u = ksymbol!("u");
    kassume(f1_post(u));
    kassert!(f2_pre(u));
}