Struct FuncInfo 

pub struct FuncInfo {
    pub inline: bool,
    pub hide: bool,
    pub rank: usize,
    pub uif: bool,
}

This type represents what we know about a flux-def after normalization, i.e. after “inlining” all or some transitively called flux-defs.

• When FLUX_SMT_DEFINE_FUN=1 is set we inline all polymorphic flux-defs, since they cannot be represented as define-fun in SMTLIB but leave all monomorphic flux-defs un-inlined.
• When the above flag is not set, we replace every flux-def with its (transitively) inlined body

Fields

inline: bool

Whether or not this function is inlined (i.e. NOT represented as define-fun). This value is irrelevant of UIFs.

hide: bool

Whether or not this function is uninterpreted by default This value is irrelevant of UIFs.

rank: usize

The rank of this function in the topological sort of all the flux-defs, needed so we can specify the define-fun in the correct order, without any “forward” dependencies which the SMT solver cannot handle.

uif: bool

Whether the function is a UIF

Trait Implementations

impl Clone for FuncInfo

fn clone(&self) -> FuncInfo

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'tcx, __D: TyDecoder<'tcx>> Decodable<__D> for FuncInfo

fn decode(__decoder: &mut __D) -> Self

impl<'tcx, __E: TyEncoder<'tcx>> Encodable<__E> for FuncInfo

fn encode(&self, __encoder: &mut __E)