From c496b75655c29b9b473ad6c7ec1f7502cc99b8a7 Mon Sep 17 00:00:00 2001
From: Benjamin Monate <benjamin.monate@cea.fr>
Date: Fri, 30 Nov 2007 13:04:09 +0000
Subject: [PATCH] project for Alarms
---
Makefile.in | 10 ++++++----
cil/ocamlutil/cilutil.ml | 8 ++++++++
cil/ocamlutil/cilutil.mli | 2 ++
src/kernel/alarms.ml | 31 ++++++++++++++++++++++---------
src/kernel/alarms.mli | 4 +++-
src/kernel/boot.ml | 6 +++++-
src/kernel/cilE.ml | 9 +--------
src/kernel/cilE.mli | 3 ---
src/kernel/computation.ml | 4 ++--
src/kernel/datatype.ml | 4 ++--
src/kernel/datatype.mli | 4 ++--
src/kernel/db.mli | 7 +++----
src/kernel/project.mli | 4 ++--
src/memory_state/cvalue_type.ml | 6 +++---
src/pdg/build.ml | 10 +++++-----
src/pdg/marks.ml | 10 +++++-----
src/slicing/printSlice.ml | 2 +-
src/slicing/register.ml | 8 ++++----
src/slicing/slicingMacros.ml | 6 +++---
src/slicing/slicingProject.ml | 2 +-
src/slicing_types/slicingTypes.ml | 4 ++--
src/value/eval.ml | 10 ++++++----
22 files changed, 88 insertions(+), 66 deletions(-)
diff --git a/Makefile.in b/Makefile.in
index 802008d92e1..30765326545 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -522,12 +522,14 @@ MODULES_TODOC += src/memory_state/widen.ml \
# modules to be linked before kernel and plugin type definitions,
# e.g. generic modules and type definitions
ACMO = src/kernel/version.cmo \
- src/kernel/alarms.cmo src/kernel/cilE.cmo \
- src/misc/utils.cmo src/kernel/ast_info.cmo \
+ src/misc/utils.cmo \
src/misc/qstack.cmo src/misc/hook.cmo \
+ src/kernel/kind.cmo src/kernel/project.cmo \
+ src/kernel/datatype.cmo src/kernel/kernel_datatype.cmo \
+ src/kernel/computation.cmo \
+ src/kernel/alarms.cmo src/kernel/cilE.cmo \
+ src/kernel/ast_info.cmo \
src/misc/mergemap.cmo \
- src/kernel/kind.cmo src/kernel/project.cmo src/kernel/datatype.cmo \
- src/kernel/kernel_datatype.cmo src/kernel/computation.cmo \
src/kernel/cil_state.cmo \
src/ai/my_bigint.cmo \
src/ai/abstract_interp.cmo \
diff --git a/cil/ocamlutil/cilutil.ml b/cil/ocamlutil/cilutil.ml
index 41eff16da38..8485726598b 100755
--- a/cil/ocamlutil/cilutil.ml
+++ b/cil/ocamlutil/cilutil.ml
@@ -1004,6 +1004,14 @@ module StmtHashtbl = struct
iter (fun k v -> Format.fprintf fmt "%d; " k.sid) s
end
+module VarinfoHashtbl =
+ Hashtbl.Make(struct
+ type t = varinfo
+ let compare v1 v2 = Pervasives.compare v1.vid v2.vid
+ let hash v1 = v1.vid
+ let equal v1 v2 = v1.vid = v2.vid
+ end)
+
let flush_all () =
Format.printf "@?";
Format.eprintf "@?"
diff --git a/cil/ocamlutil/cilutil.mli b/cil/ocamlutil/cilutil.mli
index 3f319a3f101..01a5268ef37 100644
--- a/cil/ocamlutil/cilutil.mli
+++ b/cil/ocamlutil/cilutil.mli
@@ -456,6 +456,8 @@ module StmtComparable : Graph.Sig.COMPARABLE with type t = Cil_types.stmt
module StmtHashtbl : sig include Hashtbl.S with type key = Cil_types.stmt
val pretty : Format.formatter -> 'a t -> unit
end
+
+module VarinfoHashtbl : Hashtbl.S with type key = Cil_types.varinfo
val printStages : bool ref
diff --git a/src/kernel/alarms.ml b/src/kernel/alarms.ml
index 021c201eaad..7717336aeda 100644
--- a/src/kernel/alarms.ml
+++ b/src/kernel/alarms.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(* $Id: alarms.ml,v 1.7 2007-11-28 16:34:45 uid568 Exp $ *)
+(* $Id: alarms.ml,v 1.8 2007-11-30 13:04:09 uid528 Exp $ *)
open Cil_types
open Cil
@@ -51,14 +51,28 @@ module AlarmSet =
(*WILL PROBABLY LOOP ON TYPES*)
end)
-let (tbl:AlarmSet.t InstrHashtbl.t) = InstrHashtbl.create 7
+(*let (tbl:AlarmSet.t InstrHashtbl.t) = InstrHashtbl.create 7*)
+
+module S = Project.Datatype.PersistentDummy(AlarmSet)
+
+module Alarms =
+ Computation.InstrHashtbl
+ (S)
+ (struct
+ let name =
+ Project.Computation.Name.make "alarms"
+ let dependencies = []
+ let size = 7
+ end)
+
+let self = Alarms.self
let register ki t formula =
try
let to_add = t,formula in
- let old = InstrHashtbl.find tbl ki in
+ let old = Alarms.find ki in
if AlarmSet.mem to_add old then false
- else (InstrHashtbl.add tbl ki (AlarmSet.add to_add old);
+ else (Alarms.add ki (AlarmSet.add to_add old);
(*(match ki with
|Cil_types.Kstmt k ->
Format.eprintf "Got Id:%d@." k.Cil_types.sid
@@ -72,19 +86,18 @@ let register ki t formula =
Format.eprintf "Got Id:%d@." k.Cil_types.sid
| _ -> Format.eprintf "Got GLOB@."
);*)
- InstrHashtbl.add tbl ki (AlarmSet.singleton (t,formula));
+ Alarms.add ki (AlarmSet.singleton (t,formula));
true
-let clear () = InstrHashtbl.clear tbl
+let clear () = Alarms.clear ()
let fold f acc =
- InstrHashtbl.fold
+ Alarms.fold
(fun ki set acc -> AlarmSet.fold (fun v acc -> f ki v acc) set acc)
- tbl
acc
let fold_kinstr ki f acc =
- let s = InstrHashtbl.find tbl ki in
+ let s = Alarms.find ki in
AlarmSet.fold f s acc
(*
diff --git a/src/kernel/alarms.mli b/src/kernel/alarms.mli
index d1054a3764d..908b78be89f 100644
--- a/src/kernel/alarms.mli
+++ b/src/kernel/alarms.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(* $Id: alarms.mli,v 1.5 2007-11-28 16:34:45 uid568 Exp $ *)
+(* $Id: alarms.mli,v 1.6 2007-11-30 13:04:09 uid528 Exp $ *)
type t =
| Division_alarm
@@ -33,6 +33,8 @@ val clear: unit -> unit
val fold: (Cil_types.kinstr -> (t*Cil_types.code_annotation) -> 'a -> 'a) -> 'a -> 'a
val fold_kinstr: Cil_types.kinstr -> ((t*Cil_types.code_annotation) -> 'a -> 'a) -> 'a -> 'a
+val self: Project.Computation.t
+
(*
Local Variables:
compile-command: "LC_ALL=C make -C ../.. -j"
diff --git a/src/kernel/boot.ml b/src/kernel/boot.ml
index 40d6439a30a..37ea80fc222 100644
--- a/src/kernel/boot.ml
+++ b/src/kernel/boot.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(* $Id: boot.ml,v 1.5 2007-11-28 16:34:45 uid568 Exp $ *)
+(* $Id: boot.ml,v 1.6 2007-11-30 13:04:09 uid528 Exp $ *)
(** Boot Frama-c. *)
@@ -34,6 +34,10 @@ let () =
Cil.useLogicalOperators := false; (* do not use lazy LAND and LOR *)
Pretty.flushOften := true
+(* Additional internal state dependencies *)
+let () =
+ Project.Computation.add_dependency Alarms.self Db.Value.self
+
let go () =
if Cmdline.Debug.get () > 0 then begin
(* Dump dependencies graph *)
diff --git a/src/kernel/cilE.ml b/src/kernel/cilE.ml
index a098e1441f2..d056e9c1b2a 100644
--- a/src/kernel/cilE.ml
+++ b/src/kernel/cilE.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(* $Id: cilE.ml,v 1.31 2007-11-28 16:34:45 uid568 Exp $ *)
+(* $Id: cilE.ml,v 1.32 2007-11-30 13:04:09 uid528 Exp $ *)
(* Cil extensions *)
open Cil_types
open Cil
@@ -293,13 +293,6 @@ let warn_index msg =
let warn_mem_read = warn_mem "read"
let warn_mem_write = warn_mem "write"
-module VarinfoHashtbl =
- Hashtbl.Make(struct
- type t = varinfo
- let compare v1 v2 = Pervasives.compare v1.vid v2.vid
- let hash v1 = v1.vid
- let equal v1 v2 = v1.vid = v2.vid
- end)
(*
Local Variables:
compile-command: "LC_ALL=C make -C ../.. -j"
diff --git a/src/kernel/cilE.mli b/src/kernel/cilE.mli
index f1050e6fdc8..bf4fd466082 100644
--- a/src/kernel/cilE.mli
+++ b/src/kernel/cilE.mli
@@ -48,6 +48,3 @@ val warn_shift : int -> unit
val warn_mem_read : unit -> unit
val warn_mem_write : unit -> unit
val warn_index : string -> unit
-
-
-module VarinfoHashtbl : (Hashtbl.S with type key = Cil_types.varinfo)
diff --git a/src/kernel/computation.ml b/src/kernel/computation.ml
index 9fe8189e3a7..6db1c640b60 100644
--- a/src/kernel/computation.ml
+++ b/src/kernel/computation.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(* $Id: computation.ml,v 1.7 2007-11-28 16:34:45 uid568 Exp $ *)
+(* $Id: computation.ml,v 1.8 2007-11-30 13:04:09 uid528 Exp $ *)
module type NAME_DPDS = sig
val name: Project.Computation.Name.t
@@ -103,7 +103,7 @@ end
module IntHashtbl = Make_Hashtbl(Inthash)
module InstrHashtbl = Make_Hashtbl(Cil.InstrHashtbl)
module StmtHashtbl = Make_Hashtbl(Cilutil.StmtHashtbl)
-module VarinfoHashtbl = Make_Hashtbl(CilE.VarinfoHashtbl)
+module VarinfoHashtbl = Make_Hashtbl(Cilutil.VarinfoHashtbl)
module Hashtbl(Key:Hashtbl.HashedType) = Make_Hashtbl(Hashtbl.Make(Key))
module type REF_INPUT = sig
diff --git a/src/kernel/datatype.ml b/src/kernel/datatype.ml
index 0a7dd1c5c55..e1d97cbf5f8 100644
--- a/src/kernel/datatype.ml
+++ b/src/kernel/datatype.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(* $Id: datatype.ml,v 1.7 2007-11-28 16:34:45 uid568 Exp $ *)
+(* $Id: datatype.ml,v 1.8 2007-11-30 13:04:09 uid528 Exp $ *)
module type INPUT = sig
include Project.Datatype.INPUT
@@ -58,7 +58,7 @@ module Make_Hashtbl(H: HASHTBL)(Data:INPUT)(Info:Signature.SIZE) =
module IntHashtbl = Make_Hashtbl(Inthash)
module InstrHashtbl = Make_Hashtbl(Cil.InstrHashtbl)
module StmtHashtbl = Make_Hashtbl(Cilutil.StmtHashtbl)
-module VarinfoHashtbl = Make_Hashtbl(CilE.VarinfoHashtbl)
+module VarinfoHashtbl = Make_Hashtbl(Cilutil.VarinfoHashtbl)
module Ref(Data:INPUT) =
Project.Datatype.Register
diff --git a/src/kernel/datatype.mli b/src/kernel/datatype.mli
index 49b186ce0a5..eecf44459b6 100644
--- a/src/kernel/datatype.mli
+++ b/src/kernel/datatype.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(* $Id: datatype.mli,v 1.6 2007-11-28 16:34:45 uid568 Exp $ *)
+(* $Id: datatype.mli,v 1.7 2007-11-30 13:04:09 uid528 Exp $ *)
(** Datatype implementations and builders.
Provide ways to implement signature [Project.Datatype.OUTPUT] without
@@ -61,7 +61,7 @@ module StmtHashtbl(Data:INPUT)(Info:Signature.SIZE) :
Project.Datatype.OUTPUT with type t = Data.t Cilutil.StmtHashtbl.t
module VarinfoHashtbl(Data:INPUT)(Info:Signature.SIZE) :
- Project.Datatype.OUTPUT with type t = Data.t CilE.VarinfoHashtbl.t
+ Project.Datatype.OUTPUT with type t = Data.t Cilutil.VarinfoHashtbl.t
(** Sub-signature of [Hashtbl.S]. *)
module type HASHTBL = sig
diff --git a/src/kernel/db.mli b/src/kernel/db.mli
index a66ce41481a..fa23d12c310 100644
--- a/src/kernel/db.mli
+++ b/src/kernel/db.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(* $Id: db.mli,v 1.329 2007-11-28 16:34:45 uid568 Exp $ *)
+(* $Id: db.mli,v 1.330 2007-11-30 13:04:09 uid528 Exp $ *)
(** Database in which plugins are registered. *)
@@ -434,9 +434,8 @@ module Postdominators: sig
exception Top
(** Used for {!stmt_postdominators} when the postdominators of a statement
- have not been computed. It means that there is no path from this
- statement to the function exit (infinite loop). Maybe we should do
- something for this, but what? *)
+ cannot be computed. It means that there is no path from this
+ statement to the function return. *)
val stmt_postdominators: (kernel_function -> stmt -> Cilutil.StmtSet.t) ref
(** @raise Top (see above) *)
diff --git a/src/kernel/project.mli b/src/kernel/project.mli
index 2c3e36b6a40..85d53ddec38 100644
--- a/src/kernel/project.mli
+++ b/src/kernel/project.mli
@@ -20,9 +20,9 @@
(* *)
(**************************************************************************)
-(* $Id: project.mli,v 1.51 2007-11-28 16:34:45 uid568 Exp $ *)
+(* $Id: project.mli,v 1.52 2007-11-30 13:04:09 uid528 Exp $ *)
-(** Gestion of projects.
+(** Projects management.
A project groups together all the internal states of Frama-C. An internal
state is roughly the result of a computation which depends of an AST. It is
diff --git a/src/memory_state/cvalue_type.ml b/src/memory_state/cvalue_type.ml
index 1c1dfe07ed9..30c5601c311 100644
--- a/src/memory_state/cvalue_type.ml
+++ b/src/memory_state/cvalue_type.ml
@@ -504,16 +504,16 @@ module Partial_lmap = Lmap.Make_LOffset(V)(V_Offsetmap_ext)
module Default_offsetmap =
struct
- let initialized_var_table = CilE.VarinfoHashtbl.create 17
+ let initialized_var_table = Cilutil.VarinfoHashtbl.create 17
let create_initialized_var varinfo validity initinfo =
- CilE.VarinfoHashtbl.add initialized_var_table varinfo initinfo;
+ Cilutil.VarinfoHashtbl.add initialized_var_table varinfo initinfo;
Base.create_initialized varinfo validity
let default_offsetmap varid = match varid with
| Base.Initialized_Var (v,_) ->
- (try CilE.VarinfoHashtbl.find initialized_var_table v
+ (try Cilutil.VarinfoHashtbl.find initialized_var_table v
with Not_found ->
V_Offsetmap.empty)
| Base.Var _ | Base.Null | Base.Uninitialized
diff --git a/src/pdg/build.ml b/src/pdg/build.ml
index eeea8eecfab..4d0e271fb0d 100644
--- a/src/pdg/build.ml
+++ b/src/pdg/build.ml
@@ -22,7 +22,7 @@
(* *)
(**************************************************************************)
-(* $Id: build.ml,v 1.76 2007-11-28 16:34:45 uid568 Exp $ *)
+(* $Id: build.ml,v 1.77 2007-11-30 13:04:09 uid528 Exp $ *)
(** Build graphs (PDG) for the function
(see module {!module: Build.BuildPdg})
@@ -291,7 +291,7 @@ module BuildPdg : sig
ctrl_dpds : (SimpleNodeSet.t) Cil.InstrHashtbl.t ;
(** The nodes to which each stmt control-depend on.
* The links will be added in the graph at the end. *)
- decl_nodes : t_node CilE.VarinfoHashtbl.t ;
+ decl_nodes : t_node Cilutil.VarinfoHashtbl.t ;
(** map between declaration nodes and the variables
to build the dependencies. *)
}
@@ -311,7 +311,7 @@ module BuildPdg : sig
graph = graph; states = states; index = index;
topinput = None; other_inputs = [];
ctrl_dpds = Cil.InstrHashtbl.create nb_stmts ;
- decl_nodes = CilE.VarinfoHashtbl.create 10 ;
+ decl_nodes = Cilutil.VarinfoHashtbl.create 10 ;
}
let get_kf pdg = pdg.fct
@@ -387,7 +387,7 @@ module BuildPdg : sig
let decl_var pdg var =
let key = Key.decl_var_key var in
let new_node = add_elem pdg key in
- CilE.VarinfoHashtbl.add pdg.decl_nodes var new_node;
+ Cilutil.VarinfoHashtbl.add pdg.decl_nodes var new_node;
new_node
let get_var_base zone =
@@ -463,7 +463,7 @@ module BuildPdg : sig
let add_decl_dpds pdg node dpd_kind varset =
let add_dpd var =
try
- let var_decl_node = CilE.VarinfoHashtbl.find pdg.decl_nodes var in
+ let var_decl_node = Cilutil.VarinfoHashtbl.find pdg.decl_nodes var in
add_dpd pdg node dpd_kind var_decl_node
with Not_found -> ()
in Cil.VarinfoSet.iter add_dpd varset
diff --git a/src/pdg/marks.ml b/src/pdg/marks.ml
index 307b976dbdc..9a8278b039d 100644
--- a/src/pdg/marks.ml
+++ b/src/pdg/marks.ml
@@ -120,26 +120,26 @@ module F_Proj (C : PdgMarks.T_Config) :
type t_mark = C.M.t
type t_fct = (C.M.t, C.M.t_call_info) PdgIndex.FctIndex.t
type t_fct_info = F.t
- type t = t_fct_info CilE.VarinfoHashtbl.t
+ type t = t_fct_info Cilutil.VarinfoHashtbl.t
type request = (PdgTypes.Pdg.t * (PdgTypes.Node.t * F.t_mark) list)
- let empty = CilE.VarinfoHashtbl.create 10
+ let empty = Cilutil.VarinfoHashtbl.create 10
let pdg_fvar pdg = PdgTypes.Pdg.get_var_fct pdg
let find_marks proj fct_var =
- try let f = CilE.VarinfoHashtbl.find proj fct_var in Some (F.get_idx f)
+ try let f = Cilutil.VarinfoHashtbl.find proj fct_var in Some (F.get_idx f)
with Not_found -> None
let get proj pdg =
let fct_var = pdg_fvar pdg in
- try CilE.VarinfoHashtbl.find proj fct_var
+ try Cilutil.VarinfoHashtbl.find proj fct_var
with Not_found ->
let kf = Globals.Functions.get fct_var in
let pdg = !Db.Pdg.get kf in
let info = F.create pdg in
- CilE.VarinfoHashtbl.add proj fct_var info;
+ Cilutil.VarinfoHashtbl.add proj fct_var info;
info
(** Add the marks to the pdg nodes.
diff --git a/src/slicing/printSlice.ml b/src/slicing/printSlice.ml
index 374dd935900..2e44d120085 100644
--- a/src/slicing/printSlice.ml
+++ b/src/slicing/printSlice.ml
@@ -191,7 +191,7 @@ module PrintProject = struct
let do_ff ff = List.iter (do_edge (Slice ff)) ff.T.ff_called_by
in List.iter do_ff (M.fi_slices fi)
in
- CilE.VarinfoHashtbl.iter do_f proj.T.functions
+ Cilutil.VarinfoHashtbl.iter do_f proj.T.functions
let iter_edges_actions f proj =
let rec do_act_edge n rq_list = match rq_list with
diff --git a/src/slicing/register.ml b/src/slicing/register.ml
index 748d04b8515..1def8959426 100644
--- a/src/slicing/register.ml
+++ b/src/slicing/register.ml
@@ -252,19 +252,19 @@ let merge_db_select db_select1 db_select2 =
let select = merge_select select1 select2 in
(fvar, select)
-let empty_selects () = CilE.VarinfoHashtbl.create 7
+let empty_selects () = Cilutil.VarinfoHashtbl.create 7
let add_to_selects db_select hsel =
let vf, select = db_select in
let select =
- try let old_selection = CilE.VarinfoHashtbl.find hsel vf in
+ try let old_selection = Cilutil.VarinfoHashtbl.find hsel vf in
merge_select old_selection select
with Not_found -> select
- in CilE.VarinfoHashtbl.replace hsel vf select
+ in Cilutil.VarinfoHashtbl.replace hsel vf select
let fold_selects f hsel acc =
let dof v sel acc = f (v, sel) acc in
- CilE.VarinfoHashtbl.fold dof hsel acc
+ Cilutil.VarinfoHashtbl.fold dof hsel acc
let iter_selects f hsel = fold_selects (fun s _ -> f s) hsel ()
diff --git a/src/slicing/slicingMacros.ml b/src/slicing/slicingMacros.ml
index 7f9e475f1c3..55faaa47c57 100644
--- a/src/slicing/slicingMacros.ml
+++ b/src/slicing/slicingMacros.ml
@@ -94,7 +94,7 @@ let ff_svar ff = fi_svar (ff.T.ff_fct)
let get_kf_fi proj kf =
let fct_var = Kernel_function.get_vi kf in
try
- let fi = CilE.VarinfoHashtbl.find proj.T.functions fct_var in fi
+ let fi = Cilutil.VarinfoHashtbl.find proj.T.functions fct_var in fi
with Not_found ->
let fi_def, is_def =
try let def = Kernel_function.get_definition kf in Some def, true
@@ -110,11 +110,11 @@ let get_kf_fi proj kf =
T.fi_next_ff_num = 1;
T.f_called_by = [] }
in
- CilE.VarinfoHashtbl.add proj.T.functions fct_var new_fi;
+ Cilutil.VarinfoHashtbl.add proj.T.functions fct_var new_fi;
new_fi
let fold_fi f acc proj =
- CilE.VarinfoHashtbl.fold (fun v fi acc -> f acc fi) proj.T.functions acc
+ Cilutil.VarinfoHashtbl.fold (fun v fi acc -> f acc fi) proj.T.functions acc
let ff_fi ff = ff.T.ff_fct
diff --git a/src/slicing/slicingProject.ml b/src/slicing/slicingProject.ml
index 1d198bf98af..8887be63492 100644
--- a/src/slicing/slicingProject.ml
+++ b/src/slicing/slicingProject.ml
@@ -40,7 +40,7 @@ let mk_project name =
if M.info () then Format.printf "[slicing] make slicing project '%s'@\n" name;
{ T.name = name ;
T.application = Project.current () ;
- T.functions = CilE.VarinfoHashtbl.create 17;
+ T.functions = Cilutil.VarinfoHashtbl.create 17;
T.actions = [];
}
diff --git a/src/slicing_types/slicingTypes.ml b/src/slicing_types/slicingTypes.ml
index 41cfddf0d7e..164f0a54257 100644
--- a/src/slicing_types/slicingTypes.ml
+++ b/src/slicing_types/slicingTypes.ml
@@ -231,7 +231,7 @@ type t_criterion =
(** The whole project. *)
type t_project = { name : string ;
application : Project.t ;
- functions : t_fct_info CilE.VarinfoHashtbl.t;
+ functions : t_fct_info Cilutil.VarinfoHashtbl.t;
mutable actions : t_criterion list;
}
@@ -259,7 +259,7 @@ type sl_project = Internals.t_project
type sl_select = (Cil_types.varinfo * Internals.t_fct_user_crit)
(** A set of selections, grouped by function *)
-type sl_selects = (Internals.t_fct_user_crit CilE.VarinfoHashtbl.t)
+type sl_selects = (Internals.t_fct_user_crit Cilutil.VarinfoHashtbl.t)
(** Function slice *)
type sl_fct_slice = Internals.t_fct_slice
diff --git a/src/value/eval.ml b/src/value/eval.ml
index 2ffdefada4e..a461c90de41 100644
--- a/src/value/eval.ml
+++ b/src/value/eval.ml
@@ -10,7 +10,7 @@
(* *)
(**************************************************************************)
-(* $Id: eval.ml,v 1.62 2007-11-30 10:26:53 uid527 Exp $ *)
+(* $Id: eval.ml,v 1.63 2007-11-30 13:04:09 uid528 Exp $ *)
(** Analysis for values and pointers *)
@@ -3156,7 +3156,7 @@ let compute_using_cfg kf ~call_kinstr initial_state =
(* associates [varinfo] to a fresh base for the adress returned by function
[varinfo] *)
-let leaf_table = CilE.VarinfoHashtbl.create 7
+let leaf_table = Cilutil.VarinfoHashtbl.create 7
let return_value return_type kf state =
(* Process return of function *)
@@ -3165,7 +3165,8 @@ let return_value return_type kf state =
| TPtr(typ,_) -> begin
let new_base =
(try
- CilE.VarinfoHashtbl.find leaf_table (Kernel_function.get_vi kf)
+ Cilutil.VarinfoHashtbl.find
+ leaf_table (Kernel_function.get_vi kf)
with Not_found ->
let nb =
makeGlobalVar
@@ -3180,7 +3181,8 @@ let return_value return_type kf state =
else
Base.Unknown)
in
- CilE.VarinfoHashtbl.add leaf_table (Kernel_function.get_vi kf) nb;
+ Cilutil.VarinfoHashtbl.add
+ leaf_table (Kernel_function.get_vi kf) nb;
nb)
in
let initial_value = if isArithmeticType typ
--
GitLab