sig
type gui_callstack =
GC_Filtered
| GC_Consolidated
| GC_Single of Value_types.callstack
| GC_Callstack of Value_types.callstack
val hash_gui_callstack : Gui_types.gui_callstack -> int
val compare_gui_callstack :
Gui_types.gui_callstack -> Gui_types.gui_callstack -> int
module GCallstackMap :
sig
type key = gui_callstack
type +'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val filter_map : (key -> 'a -> 'b option) -> 'a t -> 'b t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val min_binding_opt : 'a t -> (key * 'a) option
val max_binding : 'a t -> key * 'a
val max_binding_opt : 'a t -> (key * 'a) option
val choose : 'a t -> key * 'a
val choose_opt : 'a t -> (key * 'a) option
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val find_opt : key -> 'a t -> 'a option
val find_first : (key -> bool) -> 'a t -> key * 'a
val find_first_opt : (key -> bool) -> 'a t -> (key * 'a) option
val find_last : (key -> bool) -> 'a t -> key * 'a
val find_last_opt : (key -> bool) -> 'a t -> (key * 'a) option
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
val to_seq : 'a t -> (key * 'a) Seq.t
val to_seq_from : key -> 'a t -> (key * 'a) Seq.t
val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t
val of_seq : (key * 'a) Seq.t -> 'a t
end
type gui_selection =
GS_TLVal of Cil_types.term
| GS_LVal of Cil_types.lval
| GS_AbsoluteMem
| GS_Expr of Cil_types.exp
| GS_Term of Cil_types.term
| GS_Predicate of Cil_types.predicate
val pretty_gui_selection :
Stdlib.Format.formatter -> Gui_types.gui_selection -> unit
val gui_selection_equal :
Gui_types.gui_selection -> Gui_types.gui_selection -> bool
type gui_offsetmap_res =
GO_Bottom
| GO_Empty
| GO_Top
| GO_InvalidLoc
| GO_Offsetmap of Cvalue.V_Offsetmap.t
val equal_gui_offsetmap_res :
Gui_types.gui_offsetmap_res -> Gui_types.gui_offsetmap_res -> bool
val pretty_gui_offsetmap_res :
?typ:Cil_types.typ ->
Stdlib.Format.formatter -> Gui_types.gui_offsetmap_res -> unit
val join_gui_offsetmap_res :
Gui_types.gui_offsetmap_res ->
Gui_types.gui_offsetmap_res -> Gui_types.gui_offsetmap_res
type gui_loc =
GL_Stmt of Cil_types.kernel_function * Cil_types.stmt
| GL_Pre of Cil_types.kernel_function
| GL_Post of Cil_types.kernel_function
val gui_loc_equal : Gui_types.gui_loc -> Gui_types.gui_loc -> bool
val gui_loc_loc : Gui_types.gui_loc -> Cil_types.location
val kf_of_gui_loc : Gui_types.gui_loc -> Cil_types.kernel_function
val pretty_callstack :
Stdlib.Format.formatter -> Value_types.callstack -> unit
val pretty_callstack_short :
Stdlib.Format.formatter -> Value_types.callstack -> unit
type 'a gui_res =
GR_Empty
| GR_Offsm of Gui_types.gui_offsetmap_res * Cil_types.typ option
| GR_Value of 'a Eval.flagged_value * Cil_types.typ option
| GR_Status of Eval_terms.predicate_status
| GR_Zone of Locations.Zone.t
type 'a gui_after =
GA_After of 'a Gui_types.gui_res
| GA_Bottom
| GA_NA
| GA_Unchanged
module type S =
sig
type value
val pretty_gui_res :
Stdlib.Format.formatter ->
Gui_types.S.value Gui_types.gui_res -> unit
val equal_gui_res :
Gui_types.S.value Gui_types.gui_res ->
Gui_types.S.value Gui_types.gui_res -> bool
val vars_in_gui_res :
Gui_types.S.value Gui_types.gui_res -> Cil_types.varinfo list
val pretty_gui_after :
Stdlib.Format.formatter ->
Gui_types.S.value Gui_types.gui_after -> unit
val equal_gui_after :
Gui_types.S.value Gui_types.gui_after ->
Gui_types.S.value Gui_types.gui_after -> bool
end
module Make :
functor (V : Abstractions.Value) ->
sig
val pretty_gui_res : Format.formatter -> V.t gui_res -> unit
val equal_gui_res : V.t gui_res -> V.t gui_res -> bool
val vars_in_gui_res : V.t gui_res -> Cil_types.varinfo list
val pretty_gui_after : Format.formatter -> V.t gui_after -> unit
val equal_gui_after : V.t gui_after -> V.t gui_after -> bool
val get_cvalue : (V.t -> Main_values.CVal.t) option
val from_cvalue : Main_values.CVal.t -> V.t
end
end