(**************************************************************************)
(*                                                                        *)
(*  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