package frama-c
Platform dedicated to the analysis of source code written in C
Install
Dune Dependency
Authors
-
MMichele Alberti
-
TThibaud Antignac
-
GGergö Barany
-
PPatrick Baudin
-
NNicolas Bellec
-
TThibaut Benjamin
-
AAllan Blanchard
-
LLionel Blatter
-
FFrançois Bobot
-
RRichard Bonichon
-
VVincent Botbol
-
QQuentin Bouillaguet
-
DDavid Bühler
-
ZZakaria Chihani
-
SSylvain Chiron
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
MMaxime Jacquemin
-
BBenjamin Jorge
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
RRemi Lazarini
-
TTristan Le Gall
-
KKilyan Le Gallic
-
JJean-Christophe Léchenet
-
MMatthieu Lemerre
-
DDara Ly
-
DDavid Maison
-
CClaude Marché
-
AAndré Maroneze
-
TThibault Martin
-
FFonenantsoa Maurica
-
MMelody Méaulle
-
BBenjamin Monate
-
YYannick Moy
-
PPierre Nigron
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
JJan Rochel
-
MMuriel Roger
-
CCécile Ruet-Cros
-
JJulien Signoles
-
NNicolas Stouls
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
frama-c-31.0-Gallium.tar.gz
sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567
doc/src/frama-c-metrics.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 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 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362
(**************************************************************************) (* *) (* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2025 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* 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). *) (* *) (**************************************************************************) (** This module defines abstraction for Metrics use *) module HalsteadMetricsGUI = struct let name = "Halstead" let display_result (main_ui:Design.main_window_extension_points) (parent_win:GPack.box) = try let padder = GBin.alignment ~padding:(5, 5, 15, 15) ~packing:parent_win#pack () in let box = GPack.vbox ~homogeneous:false () in padder#add (box:>GObj.widget); ignore(GMisc.label ~markup:(Printf.sprintf "<b>%s</b>" name) ~justify:`LEFT ~packing:box#pack ()); ignore(GMisc.separator `HORIZONTAL ~packing:box#pack ()); let metrics = Metrics__Metrics_cabs.Halstead.get_metrics () in let table_contents = Metrics__Metrics_cabs.Halstead.to_list metrics in Metrics_gui_panels.display_as_table table_contents box with | Ast.NoUntypedAst -> main_ui#error "Cannot compute Halstead metrics: untyped AST not present.\n\ It has been removed either by user request or \ by some AST transformation." let register main_ui = Metrics_gui_panels.register_metrics name (display_result main_ui) end module CyclomaticMetricsGUI = struct open Printer_tag open Visitor let name = "Cyclomatic" class cyclo_class ~libc (main_ui:Design.main_window_extension_points) = object(self) val mutable checked_fun = Kernel_function.dummy () method get_data = let checker = (new Metrics__Metrics_cilast.slocVisitor ~libc) in ignore (visitFramacGlobal (checker :> frama_c_visitor) (Kernel_function.get_global checked_fun)); checker#get_global_metrics (* 2 becomes "2*checker#funcs" in the general case *) method do_value (main_ui:Design.main_window_extension_points) loc (total:int) (valeur:int) (percent:float) = match loc with | PVDecl (Some kf,_,_) -> begin (* Get the global of this function *) let fname = Kernel_function.get_name kf in (* create a small results window *) let dialog = GWindow.window ~title:(Format.sprintf "Value analysis statistics of %s" fname) ~modal:false ~position:`CENTER_ON_PARENT ~border_width:3 ~resizable:true () in dialog#set_transient_for main_ui#main_window#as_window; let padder = GBin.alignment ~padding:(5, 0, 15, 15) ~packing:dialog#add () in let vbox = GPack.vbox () in padder#add (vbox:>GObj.widget); ignore (dialog#event#connect#delete ~callback:(fun _ -> dialog#misc#hide (); true)); ignore(GMisc.label ~markup:(Printf.sprintf "<b>%s</b>" fname) ~justify:`LEFT ~packing:vbox#pack ()); ignore(GMisc.separator `HORIZONTAL ~packing:vbox#pack ()); let metrics_data = [["total stmts";(string_of_int total)]; ["stmts analyzed";(string_of_int valeur)]; ["percentage of stmts covered"; (string_of_float percent)] ] in Metrics_gui_panels.display_as_table metrics_data vbox; let = GButton.button ~stock:`OK ~packing:vbox#pack () in close_button#set_border_width 10; ignore (close_button#connect#clicked ~callback:dialog#misc#hide); dialog#show () end | _ -> prerr_endline "no function" method do_cyclo (main_ui:Design.main_window_extension_points) = let fname = Kernel_function.get_name checked_fun in (* create a small results window *) let dialog = GWindow.window ~title:(Format.sprintf "Measures for %s" fname) ~modal:false ~position:`CENTER_ON_PARENT ~border_width:3 ~resizable:true () in dialog#set_transient_for main_ui#main_window#as_window; let padder = GBin.alignment ~padding:(5, 0, 15, 15) ~packing:dialog#add () in let vbox = GPack.vbox () in padder#add (vbox:>GObj.widget); ignore (dialog#event#connect#delete ~callback:(fun _ -> dialog#misc#hide (); true)); ignore(GMisc.label ~markup:(Printf.sprintf "<b>%s</b>" fname) ~justify:`LEFT ~packing:vbox#pack ()); ignore(GMisc.separator `HORIZONTAL ~packing:vbox#pack ()); let metrics_data = Metrics__Metrics_base.BasicMetrics.to_list self#get_data in Metrics_gui_panels.display_as_table metrics_data vbox; let = GButton.button ~stock:`OK ~packing:vbox#pack () in close_button#set_border_width 10; ignore (close_button#connect#clicked ~callback:dialog#misc#hide); dialog#show () (* callback of menu_item "Cyclo" *) method display_localizable localizable () = begin match localizable with | PVDecl (Some kf,_,_) -> (* Process only the function selected *) (* Get the global of this function *) checked_fun <- kf; self#do_cyclo main_ui; | _ -> () end method cyclo_selector (popup_factory:GMenu.menu GMenu.factory) main_ui ~ localizable = if button = 3 && Eva.Analysis.is_computed () then match localizable with | PVDecl (Some kf, _,_) -> let callback1 () = Metrics__Metrics_parameters.debug "cyclo_selector - callback"; self#display_localizable localizable () in let callback2 () = (* function selected is kf *) Metrics__Metrics_coverage.compute_coverage_by_fun (); (* Got a list of (kf,value,total,percent). Now let's scan this list *) try let valeur,total,percent = Metrics__Metrics_coverage.get_coverage kf in self#do_value main_ui localizable valeur total percent with Not_found -> () in begin ignore (popup_factory#add_item "Cyclomatic metrics" ~callback:callback1); ignore (popup_factory#add_item "Value metrics" ~callback:callback2) end | _ -> () initializer main_ui#register_source_selector self#cyclo_selector end let display_result ~libc (parent_win:GPack.box) = let padder = GBin.alignment ~padding:(5, 5, 15, 15) ~packing:parent_win#pack () in let box = GPack.vbox ~homogeneous:false () in padder#add (box:>GObj.widget); ignore(GMisc.label ~markup:(Printf.sprintf "<b>%s</b>" name) ~justify:`LEFT ~packing:box#pack ()); ignore(GMisc.separator `HORIZONTAL ~packing:box#pack ()); let metrics = Metrics__Metrics_cilast.get_global_metrics ~libc in let table_contents = Metrics__Metrics_base.BasicMetrics.to_list metrics in Metrics_gui_panels.display_as_table table_contents box let register ~libc main_ui = ignore (new cyclo_class ~libc main_ui); Metrics_gui_panels.register_metrics name (display_result ~libc) end (** GUI hooks value coverage *) module ValueCoverageGUI = struct open Cil_datatype open Gtk_helper let name = "Eva coverage" let result = ref None let highlight = ref false let update_filetree = ref (fun _ -> ()) let filetree_enabled = ref true let filetree_visible () = !filetree_enabled && Metrics__Metrics_coverage.is_computed_by_fun () (* TODO : Metrics data structure must be projectified ? *) let compute ~libc = begin match !result with | None -> Eva.Analysis.compute (); result := Some (Metrics__Metrics_coverage.compute ~libc) | Some _ -> () end; Metrics__Metrics_coverage.compute_coverage_by_fun (); !update_filetree `Contents; Option.get !result let decorate_filetree (main_ui: Design.main_window_extension_points) = let compute get = function | Cil_types.GFun ({Cil_types.svar = v }, _) -> begin try let kf = Globals.Functions.get v in get (Metrics__Metrics_coverage.get_coverage kf) with Not_found -> -1 end | _ -> -1 in let percentage (_, _, pct_covered) = truncate (100. -. pct_covered) in let number (total, value, _) = total - value in let number_total (total, _, _) = total in let text get = fun g -> let i = compute get g in if i < 0 then "" else string_of_int i in let sort get = fun g h -> Datatype.Int.compare (compute get g) (compute get h) in let refresh_percentage = main_ui#file_tree#append_text_column ~title:"Dead code %" ~tooltip:"Percentage of dead code in each function" ~visible:filetree_visible ~text:(text percentage) ~sort:(sort percentage) in let refresh_dead_stmts = main_ui#file_tree#append_text_column ~title:"Dead stmts" ~tooltip:"Number of dead statements in each function" ~visible:filetree_visible ~text:(text number) ~sort:(sort number) in let refresh_nb_stmts = main_ui#file_tree#append_text_column ~title:"Total stmts" ~tooltip:"Number of statements in each function" ~visible:filetree_visible ~text:(text number_total) ~sort:(sort number_total) in let refresh x = refresh_percentage x; refresh_dead_stmts x; refresh_nb_stmts x in update_filetree := refresh let () = Eva.Analysis.register_computation_hook (fun _ -> Metrics__Metrics_coverage.clear_coverage_by_fun (); !update_filetree `Visibility) (* Functions are highlighted using different colors according to the following scheme: - Both semantically and syntactically reachable functions are green; - Only syntactically reachable are yellow; - Unreachable (neither semantically nor syntactically) functions are in red (bad!) *) let highlighter buffer loc ~start ~stop = if !highlight then begin match !result with | None -> () | Some metrics -> begin let pure_syntactic = Varinfo.Set.diff metrics.syntactic metrics.semantic in let hilit color = let tag = make_tag buffer#buffer ~name:"metrics" [`BACKGROUND color] in apply_tag buffer#buffer tag start stop in let syn_hilit () = hilit "yellow" and sem_hilit () = hilit "green" and unseen_hilit () = hilit "red" in match loc with | Printer_tag.PVDecl(_, _, vi) -> if Ast_types.is_fun vi.vtype then begin if Varinfo.Set.mem vi pure_syntactic then syn_hilit () else if Varinfo.Set.mem vi metrics.semantic then sem_hilit () else unseen_hilit () end | _ -> () end end let display_result ~libc main_ui (parent_win:GPack.box) = let padder = GBin.alignment ~padding:(5, 5, 15, 15) ~packing:parent_win#pack () in let box = GPack.vbox ~homogeneous:false () in padder#add (box:>GObj.widget); ignore(GMisc.label ~markup:(Printf.sprintf "<b>%s</b>" name) ~justify:`LEFT ~packing:box#pack ()); ignore(GMisc.separator `HORIZONTAL ~packing:box#pack ()); let metrics = compute ~libc in let pcent = Metrics__Metrics_coverage.percent_coverage ~libc metrics in let progress_bar = GRange.progress_bar ~packing:box#pack () in progress_bar#set_fraction (pcent /. 100.0); ignore(GMisc.label ~markup:(Format.sprintf "%s%% functions reached" (Metrics__Metrics_base.float_to_string pcent)) ~justify:`LEFT ~packing:box#pack ()); let _ignore = Gtk_helper.on_bool box "Highlight results" (fun () -> !highlight) (fun b -> highlight := b; main_ui#rehighlight ()) in let _ignore = Gtk_helper.on_bool box "Show columns" ~tooltip:"Shows the columns related to dead code in the filetree." (fun () -> !filetree_enabled) (fun b -> filetree_enabled := b; !update_filetree `Visibility) in main_ui#rehighlight () let register ~libc main_ui = Design.register_reset_extension (fun _ -> result := None); main_ui#register_source_highlighter highlighter; let apply = Metrics__Metrics_parameters.ValueCoverage.get () in Metrics_gui_panels.register_metrics ~apply name (display_result ~libc main_ui); end let register_final ?(libc=Metrics__Metrics_parameters.Libc.get ()) main_ui = let box = Metrics_gui_panels.init_panel main_ui in Design.register_reset_extension Metrics_gui_panels.reset_panel; HalsteadMetricsGUI.register main_ui; CyclomaticMetricsGUI.register ~libc main_ui; ValueCoverageGUI.register ~libc main_ui; Metrics_gui_panels.coerce_panel_to_ui box main_ui let gui (main_ui:Design.main_window_extension_points) = main_ui#register_panel register_final let () = Design.register_extension gui; Design.register_extension ValueCoverageGUI.decorate_filetree
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>