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
accessesgui.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 show variable accesses locations.
*)
class vAccWindow mainui =
object(slf)
val mutable access_display = (None : GWindow.window option)
val m_mainui = mainui
val mutable m_acc_tree_columns = ([] : string GTree.column list)
val mutable m_acc_tree = (None : GTree.list_store option)
val mutable m_acc_adjust = (None : GData.adjustment option)
(*Populates the tree view with the current
functions to be displayed.*)
method private populate_tree
(pa_tree : GTree.list_store)
(columns_list : string GTree.column list)
(pa_adjust : GData.adjustment) =
begin
match columns_list with
col0::col1::col2::col3::col4::_ ->
begin
let add_acc_to_tree nn (ep, i, f, b) =
let fname = match f with
Some(f) -> Kernel_function.get_name f
| None -> "(global)"
in
let iter = pa_tree#append () in
pa_tree#set ~row:iter ~column:col0 (Kernel_function.get_name ep);
pa_tree#set ~row:iter ~column:col1 (if b then "Write" else "Read");
pa_tree#set ~row:iter ~column:col2 (Pretty_utils.to_string Printer.pp_location (Kinstr.loc i));
pa_tree#set ~row:iter ~column:col3 fname;
pa_tree#set ~row:iter ~column:col4 (string_of_int nn);
nn+1;
in
pa_tree#clear ();
ignore (List.fold_left add_acc_to_tree 0 (AccessForList.get ()));
pa_adjust#set_bounds ~upper:(float_of_int (List.length (AccessForList.get ()))) ()
end
| _ -> ()
end
method private create_acc_display () =
begin
access_display <- Some(GWindow.window ~title:"Current variable RoW"());
ignore((get_option access_display)#connect#destroy ( fun () -> access_display <- None));
let v_box = GPack.vbox ~packing:(get_option access_display)#add () in
let h2_box = GPack.hbox ~packing:v_box#add () in
let acc_tree_columns = new GTree.column_list in
let acc_tree_column0 = acc_tree_columns#add Gobject.Data.string in
let acc_tree_column1 = acc_tree_columns#add Gobject.Data.string in
let acc_tree_column2 = acc_tree_columns#add Gobject.Data.string in
let acc_tree_column3 = acc_tree_columns#add Gobject.Data.string in
let acc_tree_column4 = acc_tree_columns#add Gobject.Data.string in
let acc_tree = GTree.list_store acc_tree_columns in
let acc_view = GTree.view ~model:acc_tree ~height:360 ~packing:h2_box#pack () in
acc_view#selection#set_mode `SINGLE;
let acc_col0 = GTree.view_column
~title: "From"
~renderer: (GTree.cell_renderer_text [], [("text", acc_tree_column0)]) ()
in
let acc_col1 = GTree.view_column
~title: "R/W"
~renderer: (GTree.cell_renderer_text [], [("text", acc_tree_column1)]) ()
in
let acc_col2 = GTree.view_column
~title: "Location"
~renderer: (GTree.cell_renderer_text [], [("text", acc_tree_column2)]) ()
in
let acc_col3 = GTree.view_column
~title: "Function"
~renderer: (GTree.cell_renderer_text [], [("text", acc_tree_column3)]) ()
in
let acc_col4 = GTree.view_column
~title: "ID"
~renderer: (GTree.cell_renderer_text [], [("text", acc_tree_column4)]) ()
in
ignore (acc_view#append_column acc_col0);
ignore (acc_view#append_column acc_col1);
ignore (acc_view#append_column acc_col2);
ignore (acc_view#append_column acc_col3);
ignore (acc_view#append_column acc_col4);
let acc_adjust = GData.adjustment () in
(*create a scroll bar*)
ignore(GRange.scrollbar `VERTICAL ~adjustment:acc_adjust ~packing:h2_box#pack ());
acc_view#set_vadjustment acc_adjust;
m_acc_tree <- Some(acc_tree);
m_acc_tree_columns <- [acc_tree_column0;
acc_tree_column1;
acc_tree_column2;
acc_tree_column3;
acc_tree_column4];
m_acc_adjust <- Some(acc_adjust);
(*Selects a row as var of interest *)
let select_kloc () =
let selected_rows = acc_view#selection#get_selected_rows in
if (List.length selected_rows) > 0 then
let model = acc_view#model in
let lid = int_of_string (get_t_row model acc_tree_column4 (List.hd selected_rows)) in
let (_, b, _, _) = List.nth (AccessForList.get ()) lid in
match b with
Kstmt(st) -> (CurrentKinstr.set b; m_mainui#view_stmt st; m_mainui#rehighlight ();)
| Kglobal -> ()
else
()
in
ignore(acc_view#connect#cursor_changed select_kloc);
slf#populate_tree acc_tree m_acc_tree_columns acc_adjust;
(get_option access_display)#show ()
end
method show_acc () =
begin
match access_display with
Some(e) ->
ignore(e#present ())
| None ->
slf#create_acc_display ()
end
method refresh () =
begin
match (access_display, m_acc_tree , m_acc_adjust) with
(Some(_), Some(b), Some(c)) ->
slf#populate_tree b m_acc_tree_columns c;
| _ -> ()
end
end