PulseModelsDSL.Syntaxmodule ModeledField = PulseOperations.ModeledFieldval let* : 'a model_monad -> ('a -> 'b model_monad) -> 'b model_monadval ret : 'a -> 'a model_monadval throw : unit model_monadval unreachable : 'a model_monadval list_fold :
'a list ->
init:'accum ->
f:('accum -> 'a -> 'accum model_monad) ->
'accum model_monadval list_iter : 'a list -> f:('a -> unit model_monad) -> unit model_monadval list_filter_map :
'a list ->
f:('a -> 'b option model_monad) ->
'b list model_monadval option_iter : 'a option -> f:('a -> unit model_monad) -> unit model_monadval absvalue_set_fold :
Pulselib.PulseBasicInterface.AbstractValue.Set.t ->
init:'accum ->
f:
('accum ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
'accum model_monad) ->
'accum model_monadval absvalue_set_iter :
Pulselib.PulseBasicInterface.AbstractValue.Set.t ->
f:(Pulselib.PulseBasicInterface.AbstractValue.t -> unit model_monad) ->
unit model_monadval ignore : 'a model_monad -> unit model_monadval assign_ret : aval -> unit model_monadassign the value to the return variable of the current function
val dynamic_dispatch :
cases:(IR.Typ.name * (unit -> 'a model_monad)) list ->
?default:(unit -> 'a model_monad) ->
aval ->
'a model_monadval dispatch_call :
(IR.Ident.t * IR.Typ.t) ->
IR.Procname.t ->
(IR.Exp.t * IR.Typ.t) list ->
Pulselib.PulseBasicInterface.ValueOrigin.t
Absint.ProcnameDispatcher.Call.FuncArg.t
list ->
unit model_monadval get_data : PulseModelsImport.model_data model_monadval disjuncts : 'a model_monad list -> 'a model_monadval start_model : unit model_monad -> PulseModelsImport.modelget a model from a disjunctive model_monad
val lift_to_monad : PulseModelsImport.model -> unit model_monadbeware that the model may modify the PulseModelsImport.model_data.ret field
val lift_to_monad_and_get_result : PulseModelsImport.model -> aval model_monadapply the model and return its result. fails if the model did not assign the reserved model_data.ret variable.
PulseOperations functions you need should be copied here
val allocation :
Pulselib.PulseBasicInterface.Attribute.allocator ->
aval ->
unit model_monadval add_dict_contain_const_keys : aval -> unit model_monadval add_dict_read_const_key : aval -> IR.Fieldname.t -> unit model_monadval remove_dict_contain_const_keys : aval -> unit model_monadval add_static_type : IR.Typ.name -> aval -> unit model_monadval deep_copy : ?depth_max:int -> aval -> aval model_monadval eval_binop : IR.Binop.t -> aval -> aval -> aval model_monadval eval_binop_int : IR.Binop.t -> aval -> IR.IntLit.t -> aval model_monadval eval_read : IR.Exp.t -> aval model_monadval eval_const_int : int -> aval model_monadval eval_const_string : string -> aval model_monadval eval_string_concat : aval -> aval -> aval model_monadval eval_to_value_origin :
IR.Exp.t ->
Pulselib.PulseBasicInterface.ValueOrigin.t model_monadval eval_access :
?desc:string ->
PulseOperationResult.Import.access_mode ->
aval ->
Pulselib.PulseBasicInterface.Access.t ->
aval model_monadval eval_deref_access :
PulseOperationResult.Import.access_mode ->
aval ->
Pulselib.PulseBasicInterface.Access.t ->
aval model_monadval and_dynamic_type_is : aval -> IR.Typ.t -> unit model_monadval get_dynamic_type :
ask_specialization:bool ->
aval ->
Pulselib.PulseBasicInterface.Formula.dynamic_type_data option model_monadval new_ : IR.Exp.t -> aval model_monadval constructor : IR.Typ.Name.t -> (string * aval) list -> aval model_monadconstructor_dsl typ_name fields builds a fresh object of type typ_name and initializes its fields using list fields
val get_const_string : aval -> string option model_monadval mk_fresh : model_desc:string -> ?more:string -> unit -> aval model_monadval write_field : ref:aval -> obj:aval -> IR.Fieldname.t -> unit model_monadval write_deref_field :
ref:aval ->
obj:aval ->
IR.Fieldname.t ->
unit model_monadval get_known_fields :
aval ->
Pulselib.PulseBasicInterface.Access.t list model_monadReturn the fields we know about. There may be more, so use with caution
val prune_eq : aval -> aval -> unit model_monadval prune_eq_int : aval -> IR.IntLit.t -> unit model_monadval prune_eq_string : aval -> string -> unit model_monadval prune_ne_string : aval -> string -> unit model_monadval prune_eq_zero : aval -> unit model_monadval prune_positive : aval -> unit model_monadval prune_lt : aval -> aval -> unit model_monadval prune_lt_int : aval -> IR.IntLit.t -> unit model_monadval prune_le : aval -> aval -> unit model_monadval prune_gt : aval -> aval -> unit model_monadval prune_ge : aval -> aval -> unit model_monadval prune_ge_int : aval -> IR.IntLit.t -> unit model_monadval prune_ne : aval -> aval -> unit model_monadval prune_ne_int : aval -> IR.IntLit.t -> unit model_monadval prune_ne_zero : aval -> unit model_monadval and_eq_int : aval -> IR.IntLit.t -> unit model_monadval and_eq : aval -> aval -> unit model_monadval and_equal_instanceof : aval -> aval -> IR.Typ.t -> unit model_monadval and_positive : aval -> unit model_monadval as_constant_q : aval -> Q.t option model_monadval as_constant_int : aval -> int option model_monadval as_constant_string : aval -> string option model_monadval aval_of_int :
Pulselib.PulseBasicInterface.ValueHistory.t ->
int ->
aval model_monadval tenv_resolve_field_info :
IR.Typ.name ->
IR.Fieldname.t ->
IR.Struct.field_info option model_monadval tenv_resolve_fieldname :
IR.Typ.name ->
string ->
IR.Fieldname.t option model_monadval write_deref : ref:aval -> obj:aval -> unit model_monadval invalidate_access :
Pulselib.PulseBasicInterface.Invalidation.t ->
aval ->
Pulselib.PulseBasicInterface.Access.t ->
unit model_monadif necessary you can convert an operation outside of this module with the following operators
val exec_command : (astate -> astate) -> unit model_monadval exec_partial_command :
(astate -> astate PulseOperationResult.t) ->
unit model_monadval exec_operation : (astate -> 'a * astate) -> 'a model_monadval exec_partial_operation :
(astate -> (astate * 'a) PulseOperationResult.t) ->
'a model_monadval exec_pure_operation : (astate -> 'a) -> 'a model_monadmodule Basic : sig ... end