pub struct FunctionDataBuilder<'env> {
pub fun_env: &'env FunctionEnv<'env>,
pub data: FunctionData,
pub options: FunctionDataBuilderOptions,
/* private fields */
}
Expand description
A builder for FunctionData
.
Fields§
§fun_env: &'env FunctionEnv<'env>
§data: FunctionData
§options: FunctionDataBuilderOptions
Implementations§
source§impl<'env> FunctionDataBuilder<'env>
impl<'env> FunctionDataBuilder<'env>
sourcepub fn new_with_options(
fun_env: &'env FunctionEnv<'env>,
data: FunctionData,
options: FunctionDataBuilderOptions
) -> Self
pub fn new_with_options( fun_env: &'env FunctionEnv<'env>, data: FunctionData, options: FunctionDataBuilderOptions ) -> Self
Creates a new builder with customized options
sourcepub fn new(fun_env: &'env FunctionEnv<'env>, data: FunctionData) -> Self
pub fn new(fun_env: &'env FunctionEnv<'env>, data: FunctionData) -> Self
Creates a new builder with options set to default values
sourcepub fn get_target(&self) -> FunctionTarget<'_>
pub fn get_target(&self) -> FunctionTarget<'_>
Gets a function target viewpoint on this builder. This locks the data for mutation until the returned value dies.
sourcepub fn add_return(&mut self, ty: Type) -> usize
pub fn add_return(&mut self, ty: Type) -> usize
Add a return parameter.
sourcepub fn set_loc_and_vc_info(&mut self, loc: Loc, message: &str)
pub fn set_loc_and_vc_info(&mut self, loc: Loc, message: &str)
Sets the default location as well as information about the verification condition
message associated with the next instruction generated with emit_with
.
sourcepub fn set_loc_from_attr(&mut self, attr_id: AttrId)
pub fn set_loc_from_attr(&mut self, attr_id: AttrId)
Sets the default location from a code attribute id.
sourcepub fn new_attr(&mut self) -> AttrId
pub fn new_attr(&mut self) -> AttrId
Creates a new bytecode attribute id with default location.
sourcepub fn emit_with<F>(&mut self, f: F)where
F: FnOnce(AttrId) -> Bytecode,
pub fn emit_with<F>(&mut self, f: F)where F: FnOnce(AttrId) -> Bytecode,
Emits a bytecode via a function which takes a freshly generated attribute id.
sourcepub fn set_next_debug_comment(&mut self, comment: String)
pub fn set_next_debug_comment(&mut self, comment: String)
Sets the debug comment which should be associated with the next instruction
emitted with self.emit_with(|id| ..)
.
sourcepub fn clear_next_debug_comment(&mut self)
pub fn clear_next_debug_comment(&mut self)
This will clear the state that the next self.emit_with(..)
will add a debug comment.
sourcepub fn emit_let(&mut self, def: Exp) -> (TempIndex, Exp)
pub fn emit_let(&mut self, def: Exp) -> (TempIndex, Exp)
Emits a let: this creates a new temporary and emits an assumption that this temporary is equal to the given expression. This can be used to abbreviate large expressions which are used multiple times, or get the value of an expression into a temporary for bytecode. Returns the temporary and a local expression referring to it.
sourcepub fn emit_let_havoc(&mut self, ty: Type) -> (TempIndex, Exp)
pub fn emit_let_havoc(&mut self, ty: Type) -> (TempIndex, Exp)
Emits a new temporary with a havoced value of given type.
Trait Implementations§
source§impl<'env> ExpGenerator<'env> for FunctionDataBuilder<'env>
impl<'env> ExpGenerator<'env> for FunctionDataBuilder<'env>
source§fn function_env(&self) -> &FunctionEnv<'env>
fn function_env(&self) -> &FunctionEnv<'env>
source§fn get_current_loc(&self) -> Loc
fn get_current_loc(&self) -> Loc
source§fn add_local(&mut self, ty: Type) -> TempIndex
fn add_local(&mut self, ty: Type) -> TempIndex
source§fn get_local_type(&self, temp: TempIndex) -> Type
fn get_local_type(&self, temp: TempIndex) -> Type
temp
index§fn global_env(&self) -> &'env GlobalEnv
fn global_env(&self) -> &'env GlobalEnv
§fn set_loc_from_node(&mut self, node_id: NodeId)
fn set_loc_from_node(&mut self, node_id: NodeId)
§fn new_node(&self, ty: Type, inst_opt: Option<Vec<Type, Global>>) -> NodeId
fn new_node(&self, ty: Type, inst_opt: Option<Vec<Type, Global>>) -> NodeId
§fn mk_bool_const(&self, value: bool) -> Exp
fn mk_bool_const(&self, value: bool) -> Exp
§fn mk_call(&self, ty: &Type, oper: Operation, args: Vec<Exp, Global>) -> Exp
fn mk_call(&self, ty: &Type, oper: Operation, args: Vec<Exp, Global>) -> Exp
§fn mk_call_with_inst(
&self,
ty: &Type,
inst: Vec<Type, Global>,
oper: Operation,
args: Vec<Exp, Global>
) -> Exp
fn mk_call_with_inst( &self, ty: &Type, inst: Vec<Type, Global>, oper: Operation, args: Vec<Exp, Global> ) -> Exp
§fn mk_ite(&self, cond: ExpData, if_true: ExpData, if_false: ExpData) -> Exp
fn mk_ite(&self, cond: ExpData, if_true: ExpData, if_false: ExpData) -> Exp
§fn mk_bool_call(&self, oper: Operation, args: Vec<Exp, Global>) -> Exp
fn mk_bool_call(&self, oper: Operation, args: Vec<Exp, Global>) -> Exp
§fn mk_identical(&self, arg1: Exp, arg2: Exp) -> Exp
fn mk_identical(&self, arg1: Exp, arg2: Exp) -> Exp
make_equal
because
it requires the exact same representation, not only interpretation.§fn mk_implies(&self, arg1: Exp, arg2: Exp) -> Exp
fn mk_implies(&self, arg1: Exp, arg2: Exp) -> Exp
§fn mk_builtin_num_const(&self, oper: Operation) -> Exp
fn mk_builtin_num_const(&self, oper: Operation) -> Exp
§fn mk_join_bool(
&self,
oper: Operation,
args: impl Iterator<Item = Exp>
) -> Option<Exp>
fn mk_join_bool( &self, oper: Operation, args: impl Iterator<Item = Exp> ) -> Option<Exp>
§fn mk_join_opt_bool(
&self,
oper: Operation,
arg1: Option<Exp>,
arg2: Option<Exp>
) -> Option<Exp>
fn mk_join_opt_bool( &self, oper: Operation, arg1: Option<Exp>, arg2: Option<Exp> ) -> Option<Exp>
§fn mk_vector_quant_opt<F>(
&self,
kind: QuantKind,
vector: Exp,
elem_ty: &Type,
f: &mut F
) -> Option<Exp>where
F: FnMut(Exp) -> Option<Exp>,
fn mk_vector_quant_opt<F>( &self, kind: QuantKind, vector: Exp, elem_ty: &Type, f: &mut F ) -> Option<Exp>where F: FnMut(Exp) -> Option<Exp>,
f
receives
an expression representing an element of the vector and returns the quantifiers predicate;
if it returns None, this function will also return None, otherwise the quantifier will be
returned.§fn mk_mem_quant_opt<F>(
&self,
kind: QuantKind,
mem: QualifiedId<StructId>,
f: &mut F
) -> Option<ExpData>where
F: FnMut(Exp) -> Option<Exp>,
fn mk_mem_quant_opt<F>( &self, kind: QuantKind, mem: QualifiedId<StructId>, f: &mut F ) -> Option<ExpData>where F: FnMut(Exp) -> Option<Exp>,
f
receives§fn mk_inst_mem_quant_opt<F>(
&self,
kind: QuantKind,
mem: &QualifiedInstId<StructId>,
f: &mut F
) -> Option<Exp>where
F: FnMut(Exp) -> Option<Exp>,
fn mk_inst_mem_quant_opt<F>( &self, kind: QuantKind, mem: &QualifiedInstId<StructId>, f: &mut F ) -> Option<Exp>where F: FnMut(Exp) -> Option<Exp>,
f
receives an expression representing a value in memory and returns the quantifiers predicate;