package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-32.0-beta-Germanium.tar.gz

sha256=868d57ef8007fe6c0836cd151d8c294003af34aa678285eff9547662cad36aa3

doc/src/frama-c-acsl-importer.gui/register_gui.ml.html

Source file `register_gui.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

open Cil_types

let add_menu
    (popup_factory:GMenu.menu GMenu.factory)
    (main_ui:Design.main_window_extension_points) localizable =
  begin
    match localizable with
    | Printer_tag.PVDecl (Some kf,_,{vglob=true}) ->
      ignore (popup_factory#add_item "Add function specification"
                ~callback:(fun () ->
                    let txt_opt =
                      GToolbox.input_string
                        ~title:"ACSL importer"
                        "  Enter an ACSL function specification to add  "
                    in
                    Option.iter
                      (fun txt ->
                         Register.paste_fun_spec
                           kf txt (Ast.get());
                         main_ui#redisplay ()) txt_opt));
      ignore
        (popup_factory#add_item "Add global annotation"
           ~callback:
             (fun () ->
                let txt_opt =
                  GToolbox.input_string
                    ~title:"ACSL importer"
                    "  Enter an ACSL annotation to add  "
                in
                Option.iter
                  (fun txt ->
                     let glob = Kernel_function.get_global kf in
                     let cfile =
                       (fst (Cil_datatype.Global.loc glob)).Filepath.pos_path
                     in
                     Register.paste_global_annot ~cfile txt (Ast.get());
                     main_ui#redisplay ()) txt_opt)) ;

    | Printer_tag.PStmt(kf,stmt) ->
      ignore
        (popup_factory#add_item "Add code annotation"
           ~callback:
             (fun () ->
                let txt_opt =
                  GToolbox.input_string
                    ~title:"ACSL importer"
                    "  Enter an ACSL annotation to add  "
                in
                Option.iter
                  (fun txt ->
                     Register.paste_code_annot kf stmt txt (Ast.get());
                     main_ui#redisplay ()) txt_opt)) ;

    | _ -> ()
  end

let select
    (popup_factory:GMenu.menu GMenu.factory)
    (main_ui:Design.main_window_extension_points)
    ~button localizable =
  match button with
  | 3 -> (* Popup Menu: *)
    add_menu  popup_factory main_ui localizable ;
  | _ -> (* Other buttons... *) ()

(* ------------------------------------------------------------------------ *)
let main main_ui =
  begin
    main_ui#register_source_selector select ;
  end

let () = Design.register_extension main

(* ------------------------------------------------------------------------ *)