Struct boogie_backend::boogie_wrapper::BoogieWrapper

pub struct BoogieWrapper<'env> {
    pub env: &'env GlobalEnv,
    pub targets: &'env FunctionTargetsHolder,
    pub writer: &'env CodeWriter,
    pub options: &'env BoogieOptions,
}

Represents the boogie wrapper.

Fields

env: &'env GlobalEnv

targets: &'env FunctionTargetsHolder

writer: &'env CodeWriter

options: &'env BoogieOptions

Implementations

impl<'env> BoogieWrapper<'env>

pub fn call_boogie(&self, boogie_file: &str) -> Result<BoogieOutput>

Calls boogie on the given file. On success, returns a struct representing the analyzed output of boogie.

pub fn call_boogie_and_verify_output(&self, boogie_file: &str) -> Result<()>

Calls boogie and analyzes output.