Eva_gui.Gui_types
type gui_callstack =
| GC_Filtered |
| GC_Consolidated |
| GC_Single of Frama_c_kernel.Value_types.callstack |
| GC_Callstack of Frama_c_kernel.Value_types.callstack |
val hash_gui_callstack : gui_callstack -> int
val compare_gui_callstack : gui_callstack -> gui_callstack -> int
type gui_selection =
| GS_TLVal of Frama_c_kernel.Cil_types.term |
| GS_LVal of Frama_c_kernel.Cil_types.lval |
| GS_AbsoluteMem |
| GS_Expr of Frama_c_kernel.Cil_types.exp |
| GS_Term of Frama_c_kernel.Cil_types.term |
| GS_Predicate of Frama_c_kernel.Cil_types.predicate |
val pretty_gui_selection : Stdlib.Format.formatter -> gui_selection -> unit
val gui_selection_equal : gui_selection -> gui_selection -> bool
type gui_offsetmap_res =
| GO_Bottom |
| GO_Empty |
| GO_Top |
| GO_InvalidLoc |
| GO_Offsetmap of Frama_c_kernel.Cvalue.V_Offsetmap.t |
val equal_gui_offsetmap_res : gui_offsetmap_res -> gui_offsetmap_res -> bool
val pretty_gui_offsetmap_res :
?typ:Frama_c_kernel.Cil_types.typ ->
Stdlib.Format.formatter ->
gui_offsetmap_res ->
unit
val join_gui_offsetmap_res :
gui_offsetmap_res ->
gui_offsetmap_res ->
gui_offsetmap_res
type gui_loc =
| GL_Stmt of Frama_c_kernel.Cil_types.kernel_function
* Frama_c_kernel.Cil_types.stmt |
| GL_Pre of Frama_c_kernel.Cil_types.kernel_function |
| GL_Post of Frama_c_kernel.Cil_types.kernel_function |
val gui_loc_loc : gui_loc -> Frama_c_kernel.Cil_types.location
val kf_of_gui_loc : gui_loc -> Frama_c_kernel.Cil_types.kernel_function
val pretty_callstack :
Stdlib.Format.formatter ->
Frama_c_kernel.Value_types.callstack ->
unit
val pretty_callstack_short :
Stdlib.Format.formatter ->
Frama_c_kernel.Value_types.callstack ->
unit
type 'a gui_res =
| GR_Empty |
| GR_Offsm of gui_offsetmap_res * Frama_c_kernel.Cil_types.typ option |
| GR_Value of 'a Eva.Eval.flagged_value * Frama_c_kernel.Cil_types.typ option |
| GR_Status of Frama_c_kernel.Abstract_interp.Comp.result |
| GR_Zone of Frama_c_kernel.Locations.Zone.t |
module type S = sig ... end