package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file GuiList.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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- PO List View                                                       --- *)
(* -------------------------------------------------------------------------- *)

open Wpo

module Windex = Indexer.Make(Wpo.S)

class model =
  object(self)
    val mutable index = Windex.empty
    method reload = index <- Windex.empty
    method add w = index <- Windex.add w index
    method size = Windex.size index
    method index w = Windex.index w index
    method get k = Windex.get k index
    method coerce = (self :> Wpo.t Wtable.listmodel)
  end

let render_prover_result p =
  let icn_stock name = [`STOCK_ID name] in
  let icn_status s = [`PIXBUF(Gtk_helper.Icon.get (Gtk_helper.Icon.Feedback s))] in
  let icn_na      = [`PIXBUF(Gtk_helper.Icon.get Gtk_helper.Icon.Unmark)] in
  let icn_none    = icn_stock "" in
  let icn_valid   = icn_status Property_status.Feedback.Valid in
  let icn_unknown = icn_status Property_status.Feedback.Unknown in
  let icn_invalid = icn_status Property_status.Feedback.Invalid in
  let icn_failed  = icn_stock "gtk-dialog-warning" in
  let icn_cut     = icn_stock "gtk-cut" in
  let icn_running = icn_stock "gtk-execute" in
  let open VCS in
  let icon_of_verdict ~smoke = function
    | NoResult -> icn_none
    | Valid    -> if smoke then icn_invalid else icn_valid
    | Invalid  -> if smoke then icn_valid else icn_invalid
    | Unknown  -> if smoke then icn_valid else icn_unknown
    | Timeout | Stepout -> if smoke then icn_valid else icn_cut
    | Failed   -> icn_failed
    | Computing _ -> icn_running
  in fun w ->
    match Wpo.get_result w p , p with
    | { verdict=NoResult } , Qed -> icn_na
    | { verdict=NoResult } , Tactical ->
      begin
        match ProverScript.get w with
        | `None -> icn_na
        | `Script -> icn_stock "gtk-media-play"
        | `Proof -> icn_stock "gtk-edit"
        | `Saved -> icn_stock "gtk-file"
      end
    | result , _ ->
      icon_of_verdict ~smoke:(Wpo.is_smoke_test w) result.verdict

class pane (gprovers:GuiConfig.provers) =
  let model = new model in
  let list = new Wtable.list ~headers:true ~rules:true model#coerce in
  object(self)

    method coerce = list#coerce
    method reload = list#reload

    method add wpo =
      begin
        model#add wpo ;
        list#insert_row wpo ;
      end

    method size = model#size
    method index = model#index
    method get = model#get

    method update_all = list#update_all
    method update w = list#update_row w

    (* -------------------------------------------------------------------------- *)
    (* --- Prover Columns Management                                          --- *)
    (* -------------------------------------------------------------------------- *)

    val mutable provers : (VCS.prover * GTree.view_column) list = []

    method private prover_of_column c =
      let id = c#misc#get_oid in
      try Some(fst(List.find (fun (_,c0) -> id = c0#misc#get_oid) provers))
      with Not_found -> None

    method private column_of_prover p =
      try Some(snd(List.find (fun (p0,_) -> p=p0) provers))
      with Not_found -> None

    method private create_prover p =
      begin
        let title = VCS.title_of_prover p in
        let column = list#add_column_pixbuf ~title [] (render_prover_result p)
        in if p <> VCS.Qed then provers <- (p,column) :: provers
      end

    method private configure (dps:Why3.Whyconf.Sprover.t) =
      begin
        (* Removing Useless Columns *)
        List.iter
          (fun (vcs,column) ->
             match vcs with
             | VCS.Why3 p ->
               column#set_visible (Why3.Whyconf.Sprover.mem p dps) ;
               (* ignore (list#view#remove_column column) *)
             | _ -> ()
          ) provers ;
        (* Installing Missing Columns *)
        Why3.Whyconf.Sprover.iter
          (fun dp ->
             let prv = VCS.Why3 dp in
             match self#column_of_prover prv with
             | None -> self#create_prover prv
             | Some _ -> ()
          ) dps ;
      end

    initializer
      begin
        let render w =
          [`TEXT (Pretty_utils.to_string Wpo.pp_index w.po_idx)] in
        ignore (list#add_column_text ~title:"Module" [] render) ;
        let render w =
          [`TEXT (Pretty_utils.to_string Wpo.pp_title w)] in
        ignore (list#add_column_text ~title:"Goal" [] render) ;
        let render w = [`TEXT (Wpo.get_model w |> WpContext.MODEL.descr)] in
        ignore (list#add_column_text ~title:"Model" [] render) ;
        List.iter
          self#create_prover
          [ VCS.Qed ; VCS.Tactical ] ;
        ignore (list#add_column_empty) ;
        list#set_selection_mode `MULTIPLE ;
        gprovers#connect self#configure ;
        self#configure gprovers#get ;
      end

    method private on_cell f w c = f w (self#prover_of_column c)

    method on_click f = list#on_click (self#on_cell f)
    method on_double_click f = list#on_double_click (self#on_cell f)
    method on_right_click f = list#on_right_click (self#on_cell f)
    method on_selection f = list#on_selection (fun () -> f list#count_selected)
    method iter_selected = list#iter_selected
    method count_selected = list#count_selected

    method show w =
      let col = list#view#get_column 1 in
      list#set_focus w col

  end
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