diff --git a/meta_annotate.ml b/meta_annotate.ml
index 97dec2c2cdcdd3fc000abd4fc0966a1d0836f30a..451ef6de4b1fd5588484709074f0ef7484fb44b0 100644
--- a/meta_annotate.ml
+++ b/meta_annotate.ml
@@ -62,28 +62,19 @@ let add_label stmt =
label_counter := !label_counter + 1
)
-module Stmt_Hashtbl = Cil_datatype.Stmt.Hashtbl
let delayed_instances = Stmt_Hashtbl.create 256
-module Fundec_Hashtbl = Cil_datatype.Fundec.Hashtbl
let delayed_contracts = Fundec_Hashtbl.create 256
-let add_to_hash_list (find_opt, replace) table key v =
- let old_list = match find_opt table key with
- | None -> []
- | Some l -> l
- in
- replace table key (v :: old_list)
-
(* Common class for contexts *)
class context_visitor flags all_mp table = object(self)
inherit Visitor.frama_c_inplace
val mutable mp_todo = []
- val skip_to_add = Hashtbl.create 50
+ val skip_to_add = Stmt_Hashtbl.create 50
(* Fill mp_todo with MPs to process for the given function name *)
method fill_todo fn =
- let todo = Hashtbl.find_all table fn in
+ let todo = find_hash_list Str_Hashtbl.find_opt table fn in
mp_todo <- List.map (Hashtbl.find all_mp) todo
(* Determine is the current function is a target for some of the properties
@@ -92,7 +83,7 @@ class context_visitor flags all_mp table = object(self)
self # fill_todo f.svar.vname;
if mp_todo = [] then Cil.SkipChildren
else (
- Hashtbl.clear skip_to_add;
+ Stmt_Hashtbl.clear skip_to_add;
Cil.DoChildren
)
@@ -101,7 +92,7 @@ class context_visitor flags all_mp table = object(self)
method private create_next_stmt stmt =
let loc = Cil.CurrentLoc.get () in
let new_stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip loc) in
- Hashtbl.add skip_to_add stmt.sid new_stmt;
+ add_to_hash_list Stmt_Hashtbl.(find_opt, replace) skip_to_add stmt new_stmt;
new_stmt
(* Insert registered SKIPs in corresponding blocks *)
@@ -109,7 +100,7 @@ class context_visitor flags all_mp table = object(self)
let rec aux = function
| [] -> []
| s :: t ->
- s :: (Hashtbl.find_all skip_to_add s.sid) @ (aux t)
+ s :: (find_hash_list Stmt_Hashtbl.find_opt skip_to_add s) @ (aux t)
in block.bstmts <- aux block.bstmts;
block
)
@@ -617,18 +608,14 @@ let annotate flags all_mp by_context =
(* Reset assertion numbers *)
Hashtbl.iter (fun _ ump -> ump.ump_counter := 0) all_mp;
(* Instantiate delayed contracts *)
- begin match Fundec_Hashtbl.find_opt delayed_contracts f with
- | None -> ()
- | Some todo -> List.iter (fun f -> f ()) (List.rev todo)
- end ;
+ let todo = find_hash_list Fundec_Hashtbl.find_opt delayed_contracts f in
+ List.iter (fun f -> f ()) (List.rev todo);
Cil.DoChildren
method! vstmt_aux stmt =
(* Instantiate delayed annotations *)
- begin match Stmt_Hashtbl.find_opt delayed_instances stmt with
- | None -> ()
- | Some todo -> List.iter (fun f -> f ()) (List.rev todo)
- end ;
+ let todo = find_hash_list Stmt_Hashtbl.find_opt delayed_instances stmt in
+ List.iter (fun f -> f ()) (List.rev todo);
Cil.DoChildren
end in
diff --git a/meta_bindings.ml b/meta_bindings.ml
index 72b2e4a570732e015fe37a0708d7c5058a4e3150..741af90891a76d330aeec344cae876b3e4808674 100644
--- a/meta_bindings.ml
+++ b/meta_bindings.ml
@@ -24,6 +24,8 @@ open Logic_ptree
open Logic_typing
open Cil_types
+module Stmt_Hashtbl = Cil_datatype.Stmt.Hashtbl
+
(* Gathered bindings *)
let gathered_bindings = ref []
let types = Hashtbl.create 5
@@ -104,7 +106,7 @@ let ext_flags = ref None
(* to_add maps sids to statements that must be inserted before the
* corresponding statements *)
-let to_add = Hashtbl.create 5
+let to_add = Stmt_Hashtbl.create 5
(* Toggles the inline visitor *)
let visit_inline = ref false
@@ -151,12 +153,12 @@ let add_ghost_code flags =
let rec aux = function
| [] -> []
| s :: t ->
- (Hashtbl.find_all to_add s.sid) @ [s] @ (aux t)
+ (find_hash_list Stmt_Hashtbl.find_opt to_add s) @ [s] @ (aux t)
in block.bstmts <- aux block.bstmts;
block
)
method! vfunc _ =
- Hashtbl.clear to_add;
+ Stmt_Hashtbl.clear to_add;
Cil.DoChildren
end in
Visitor.visitFramacFile vis f
@@ -209,12 +211,14 @@ let gf () =
let process_imeta vis = if !visit_inline then function
| Ext_id id ->
let lvar, name = from_id id in
- let sid = begin match vis#current_kinstr with
+ let s = begin match vis#current_kinstr with
| Kglobal -> assert false
- | Kstmt s -> s.sid
+ | Kstmt s -> s
end in
let gf = gf () in
- List.iter (Hashtbl.add to_add sid) (gf name lvar);
+ List.iter (fun (v : stmt) ->
+ add_to_hash_list Stmt_Hashtbl.(find_opt, replace) to_add s v
+ ) (gf name lvar);
Cil.SkipChildren
| _ -> Cil.SkipChildren
else fun _ -> Cil.SkipChildren
diff --git a/meta_dispatch.ml b/meta_dispatch.ml
index 9d2a9c0d8695308ed635b73a7f6e69715501fb79..c114a443e2b3358c68ca0558fe21da2d06072f62 100644
--- a/meta_dispatch.ml
+++ b/meta_dispatch.ml
@@ -91,9 +91,8 @@ let unpack_mp flags mp admit =
in
{ump_emitter; ump_property; ump_ip; ump_counter; ump_admit = admit; ump_assert}
-
(* Returns an assoc list associating each context to a
- * hash table mapping each function to a list (Hashtbl.find_all) of
+ * hash table mapping each function to a list of
* MP names to process for that context and for that function
*
* Also returns a hash table mapping a MP name to an unpacked MP
@@ -102,7 +101,7 @@ let dispatch flags mps =
let all_mp = Hashtbl.create 10 in
let ctxts = [Weak_invariant; Strong_invariant; Writing; Reading; Calling;
Precond; Postcond] in
- let tables = List.map (fun ctx -> ctx, Hashtbl.create 5) ctxts in
+ let tables = List.map (fun ctx -> ctx, Str_Hashtbl.create 5) ctxts in
List.iter (fun mp ->
let table = List.assoc mp.mp_context tables in
let targets = Meta_deduce.compute_target mp.mp_target in
@@ -118,7 +117,9 @@ let dispatch flags mps =
Meta_deduce.deduce flags mp ip mps
in
if mp.mp_translation <> MtNone then (
- StrSet.iter (fun target -> Hashtbl.add table target mp.mp_name) targets;
+ StrSet.iter (fun target ->
+ add_to_hash_list Str_Hashtbl.(find_opt, replace) table target mp.mp_name
+ ) targets;
Hashtbl.add all_mp mp.mp_name (unpack_mp flags mp admit)
);
) mps;
@@ -135,14 +136,14 @@ module UmpHashtbl = Hashtbl.Make(UmpHash)
let dependencies = UmpHashtbl.create 10
(* Call each time an instantiation of a prop is done *)
let add_dependency ump ips =
- List.iter (UmpHashtbl.add dependencies ump) ips
+ List.iter (add_to_hash_list UmpHashtbl.(find_opt, replace) dependencies ump) ips
(* Call once at the end to actually register dependencies between props and
* their instanciations *)
let finalize_dependencies () =
let keys = UmpHashtbl.to_seq_keys dependencies in
let add_one prop =
- let deps = UmpHashtbl.find_all dependencies prop in
+ let deps = find_hash_list UmpHashtbl.find_opt dependencies prop in
(* If the MP is admitted, every instance *is* true *)
if prop.ump_admit then
List.iter (fun inst ->
diff --git a/meta_dispatch.mli b/meta_dispatch.mli
index cd0341dfd203be93136da89a6dd61a92e9b87d4b..b70d07be512caa65603993a035e93b92dc63c788 100644
--- a/meta_dispatch.mli
+++ b/meta_dispatch.mli
@@ -34,7 +34,7 @@ type unpacked_metaproperty = {
val dispatch : meta_flags ->
metaproperty list ->
- (context * (string, string) Hashtbl.t) list *
+ (context * string list Str_Hashtbl.t) list *
(string, unpacked_metaproperty) Hashtbl.t
val name_mp_pred : meta_flags ->
diff --git a/meta_options.ml b/meta_options.ml
index 937e8b6f72eb9686165b9ee9379e88bcf6d591d8..09ab6019bf3eaca44d9db78709eb0f3eacdc6d8a 100644
--- a/meta_options.ml
+++ b/meta_options.ml
@@ -107,3 +107,14 @@ type meta_flags = {
keep_proof_files : bool;
default_to_assert : bool;
}
+
+let find_hash_list find_opt table key =
+ match find_opt table key with
+ | Some l -> l
+ | None -> []
+
+(* In a hashtable mapping key to lists of values, adds v to that list *)
+let add_to_hash_list (find_opt, replace) table key v =
+ let old_list = find_hash_list find_opt table key in
+ replace table key (v :: old_list)
+
diff --git a/meta_parse.ml b/meta_parse.ml
index 208e7132dd012f0883ef484ae61f313b858077e9..0703e25837942eedabc10faab6fee2bc916980f3 100644
--- a/meta_parse.ml
+++ b/meta_parse.ml
@@ -35,6 +35,9 @@ type context =
| Precond
module StrSet = Datatype.String.Set
+module Str_Hashtbl = Datatype.String.Hashtbl
+module Stmt_Hashtbl = Cil_datatype.Stmt.Hashtbl
+module Fundec_Hashtbl = Cil_datatype.Fundec.Hashtbl
type target =
| TgAll
@@ -454,6 +457,17 @@ let rec check_for_duplicates = function
| h1 :: h2 :: _ when h1.mp_name = h2.mp_name -> Some (h1, h2)
| _ :: t -> check_for_duplicates t
+(*
+let add_to_hash_list_mod (type k table)
+ (module H : Datatype.Hashtbl with type key = k and type 'a t = table)
+ table (key : k) v =
+ let old_list = match H.find_opt table key with
+ | None -> []
+ | Some l -> l
+ in
+ H.replace table key (v :: old_list)
+*)
+
let metaproperties () =
(* Check that there are no duplicate MPs *)
let sorted_props = List.sort (fun a b -> compare a.mp_name b.mp_name)
diff --git a/meta_parse.mli b/meta_parse.mli
index 6fb954c70f6f7f9fea30ab14958a1cade2980c34..6d74d042f117030ee8d145a1ca42fe7f3a501044 100644
--- a/meta_parse.mli
+++ b/meta_parse.mli
@@ -31,6 +31,9 @@ type context =
| Precond
module StrSet = Datatype.String.Set
+module Str_Hashtbl = Datatype.String.Hashtbl
+module Stmt_Hashtbl = Cil_datatype.Stmt.Hashtbl
+module Fundec_Hashtbl = Cil_datatype.Fundec.Hashtbl
type target =
| TgAll
@@ -65,4 +68,3 @@ type metaproperty = {
val register_parsing : unit -> unit
val metaproperties : unit -> metaproperty list
-