Struct move_model::ast::SpecFunDecl
source · [−]pub struct SpecFunDecl {Show 13 fields
pub loc: Loc,
pub name: Symbol,
pub type_params: Vec<(Symbol, Type)>,
pub params: Vec<(Symbol, Type)>,
pub context_params: Option<Vec<(Symbol, bool)>>,
pub result_type: Type,
pub used_memory: BTreeSet<QualifiedInstId<StructId>>,
pub uninterpreted: bool,
pub is_move_fun: bool,
pub is_native: bool,
pub body: Option<Exp>,
pub callees: BTreeSet<QualifiedId<SpecFunId>>,
pub is_recursive: RefCell<Option<bool>>,
}Fields
loc: Locname: Symboltype_params: Vec<(Symbol, Type)>params: Vec<(Symbol, Type)>context_params: Option<Vec<(Symbol, bool)>>result_type: Typeused_memory: BTreeSet<QualifiedInstId<StructId>>uninterpreted: boolis_move_fun: boolis_native: boolbody: Option<Exp>callees: BTreeSet<QualifiedId<SpecFunId>>is_recursive: RefCell<Option<bool>>Trait Implementations
sourceimpl Clone for SpecFunDecl
impl Clone for SpecFunDecl
sourcefn clone(&self) -> SpecFunDecl
fn clone(&self) -> SpecFunDecl
Returns a copy of the value. Read more
1.0.0 · sourcefn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source. Read more
Auto Trait Implementations
impl !RefUnwindSafe for SpecFunDecl
impl !Send for SpecFunDecl
impl !Sync for SpecFunDecl
impl Unpin for SpecFunDecl
impl UnwindSafe for SpecFunDecl
Blanket Implementations
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
sourceimpl<T> ToOwned for T where
T: Clone,
impl<T> ToOwned for T where
T: Clone,
type Owned = T
type Owned = T
The resulting type after obtaining ownership.
sourcefn clone_into(&self, target: &mut T)
fn clone_into(&self, target: &mut T)
🔬 This is a nightly-only experimental API. (
toowned_clone_into)Uses borrowed data to replace owned data, usually by cloning. Read more