How it can support ensures, requires, invariant API in Rust

[1vs9]

Now，smack doesn't support ensures，requires and invariant API in Rust，
When I Just declare them in smack.rs，it doesn't work，

#![crate_type = "staticlib"]

use std::alloc::Layout;

#[cfg(verifier = "smack")]
extern "C" {
    pub fn __VERIFIER_assert(x: i32);
    pub fn __VERIFIER_assume(x: i32);
    pub fn __VERIFIER_nondet_i8() -> i8;
    pub fn __VERIFIER_nondet_u8() -> u8;
    pub fn __VERIFIER_nondet_i16() -> i16;
    pub fn __VERIFIER_nondet_u16() -> u16;
    pub fn __VERIFIER_nondet_i32() -> i32;
    pub fn __VERIFIER_nondet_u32() -> u32;
    pub fn __VERIFIER_nondet_i64() -> i64;
    pub fn __VERIFIER_nondet_u64() -> u64;
    pub fn __VERIFIER_nondet_float() -> f32;
    pub fn __VERIFIER_nondet_double() -> f64;
    pub fn malloc(size: usize) -> *mut u8;
    pub fn __VERIFIER_memcpy(dest: *mut u8, src: *mut u8, count: usize) -> *mut u8;
    pub fn free(ptr: *mut u8);
    pub fn memset(ptr: *mut u8, ch: i32, count: usize);
    pub fn realloc(ptr: *mut u8, new_size: usize) -> *mut u8;
    // contract
    pub fn __CONTRACT_requires(expr: bool);
    pub fn __CONTRACT_ensures(expr: bool);
    pub fn __CONTRACT_invariant(expr: bool);
}

#[macro_export]
macro_rules! requires {
    ( $cond:expr ) => {
        unsafe {
            __CONTRACT_requires($cond as bool);
        };
    };
}

#[macro_export]
macro_rules! ensures {
    ( $cond:expr ) => {
        unsafe {
            __CONTRACT_ensures($cond);
        };
    };
}

#[macro_export]
macro_rules! invariant {
    ( $cond:expr ) => {
        unsafe {
            __CONTRACT_invariant($cond as bool);
        };
    };
}

And Then I test it by add ensures in test file

#[macro_use]
extern crate smack;
use smack::*;

// @expect verified

fn main() {
    smack::ensures(false);
}

The result is a error which tells me "ensure you have llvm-symbolizer in your PATH or set the environment var LLVM_SYMBOLIZER_PATH to point it", and return a Exception("segmentation fault")

So, if I want to use ensures, requires and invariant API in Rust just like in clang, what should I do?
I would be very happy if you could guide me, and I will be very glad to help you to implement the relevant content!
Thanks again!