package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. A
    Anne Pacalet
  36. V
    Valentin Perrelle
  37. G
    Guillaume Petiot
  38. D
    Dario Pinto
  39. V
    Virgile Prevosto
  40. A
    Armand Puccetti
  41. F
    Félix Ridoux
  42. V
    Virgile Robles
  43. M
    Muriel Roger
  44. J
    Julien Signoles
  45. N
    Nicolas Stouls
  46. K
    Kostyantyn Vorobyov
  47. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz
sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c.gui/Frama_c_gui/Gtk_helper/index.html

Module Frama_c_gui.Gtk_helperSource

Generic Gtk helpers.

  • since Boron-20100401
Sourceval framac_icon : GdkPixbuf.pixbuf option
  • since Boron-20100401
Sourcemodule Icon : sig ... end

Some generic icon management tools.

Sourcemodule Configuration : sig ... end

Configuration module for the GUI: all magic visual constants should use this mechanism (window width, ratios, ...).

Tags

Sourceval make_tag : < tag_table : Gtk.text_tag_table ; create_tag : ?name:string -> GText.tag_property list -> GText.tag.. > -> name:string -> GText.tag_property list -> GText.tag
Sourceval apply_tag : GSourceView.source_buffer -> GText.tag -> int -> int -> unit
Sourceval remove_tag : GSourceView.source_buffer -> GText.tag -> int -> int -> unit
Sourceval cleanup_tag : GSourceView.source_buffer -> GText.tag -> unit
Sourceval cleanup_all_tags : GSourceView.source_buffer -> unit

Channels

Sourceval make_formatter : ?flush:(unit -> unit) -> GText.buffer -> Format.formatter

Build a formatter that redirects its output to the given buffer. flush is called whenever the formatter is flushed.

Sourceval log_redirector : ?flush:(unit -> unit) -> (string -> unit) -> unit

Redirects all strings written to the terminal and call the given function on each.

Sourceval redirect : Format.formatter -> GText.buffer -> unit

Redirect the given formatter to the given buffer

Asynchronous command execution

Sourceval spawn_command : ?timeout:int -> ?stdout:Buffer.t -> ?stderr:Buffer.t -> string -> string array -> (Unix.process_status -> unit) -> unit

Launches the given command and calls the given function when the process terminates. If timeout is > 0 (the default) then the process will be killed if it does not end before timeout seconds. In this case the returned process status will be Unix.WSIGNALED Sys.sigalrm.

Locks

Sourceval gui_unlocked : bool ref

This is a mutex you may use to prevent running some code while the GUI is locked.

Sourceval register_locking_machinery : ?lock_last:bool -> lock:(bool -> unit) -> unlock:(unit -> unit) -> unit -> unit

Add hooks to the locking mechanism of the GUI. lock_last must be set to true if lock must be executed after all the others locking actions and unlock must be executed before all the others unlocking actions. Default is false. At least one "lock_last" action is allowed.

  • since Beryllium-20090901

2 Tooltips

Sourceval do_tooltip : ?tooltip:string -> < coerce : GObj.widget.. > -> unit

Add the given tooltip to the given widget. It has no effect if no tooltip is given.

Chooser

Sourcetype 'a chooser = GPack.box -> string -> (unit -> 'a) -> ('a -> unit) -> unit -> unit

The created widget is packed in the box. The two following functions are supposed to be accessors(get and set) for the value to be displayed. The returned closure may be called to resynchronize the value in the widget from the get function.

Sourceval on_bool : ?tooltip:string -> ?use_markup:bool -> bool chooser

Pack a check button

Sourceval range_selector : ?tooltip:string -> ?use_markup:bool -> GPack.box -> label:string -> lower:int -> upper:int -> (int -> unit) -> (unit -> int) -> unit -> unit
Sourceval on_int : ?tooltip:string -> ?use_markup:bool -> ?lower:int -> ?upper:int -> ?sensitive:(unit -> bool) -> ?width:int -> int chooser

Pack a spin button. By default, sensitivity is set to true when this function is called.

Sourceval on_string : ?tooltip:string -> ?use_markup:bool -> ?validator:(string -> bool) -> ?width:int -> string chooser

Pack a string chooser

Sourceval on_string_set : ?tooltip:string -> ?use_markup:bool -> ?width:int -> string chooser

Pack a string-set chooser

Sourceval on_string_completion : ?tooltip:string -> ?use_markup:bool -> ?validator:(string -> bool) -> string list -> string chooser
Sourceval on_combo : string list -> ?tooltip:string -> ?use_markup:bool -> ?width:int -> string chooser

Pack a string-selector

Error manager

Sourceclass type host = object ... end

A utility class to catch exceptions and report proper error messages. See the documentations of the methods in Design.main_window_extension_points, which inherits from this class.

Sourceclass error_manager : ?reset:(unit -> unit) -> GWindow.window_skel -> host

A utility class to catch exceptions and report proper error messages. The error dialog will be transient for the GWindow.window_skel argument.

Source files chooser

Sourceclass type source_files_chooser_host = object ... end
Sourceval source_files_chooser : source_files_chooser_host -> string list -> (string list -> unit) -> unit

Open a dialog box for choosing C source files and performing an action on them.

  • since Boron-20100401
Sourceval select_file : ?title:string -> ?dir:string ref -> ?filename:string -> unit -> string option

Launches a standard gtk file chooser window and returns the name of the selected file. Replaces GToolbox.select_file that has not been ported to lablgtk3.

  • since 19.0-Potassium

Miscellaneous

Sourceval refresh_gui : unit -> unit

Process some pending events in the main Glib loop. This is intended to be called only when !gui_unlocked == false.

  • since Beryllium-20090901
Sourceval string_selector : string list -> (GObj.widget -> unit) -> GEdit.entry
Sourceval expand_to_path : GTree.view -> Gtk.tree_path -> unit
Sourceval make_string_list : packing:(GObj.widget -> unit) -> (string -> unit) * (unit -> unit) * (unit -> string list)
  • returns

    (add, remove_selected, get_elements)

Sourceval place_paned : GPack.paned -> float -> unit

Sets the position of the paned widget to the given ratio

Sourceval save_paned_ratio : string -> GPack.paned -> unit

Saves the current ratio of the panel associated to the given key.

Sourceval old_gtk_compat : ('a -> unit) -> 'a -> unit

Catch exception Not_found and do nothing

Sourceval trace_event : GObj.event_ops -> unit

Trace all events on stderr for the given object. This is a debugging function: it should not be called during normal execution.

Sourceval make_text_page : ?pos:int -> GPack.notebook -> string -> (GPack.notebook -> unit) * GText.view

Insert a GText.view in a new page of the notebook with the given title, at position pos if specified, or last if not. It returns a new GText.view together with a function to reparent the inserted page in another notebook. The tab label of the created page will be highlighted whenever its contents changes.

  • since Beryllium-20090901
Sourceval open_in_external_viewer : ?line:int -> Frama_c_kernel.Datatype.Filepath.t -> unit

Opens file in an external viewer, optionally centered on line line (if supported by the viewer). The viewer is executed in the background (i.e. it does not block the execution of Frama-C). The external viewer is given by the environment variable EDITOR. If undefined, a default viewer is used.

  • since Magnesium-20151001
Sourcemodule MAKE_CUSTOM_LIST (A : sig ... end) : sig ... end

A functor to build custom Gtk lists. You'll probably prefer to use the highlevel custom models in the next module named Custom.List. It may be part of a future lablgtk release. Do not change anything without changing lablgtk svn.

Sourceval input_string : parent:GWindow.window -> title:string -> ?ok:string -> ?cancel:string -> ?text:string -> string -> string option

Copied from lablgtk GToolbox.input_string. See the lablgtk API for more details.

Sourceval image_menu_item : image:GObj.widget -> text:string -> packing:(GMenu.menu_item -> unit) -> GMenu.menu_item

calls the packing function to append a new menu item with an icon and a label. replaces GMenu.image_menu_item that has been deprecated in GTK3

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct