module Register_gui: sig
.. end
Extension of the GUI in order to support the value analysis.
No function is exported.
type
lval_or_absolute =
val pretty_lval_or_absolute : Format.formatter -> lval_or_absolute -> unit
type
offsetmap_result =
| |
Bottom |
| |
InvalidLoc |
| |
Offsetmap of Cvalue.V_Offsetmap.t |
val equal_offsetmap_result : offsetmap_result -> offsetmap_result -> bool
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 log_alarms : unit -> CilE.warn_mode * bool Pervasives.ref
val pp_eval_ok : Format.formatter -> bool -> unit
val lval_or_absolute_to_offsetmap : Cvalue.Model.t ->
lval_or_absolute -> offsetmap_result * bool
val pretty_lva_before_after : Design.main_window ->
before:Cvalue.Model.t ->
after:(Cvalue.Model.t * bool) option -> lval_or_absolute -> unit
val pretty_lva_callstacks : Design.main_window ->
cbefore:Cvalue.Model.t Value_types.Callstack.Hashtbl.t ->
cafter:Cvalue.Model.t Value_types.Callstack.Hashtbl.t option ->
lval_or_absolute -> unit
val approximated_after_state : Cil_types.stmt -> Cvalue.Model.t
val pretty_lva_at_stmt : Design.main_window ->
Db.Value.AfterTable.key -> lval_or_absolute -> unit
val pretty_formal_initial_state : Design.main_window_extension_points ->
Cil_types.varinfo -> Cvalue.Model.t -> unit
val gui_compute_values : Design.main_window_extension_points -> unit
val cleant_outputs : Cil_types.kernel_function -> Cil_types.stmt -> Locations.Zone.t option
val eval_user_term : Design.main_window ->
Cil_types.kernel_function -> Cil_datatype.Stmt.t -> string -> unit
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