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
concurguiglobs.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 Callgraph
open Cil_datatype
open Cil_types
open Concurrency_main
exception No_value;;
(*this might be unnecessary if we include the Option library*)
let get_option ip =
match ip with
None -> raise No_value
| Some(e) -> e;;
(** Constants used during initialisation*)
let init_varinfo = Varinfo.dummy ;; (*initial variable*)
let init_fundec = Kernel_function.dummy ();; (*inital thread*)
let refresh = ref (true,true,true,false, false);; (*the GUI statemachine*)
(*The code's call graph*)
let cg = ref (None : callgraph option);;
(*Function to obtain a row from a Treeview model. *)
let get_t_row (model: GTree.model) col path =
let row = model#get_iter path in
let name = model#get ~row ~column:col in
name;;
(** Current variable to be passed to -var-overlap command line option*)
module LockedVar =
State_builder.Ref
(Varinfo)
(struct
let name = "Concurrency_gui.LockedVar"
let dependencies = []
let default () = init_varinfo
end);;
(** Holds current -var-overlap output*)
module VarOverlapSet_ref =
State_builder.Ref (*Tried Set_ref but it did not work*)
(Varinfo.Set)
(struct
let name = "Concurrency_gui. VarOverlapList"
let dependencies = []
let default () = Varinfo.Set.empty
end);;
(** List of currently selected threads to intersect*)
module SelectedThreads =
State_builder.List_ref
(Kernel_function)
(struct
let name = "Concurrency_gui.SelectedThreads"
let dependencies = []
end) ;;
(** Currently selected "main" thread to intersect*)
module SelectedMain =
State_builder.Ref
(Kernel_function)
(struct
let name = "Concurrency_gui.SelectedMain"
let dependencies = []
let default () = init_fundec
end) ;;
(** Holds all entry points detected*)
module AllEntryPoints =
State_builder.List_ref
(Kernel_function)
(struct
let name = "Concurrency_gui.AllEntryPoints"
let dependencies = []
end);;
(** Holds entry points selected by user - we can subsume this
* into AllEntryPoints if we use a (Kernel_function, bool) type
* where the second argument denotes show/hide.
*)
module FilteredEntryPoints =
State_builder.List_ref
(Kernel_function)
(struct
let name = "Concurrency_gui.FilteredEntryPoints"
let dependencies = []
end);;
module CurrentKinstr =
State_builder.Ref
(Kinstr)
(struct
let name = "Concurrency_gui.CurrentKinstr"
let dependencies = []
let default () = Kglobal
end);;
(** Holds current -access-for output*)
module AccessForList =
State_builder.List_ref
(Datatype.Make
(struct
include Datatype.Serializable_undefined
type t = Kernel_function.t * Kinstr.t * Kernel_function.t option * bool
let name = "Access for type"
(*dont know what reprs is - could be replicators??*)
let reprs = [(init_fundec, Kglobal, None, false)]
let mem_project = Datatype.never_any_project
end))
(struct
let name = "Concurrency_gui. AccessForList"
let dependencies = []
end);;
(**
* Initialises the concurrency gui
*)
let start_concurrency () =
cg := Some(computeGraph (Ast.get()));
let eps = computeEntryPoints (get_option !cg) in
SelectedMain.set init_fundec;
LockedVar.set init_varinfo;
SelectedThreads.set [];
CurrentKinstr.set Kglobal;
(*Set the identified entry point functions*)
AllEntryPoints.set eps;
FilteredEntryPoints.set eps;
VarOverlapSet_ref.set Varinfo.Set.empty;
AccessForList.set [];;
(**
* Resets the concurrency gui without affecting the entry point lists
*)
let reset_concurrency () =
SelectedMain.set init_fundec;
LockedVar.set init_varinfo;
SelectedThreads.set [];
CurrentKinstr.set Kglobal;
VarOverlapSet_ref.set Varinfo.Set.empty;
AccessForList.set [];;