Struct Task 

pub struct Task<T: Types> {
    pub comments: Vec<String>,
    pub constants: Vec<ConstDecl<T>>,
    pub data_decls: Vec<DataDecl<T>>,
    pub define_funs: Vec<FunDef<T>>,
    pub kvars: Vec<KVarDecl<T>>,
    pub constraint: Constraint<T>,
    pub qualifiers: Vec<Qualifier<T>>,
    pub scrape_quals: bool,
    pub solver: SmtSolver,
}

Fields

comments: Vec<String>

constants: Vec<ConstDecl<T>>

data_decls: Vec<DataDecl<T>>

define_funs: Vec<FunDef<T>>

kvars: Vec<KVarDecl<T>>

constraint: Constraint<T>

qualifiers: Vec<Qualifier<T>>

scrape_quals: bool

solver: SmtSolver

Implementations

impl<T: Types> Task<T>

pub fn hash_with_default(&self) -> u64

pub fn run( &self, timeout: Option<Duration>, ) -> Result<VerificationResult<T::Tag>, FixpointError>

Runs the task by calling the fixpoint binary. If timeout is given and fixpoint doesn’t finish in time, the process is killed and FixpointError::Timeout is returned.

Trait Implementations

impl<T: Types> Debug for Task<T>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<T: Types> Display for Task<T>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<T: Types> Hash for Task<T>

fn hash<__H: Hasher>(&self, __state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.