Module Register_gui

module Register_gui: sig .. end
Generic functions working for lvalues and expressions.

Extension of the GUI in order to support the value analysis. No function is exported.


val results_kf_computed : Cil_types.kernel_function -> bool

Generic functions working for lvalues and expressions.
val log_alarms : unit -> CilE.warn_mode * bool Pervasives.ref
val pp_eval_ok : Format.formatter -> bool -> unit
type ('states, 'expr, 'v) evaluation_functions = {
   eval_and_warn : 'states -> 'expr -> 'v * bool;
   equal : 'v -> 'v -> bool;
   bottom : 'v;
   join : 'v -> 'v -> 'v;
   pretty : 'expr -> Format.formatter -> 'v -> unit;
}
val pretty_before_after : ('a, 'b, 'c) evaluation_functions ->
Design.main_window -> before:'a -> after:'a option -> 'b -> unit
val pretty_per_callstacks : (Cvalue.Model.t, 'a, 'b) evaluation_functions ->
Design.main_window ->
before:Cvalue.Model.t Value_types.Callstack.Hashtbl.t ->
after:Cvalue.Model.t Value_types.Callstack.Hashtbl.t option -> 'a -> unit
val callstack_fold : ('a, 'b, 'c) evaluation_functions ->
'a Value_types.Callstack.Hashtbl.t -> 'b -> 'c * bool
val pretty_callstack_summary : ('a, 'b, 'c) evaluation_functions ->
Design.main_window ->
before:'a Value_types.Callstack.Hashtbl.t ->
after:'a Value_types.Callstack.Hashtbl.t option -> 'b -> unit
val pretty_at_stmt : (Cvalue.Model.t, 'a, 'b) evaluation_functions ->
Design.main_window -> Cil_types.stmt -> 'a -> unit

lvalues-related functions
type lval_or_absolute = 
| TLVal of Cil_types.term
| LVal of Cil_types.lval
| AbsoluteMem
val pretty_lval_or_absolute : Format.formatter -> lval_or_absolute -> unit
type offsetmap_result = 
| Bottom
| Top
| InvalidLoc
| Offsetmap of Cvalue.V_Offsetmap.t
val equal_offsetmap_result : offsetmap_result -> offsetmap_result -> bool
val join_offsetmap_result : offsetmap_result ->
offsetmap_result -> offsetmap_result
val pretty_stitched_offsetmap : Format.formatter -> Cil_types.typ -> Cvalue.V_Offsetmap.t -> unit
val pretty_offsetmap_result : lval_or_absolute ->
Format.formatter -> offsetmap_result -> unit
val lval_or_absolute_to_offsetmap : Cvalue.Model.t ->
lval_or_absolute -> offsetmap_result * bool
val lval_ev : (Cvalue.Model.t, lval_or_absolute,
offsetmap_result)
evaluation_functions
val pretty_lva_at_stmt : Design.main_window ->
Cil_datatype.Stmt.t -> lval_or_absolute -> unit

Expressions-related functions
val eval_exp_and_warn : Cvalue.Model.t -> Cil_types.exp -> Cvalue.V.t * bool
val pretty_exp_result : Cil_types.exp -> Format.formatter -> Cvalue.V.t -> unit
val exp_ev : (Cvalue.Model.t, Cil_types.exp, Cvalue.V.t) evaluation_functions
val pretty_exp_at_stmt : Design.main_window -> Cil_types.stmt -> Cil_types.exp -> unit
val pretty_formal_initial_state : Design.main_window_extension_points ->
lval_or_absolute -> Cvalue.Model.t -> unit
Special case for formals

Core of the graphical interface.
val gui_compute_values : Design.main_window_extension_points -> unit
val cleant_outputs : Cil_types.kernel_function -> Cil_types.stmt -> Locations.Zone.t option
module C_labels: State_builder.Ref(Datatype.Option(Cil_datatype.Logic_label.Map.Make(Cvalue.Model)))(sig
val name : string
val dependencies : State.t list
val default : unit -> 'a option
end)
val c_labels : unit -> Cil_datatype.Logic_label.Map.Make(Cvalue.Model).t
val eval_user_term : Design.main_window ->
Cil_types.kernel_function -> Cil_datatype.Stmt.t -> string -> unit
val last_evaluate_acsl_request : string Pervasives.ref
val to_do_on_select : GMenu.menu GMenu.factory ->
Design.main_window_extension_points ->
int -> Pretty_source.localizable -> unit
module UsedVarState: Cil_state_builder.Varinfo_hashtbl(Datatype.Bool)(sig
val size : int
val name : string
val dependencies : State.t list
end)
val used_var : UsedVarState.key -> UsedVarState.data
val hide_unused : (unit -> bool) Pervasives.ref
val sync_filetree : Filetree.t -> unit
val hide_unused_function_or_var : Cil_types.global -> bool
module DegeneratedHighlighted: State_builder.Option_ref(Pretty_source.Localizable)(sig
val name : string
val dependencies : State.t list
end)
val value_panel : Design.main_window_extension_points ->
string * GObj.widget * (unit -> unit) option
val main : Design.main_window_extension_points -> unit