module GuiSource: sig
.. end
type
selection =
| |
S_none |
| |
S_fun of Kernel_function.t |
| |
S_prop of Property.t |
| |
S_call of call |
type
call = {
|
s_caller : Kernel_function.t ; |
|
s_called : Kernel_function.t ; |
|
s_stmt : Cil_datatype.Stmt.t ; |
}
val selection_of_localizable : Pretty_source.localizable -> selection
val kind_of_property : Property.identified_property -> string
val is_rte_generated : Cil_types.kernel_function -> bool
val is_rte_precond : Cil_types.kernel_function -> bool
class popup : unit ->
object
.. end
module PATH: Cil_datatype.Stmt.Set
module DEPS: Property.Set
val apply_tag : string ->
GText.tag_property list -> GSourceView2.source_buffer -> int -> int -> unit
val apply_goal : GSourceView2.source_buffer -> int -> int -> unit
val apply_effect : GSourceView2.source_buffer -> int -> int -> unit
val apply_path : GSourceView2.source_buffer -> int -> int -> unit
val apply_depend : GSourceView2.source_buffer -> int -> int -> unit
val instructions : PATH.t -> PATH.t
val lemmas : LogicUsage.logic_lemma list -> DEPS.t
class highlighter : Design.main_window_extension_points ->
object
.. end