https://bitbucket.org/adelard/simple-concurrency
Tip revision: cd7dfa9b13e79137daa54446067371af0a68515d authored by Dan Sheridan on 27 February 2015, 15:32:58 UTC
Change -accesses-for to report accesses from the "main" entry point even if it is not explicitly listed in -threads; this better matches the behaviour of -var-overlap.
Change -accesses-for to report accesses from the "main" entry point even if it is not explicitly listed in -threads; this better matches the behaviour of -var-overlap.
Tip revision: cd7dfa9
vappgui.ml
(**************************************************************************)
(* *)
(* This file is part of the Concurrency Plugin for Frama-C *)
(* *)
(* Copyright (C) 2013 *)
(* Adelard LLP *)
(* CINIF (Control and Instrumentation Nuclear Industry Forum) *)
(* *)
(* 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 3. *)
(* *)
(* 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 v3 *)
(* for more details (enclosed in the file ./LGPLv3). *)
(* *)
(**************************************************************************)
open Concurguiglobs
open Cil_datatype
open Cil_types
(**
* A form to list variable information.
*)
class vAppWindow =
object(slf)
val mutable var_overlap_display = (None : GWindow.window option)
val mutable vapp_tree_columns = ([] : string GTree.column list)
val mutable g_vapp_tree = (None : GTree.list_store option)
val mutable m_vapp_adjust = (None : GData.adjustment option)
(*Populates the tree view with the current
functionsvariables to be displayed.*)
method private populate_tree
(vapp_tree : GTree.list_store)
(columns_list : string GTree.column list)
(vapp_adjust : GData.adjustment) =
begin
match columns_list with
col0::col1::col2::col3::_ ->
begin
let add_vapp_to_tree vi =
let vi_storage_class = (match vi.vstorage with
NoStorage -> if vi.vglob then "(global)" else "(local)"
| Static -> "(static)"
| Register -> "(register)"
| Extern ->
try
(
let _ = Globals.Functions.get vi in
"(extern function)"
)
with Not_found -> "(extern)")
in
(*Cil.bytesSizeOf is machine dependent so use frama-c-gui
-machdep x86_16 for 16bit architecture*)
let vi_size = (try string_of_int(Cil.bytesSizeOf vi.vtype)
with
Cil.SizeOfError (_,_) -> "(unknown)")
in
let iter = vapp_tree#append () in
Format.fprintf Format.str_formatter "%a " Printer.pp_typ vi.vtype;
vapp_tree#set ~row:iter ~column:col0 vi_storage_class;
vapp_tree#set ~row:iter ~column:col1 (Format.flush_str_formatter ());
vapp_tree#set ~row:iter ~column:col2 vi_size;
vapp_tree#set ~row:iter ~column:col3 vi.vname;
in
vapp_tree#clear ();
Varinfo.Set.iter add_vapp_to_tree (VarOverlapSet_ref.get ());
vapp_adjust#set_bounds
~upper:(float_of_int (Varinfo.Set.cardinal (VarOverlapSet_ref.get ()))) ();
end
| _ -> ()
end
(**
* Creates the var-overlap display window and populates
*)
method private create_var_overlap_display () =
begin
var_overlap_display <- Some(GWindow.window ~title:"Shared variable details"());
ignore((get_option var_overlap_display)#connect#destroy (fun () -> var_overlap_display <- None));
let v_box = GPack.vbox ~packing:(get_option var_overlap_display)#add () in
let h2_box = GPack.hbox ~packing:v_box#add () in
let vapp_columns = new GTree.column_list in
let vapp_tree_column0 = vapp_columns#add Gobject.Data.string in
let vapp_tree_column1 = vapp_columns#add Gobject.Data.string in
let vapp_tree_column2 = vapp_columns#add Gobject.Data.string in
let vapp_tree_column3 = vapp_columns#add Gobject.Data.string in
let vapp_tree = GTree.list_store vapp_columns in
let vapp_view = GTree.view ~model:vapp_tree ~height:360 ~packing:h2_box#pack () in
(*configure the columns*)
let vapp_col0 = GTree.view_column
~title: "Storage class"
~renderer: (GTree.cell_renderer_text [], [("text", vapp_tree_column0)]) ()
in
let vapp_col1 = GTree.view_column
~title: "Type"
~renderer: (GTree.cell_renderer_text [], [("text", vapp_tree_column1)]) ()
in
let vapp_col2 = GTree.view_column
~title: "Size"
~renderer: (GTree.cell_renderer_text [], [("text", vapp_tree_column2)]) ()
in
let vapp_col3 = GTree.view_column
~title: "Name"
~renderer: (GTree.cell_renderer_text [], [("text", vapp_tree_column3)]) ()
in
let vapp_adjust = GData.adjustment () in
(*create a scroll bar*)
ignore(GRange.scrollbar `VERTICAL ~adjustment:vapp_adjust ~packing:h2_box#pack ());
vapp_view#selection#set_mode `SINGLE;
vapp_view#set_vadjustment vapp_adjust;
g_vapp_tree <- Some(vapp_tree);
m_vapp_adjust <- Some(vapp_adjust);
vapp_tree_columns <- [vapp_tree_column0;
vapp_tree_column1;
vapp_tree_column2;
vapp_tree_column3];
ignore (vapp_view#append_column vapp_col0);
ignore (vapp_view#append_column vapp_col1);
ignore (vapp_view#append_column vapp_col2);
ignore (vapp_view#append_column vapp_col3);
(* Selects a row as var of interest *)
let select_lockedvar () =
let selected_rows = vapp_view#selection#get_selected_rows in
if (List.length selected_rows) > 0 then
(let model = vapp_view#model in
let vname = (get_t_row model vapp_tree_column3 (List.hd selected_rows)) in
try
LockedVar.set (Globals.Vars.find_from_astinfo vname VGlobal);
let (a, b, _, _, h) = !refresh in
refresh := (a, b, true, true, h)
with Not_found -> ()
)
in
ignore(vapp_view#connect#cursor_changed select_lockedvar);
slf#populate_tree vapp_tree vapp_tree_columns vapp_adjust;
(get_option var_overlap_display)#show ()
end
method show_vapp () =
begin
match var_overlap_display with
Some(e) ->
ignore(e#present ())
| None ->
slf#create_var_overlap_display ()
end
method refresh () =
begin
match (var_overlap_display, g_vapp_tree, m_vapp_adjust)
with
(Some(_),Some(b),Some(c)) ->
slf#populate_tree b vapp_tree_columns c
| _ -> ()
end
end