pub struct SmtSolver { /* private fields */ }Expand description
SMT solver integration for formal verification
Implementations§
Source§impl SmtSolver
impl SmtSolver
pub fn new(solver_type: SolverType) -> Self
pub fn with_timeout(solver_type: SolverType, timeout: Duration) -> Self
Sourcepub fn verify_function(
&mut self,
function: &Function,
spec: &FunctionSpec,
) -> VerificationResult
pub fn verify_function( &mut self, function: &Function, spec: &FunctionSpec, ) -> VerificationResult
Verify a function against its specification
Sourcepub fn verify_loop_invariant(
&mut self,
loop_info: &LoopInfo,
invariant: &str,
) -> LoopVerificationResult
pub fn verify_loop_invariant( &mut self, loop_info: &LoopInfo, invariant: &str, ) -> LoopVerificationResult
Verify loop invariants
Auto Trait Implementations§
impl Freeze for SmtSolver
impl RefUnwindSafe for SmtSolver
impl Send for SmtSolver
impl Sync for SmtSolver
impl Unpin for SmtSolver
impl UnwindSafe for SmtSolver
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> Instrument for T
impl<T> Instrument for T
Source§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
Source§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more