Struct TermAnnotation

pub struct TermAnnotation {
    pub sig: TermSignature,
    pub assumptions: Vec<Box<Expr>>,
    pub assertions: Vec<Box<Expr>>,
}

Verification IR annotations for an ISLE term consist of the function signature and a list of assertions.

Fields

sig: TermSignature

assumptions: Vec<Box<Expr>>

assertions: Vec<Box<Expr>>

Implementations

impl TermAnnotation

pub fn new( sig: TermSignature, assumptions: Vec<Expr>, assertions: Vec<Expr>, ) -> Self

New annotation

pub fn sig(&self) -> &TermSignature

pub fn assertions(&self) -> Vec<Expr>

Trait Implementations

impl Clone for TermAnnotation

fn clone(&self) -> TermAnnotation

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TermAnnotation

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

Formats the value using the given formatter.

impl PartialEq for TermAnnotation

fn eq(&self, other: &TermAnnotation) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for TermAnnotation

impl StructuralPartialEq for TermAnnotation