Module PerfMeasurer.Make

Parameters

module S : SMemory.S

Signature

val perf : (string, int * float) Stdlib.Hashtbl.t Stdlib.ref
val measure_ : string -> (unit -> 'a) -> 'a
val m1 : string -> ('a -> 'b) -> 'a -> 'b
val m2 : string -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c
val m3 : string -> ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
val m4 : string -> ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e
include module type of struct include S end
type init_data = S.init_data

Type of data that is given the first time memory is created. Useful when there's global context to know about like a type-system

Type of GIL values

Type of GIL substitutions

type err_t = S.err_t
val err_t_to_yojson : err_t -> Yojson.Safe.t
val err_t_of_yojson : Yojson.Safe.t -> err_t Ppx_deriving_yojson_runtime.error_or
val pp_err_t : Ppx_deriving_runtime.Format.formatter -> err_t -> Ppx_deriving_runtime.unit
val show_err_t : err_t -> Ppx_deriving_runtime.string
type t = S.t

Type of GIL general states

val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val pp_by_need : Utils.Containers.SS.t -> Stdlib.Format.formatter -> t -> unit
val pp_err : Stdlib.Format.formatter -> err_t -> unit
val init : init_data -> t
val get_init_data : t -> init_data
val clear : t -> t
val execute_action : string -> t -> Engine.Gpc.t -> Gillian.Symbolic.Values.t list -> (t * Gillian.Symbolic.Values.t list, err_t) Engine.Symex.result
val produce : string -> t -> Engine.Gpc.t -> Gillian.Symbolic.Values.t list -> t Engine.Symex.t
val is_overlapping_asrt : string -> bool
val copy : t -> t
val substitution_in_place : pfs:Gillian.Symbolic.Pure_context.t -> gamma:Gillian.Symbolic.Type_env.t -> Gillian.Symbolic.Subst.t -> t -> (t * Gil_syntax.Expr.Set.t * (string * Gillian.Gil_syntax.Type.t) list) list
val clean_up : ?keep:Gil_syntax.Expr.Set.t -> t -> Gil_syntax.Expr.Set.t * Gil_syntax.Expr.Set.t
val lvars : t -> Utils.Containers.SS.t
val alocs : t -> Utils.Containers.SS.t
val assertions : ?to_keep:Utils.Containers.SS.t -> t -> Gillian.Gil_syntax.Asrt.t
val mem_constraints : t -> Gillian.Gil_syntax.Expr.t list
val get_failing_constraint : err_t -> Gillian.Gil_syntax.Expr.t
val get_fixes : err_t -> Gillian.Gil_syntax.Asrt.t list
val can_fix : err_t -> bool
val sure_is_nonempty : t -> bool
val split_further : t -> string -> Gillian.Symbolic.Values.t list -> err_t -> (Gillian.Symbolic.Values.t list list * Gillian.Symbolic.Values.t list) option
val pp : Stdlib.Format.formatter -> 'a -> unit