diff --git a/.gitignore b/.gitignore
index e8f37b339ea3a2c3ac563612af254fde71fc4392..d738d2a9d630e12e2dc33b0df2968ba838bd22d7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,9 +9,9 @@
/top/
# Build files
-/*.cm*
-/*.o
-/.depend
+*.cm*
+*.o
+.depend
/*.log
# Configure-generated files
@@ -76,3 +76,4 @@
/case_studies/wookey/loader/src/shr.h
/case_studies/wookey/loader/src/types.h
+/case_studies/wookey/loader/.cache/
diff --git a/Makefile.in b/Makefile.in
index 82d2e16ec4a07084a313b6452e603b2f5e6299b9..7c7badc4debe8619a15e87af5dd350a93aa2bae7 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -2,7 +2,7 @@
# #
# This file is part of the Frama-C's MetACSL plug-in. #
# #
-# Copyright (C) 2018-2021 #
+# Copyright (C) 2018-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
diff --git a/MetAcsl.mli b/MetAcsl.mli
index 14274bb2f47d5d0e13b27de174c40a1b82f92e51..c5a3a239c19083c69fc45fde6575c960866fdee8 100644
--- a/MetAcsl.mli
+++ b/MetAcsl.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
@@ -20,12 +20,12 @@
(* *)
(**************************************************************************)
-module Meta_options : sig
- module StringSet : (Set.S with type elt = string)
+module Meta_utils : sig
+ module StrSet : Set.S with type elt = string
end
module Meta_run : sig
val translate : ?check_external:bool -> ?simpl:bool ->
- ?target_set:Meta_options.StringSet.t -> ?number_assertions:bool ->
+ ?target_set:Meta_utils.StrSet.t -> ?number_assertions:bool ->
?prefix_meta:bool -> ?static_bindings:int -> unit -> Project.t
end
diff --git a/configure.ac b/configure.ac
index b5099a01421256e0013aa4040f01640ca0c927dd..e35b2fe1767559e2d918424ffecfe9e9057cae0c 100644
--- a/configure.ac
+++ b/configure.ac
@@ -2,7 +2,7 @@
# #
# This file is part of the Frama-C's MetACSL plug-in. #
# #
-# Copyright (C) 2018-2021 #
+# Copyright (C) 2018-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
diff --git a/headers/close-source/CEA_LGPL_OR_PROPRIETARY.META b/headers/close-source/CEA_LGPL_OR_PROPRIETARY.META
index 13946cac0266c6bd596b3b59a629ca04935606ab..32648b67f0b741c93fffc73517dc594c0e0b1db1 100644
--- a/headers/close-source/CEA_LGPL_OR_PROPRIETARY.META
+++ b/headers/close-source/CEA_LGPL_OR_PROPRIETARY.META
@@ -1,7 +1,7 @@
This file is part of the Frama-C's MetACSL plug-in.
-Copyright (C) 2018-2021
+Copyright (C) 2018-2022
CEA (Commissariat à l'énergie atomique et aux énergies
alternatives)
diff --git a/headers/header_config.txt b/headers/header_config.txt
index d6b2d4eb97174ea8649867d3db0dc2f1ad4a9cca..94038435ce599679b7908349389b197bee307505 100644
--- a/headers/header_config.txt
+++ b/headers/header_config.txt
@@ -4,5 +4,6 @@
# PROLOG #
##########
| ".*\.pl" -> frame open: "%" line: "%" close: "%"
-| ".*\.pl" -> skip match: "\(#!.*\|:- encoding.*\)"
+| ".*\.pl" -> skip match: "#!.*"
+| ".*\.pl" -> skip match: ":- encoding.*"
| ".*\.slog" -> frame open: "%" line: "%" close: "%"
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 3bbb0762b3136fde0638722c48a9cfb2fcc37572..70d60358586f7d808f29e2d312353e1e3b1f5fb1 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -5,18 +5,23 @@ configure: .ignore
configure.ac: CEA_LGPL_OR_PROPRIETARY.META
MetAcsl.mli: CEA_LGPL_OR_PROPRIETARY.META
meta_annotate.ml: CEA_LGPL_OR_PROPRIETARY.META
+meta_annotate.mli: CEA_LGPL_OR_PROPRIETARY.META
meta_bindings.ml: CEA_LGPL_OR_PROPRIETARY.META
meta_bindings.mli: CEA_LGPL_OR_PROPRIETARY.META
meta_deduce.ml: CEA_LGPL_OR_PROPRIETARY.META
+meta_deduce.mli: CEA_LGPL_OR_PROPRIETARY.META
meta_dispatch.ml: CEA_LGPL_OR_PROPRIETARY.META
meta_dispatch.mli: CEA_LGPL_OR_PROPRIETARY.META
meta_options.ml: CEA_LGPL_OR_PROPRIETARY.META
+meta_options.mli: CEA_LGPL_OR_PROPRIETARY.META
meta_parse.ml: CEA_LGPL_OR_PROPRIETARY.META
meta_parse.mli: CEA_LGPL_OR_PROPRIETARY.META
meta_run.ml: CEA_LGPL_OR_PROPRIETARY.META
+meta_run.mli: CEA_LGPL_OR_PROPRIETARY.META
meta_simplify.ml: CEA_LGPL_OR_PROPRIETARY.META
meta_simplify.mli: CEA_LGPL_OR_PROPRIETARY.META
meta_utils.ml: CEA_LGPL_OR_PROPRIETARY.META
+meta_utils.mli: CEA_LGPL_OR_PROPRIETARY.META
README.md: .ignore
tests: .ignore
opam: .ignore
diff --git a/headers/open-source/CEA_LGPL_OR_PROPRIETARY.META b/headers/open-source/CEA_LGPL_OR_PROPRIETARY.META
index 2ea608fdeae3fa854bc37ff5274e84237efaa904..c1dbb2892270e81aeef35c7af3159017cc17d99d 100644
--- a/headers/open-source/CEA_LGPL_OR_PROPRIETARY.META
+++ b/headers/open-source/CEA_LGPL_OR_PROPRIETARY.META
@@ -1,7 +1,7 @@
This file is part of the Frama-C's MetACSL plug-in.
-Copyright (C) 2018-2021
+Copyright (C) 2018-2022
CEA (Commissariat à l'énergie atomique et aux énergies
alternatives)
diff --git a/meta_annotate.ml b/meta_annotate.ml
index a62bd11e9cf96aebee2593189117e2132478474e..cb324f2080cd9c846e18e53cf5deda9cfc3b9646 100644
--- a/meta_annotate.ml
+++ b/meta_annotate.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
@@ -618,17 +618,6 @@ class strong_inv_visitor flags all_mp table = object (self)
else Cil.DoChildren
end
-(* Print how the MPs were dispatched *)
-let report all_mp tables =
- let open Meta_dispatch in
- List.iter (fun (_, table) ->
- Self.feedback "New context";
- Hashtbl.iter (fun key value ->
- Self.feedback "%s -> %s" key
- (Emitter.get_name (Hashtbl.find all_mp value).ump_emitter)
- ) table
- ) tables
-
(* Make one copy-pass for each context, typing and instanciating MPs on the fly *)
let annotate flags all_mp by_context =
let get_vis table = function
diff --git a/meta_annotate.mli b/meta_annotate.mli
new file mode 100644
index 0000000000000000000000000000000000000000..830ab908910203115f2499403ad9612522d8709e
--- /dev/null
+++ b/meta_annotate.mli
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's MetACSL plug-in. *)
+(* *)
+(* Copyright (C) 2018-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* 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 2.1. *)
+(* *)
+(* 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 2.1 *)
+(* for more details (enclosed in the file LICENSE) *)
+(* *)
+(**************************************************************************)
+
+(** generate all instances of an HILARE *)
+
+val annotate:
+ Meta_options.meta_flags ->
+ (string,Meta_dispatch.unpacked_metaproperty) Hashtbl.t ->
+ (Meta_parse.context * string list Meta_utils.Str_Hashtbl.t)
+ list ->
+ unit
diff --git a/meta_bindings.ml b/meta_bindings.ml
index e37d8a8e8a9cf07b7c7ee9a53093d52b115f070f..0f1d6801914e066f06641bd4690e58609a2799a4 100644
--- a/meta_bindings.ml
+++ b/meta_bindings.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/meta_bindings.mli b/meta_bindings.mli
index 9a13f46cab99602012a56570172158636516690c..1297d2b8fcb9b60dc81adca8cde51b35f716dd99 100644
--- a/meta_bindings.mli
+++ b/meta_bindings.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/meta_deduce.ml b/meta_deduce.ml
index 0d2e8311e46663955d4f4b9491907e616b6814bf..eff3cb2dd3878899dd22e0ff37e7d65891bf3e20 100644
--- a/meta_deduce.ml
+++ b/meta_deduce.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/meta_deduce.mli b/meta_deduce.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f5219a2a4a2b17195e8f1a251981c857b9224b43
--- /dev/null
+++ b/meta_deduce.mli
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's MetACSL plug-in. *)
+(* *)
+(* Copyright (C) 2018-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* 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 2.1. *)
+(* *)
+(* 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 2.1 *)
+(* for more details (enclosed in the file LICENSE) *)
+(* *)
+(**************************************************************************)
+
+(** use meta-deduction to prove an HILARE *)
+
+(** computes the set of function names that compose the given target. *)
+val compute_target: Meta_parse.target -> Meta_utils.StrSet.t
+
+(** [deduce flags mp ip mps] attempts to prove [mp] under the hypothesis that
+ [mps] hold, in the environment [flags]. [ip] is the corresponding identified
+ property for the kernel: its status will be set according to the result of
+ the proof attempt. Returns [true] iff the proof has succeeded.
+*)
+val deduce:
+ Meta_options.meta_flags ->
+ Meta_parse.metaproperty ->
+ Property.t ->
+ Meta_parse.metaproperty list ->
+ bool
diff --git a/meta_dispatch.ml b/meta_dispatch.ml
index 27de33b58005ec5c5bea7e292c7aff70546d17be..8067462d34c77a9620cc8eae61692088a0da7bf6 100644
--- a/meta_dispatch.ml
+++ b/meta_dispatch.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/meta_dispatch.mli b/meta_dispatch.mli
index 0c9ec21679ba0bcfd2d39e7f454c539615fad95a..5f510ffccd5361991be9735c3e9a9df9fb2cf9b4 100644
--- a/meta_dispatch.mli
+++ b/meta_dispatch.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/meta_options.ml b/meta_options.ml
index d0e8c762fbdaec6a3fb3e9084638df85a586e284..ae7a69fca9d1de9484d4846d264c74057a89def5 100644
--- a/meta_options.ml
+++ b/meta_options.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
@@ -59,8 +59,6 @@ module Simpl = Self.True (struct
let help = "Discard annotations that are obviously true"
end)
-module StringSet = Set.Make(String)
-
module Number_assertions = Self.False (struct
let option_name = "-meta-number-assertions"
let help = "Add an unique number to each instance of a meta-propery."
@@ -109,7 +107,7 @@ type meta_flags = {
simpl : bool;
eacsl_transform : bool;
static_bindings : int option;
- target_set : StringSet.t option;
+ target_set : Meta_utils.StrSet.t option;
number_assertions : bool;
prefix_meta : bool;
list_targets : bool;
diff --git a/meta_options.mli b/meta_options.mli
new file mode 100644
index 0000000000000000000000000000000000000000..66a2ee11891a212ad0a6d5f8602b0e2ada081e03
--- /dev/null
+++ b/meta_options.mli
@@ -0,0 +1,76 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's MetACSL plug-in. *)
+(* *)
+(* Copyright (C) 2018-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* 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 2.1. *)
+(* *)
+(* 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 2.1 *)
+(* for more details (enclosed in the file LICENSE) *)
+(* *)
+(**************************************************************************)
+
+(** Command line options and plugin registration. *)
+
+module Self: Plugin.S
+
+(** value of [-meta] *)
+module Enabled: Parameter_sig.Bool
+
+(** value of [-meta-check-ext] *)
+module Check_External: Parameter_sig.Bool
+
+(** value of [-meta-eacsl] *)
+module Eacsl_transform: Parameter_sig.Bool
+
+(** value of [-meta-set] *)
+module Targets: Parameter_sig.String_set
+
+(** value of [-meta-simpl] *)
+module Simpl: Parameter_sig.Bool
+
+(** value of [-meta-number-assertions] *)
+module Number_assertions: Parameter_sig.Bool
+
+(** value of [-meta-add-prefix] *)
+module Prefix_meta: Parameter_sig.Bool
+
+(** value of [-meta-list-targets] *)
+module List_targets: Parameter_sig.Bool
+
+(** value of [-meta-keep-proof-files] *)
+module Keep_proof_files: Parameter_sig.Bool
+
+(** value of [-meta-static-bindings] *)
+module Static_bindings: Parameter_sig.Int
+
+(** value of [-meta-separate-annots] *)
+module Separate_annots: Parameter_sig.Bool
+
+(** value of [-meta-asserts] *)
+module Default_to_assert: Parameter_sig.Bool
+
+(** record with all the options as set at the start
+ of the analysis. *)
+type meta_flags = {
+ check_external : bool;
+ simpl : bool;
+ eacsl_transform : bool;
+ static_bindings : int option;
+ target_set : Meta_utils.StrSet.t option;
+ number_assertions : bool;
+ prefix_meta : bool;
+ list_targets : bool;
+ keep_proof_files : bool;
+ default_to_assert : bool;
+}
diff --git a/meta_parse.ml b/meta_parse.ml
index 2e1687f1a416c0a39aa254cc4a99a82f306cc4c2..fe768bb8dd311bfaeb77b07c1aa881003d080327 100644
--- a/meta_parse.ml
+++ b/meta_parse.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/meta_parse.mli b/meta_parse.mli
index 4540c41768721bbc8a8b28f1ba91f67adf02b5e7..385e9f2d42ad0e0e507956cd40fc21b7133e816e 100644
--- a/meta_parse.mli
+++ b/meta_parse.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/meta_run.ml b/meta_run.ml
index ab057a24cd52e697b9e1a1c35520c40c77ceef3e..5cb7182ec3ba991c3621d09af36a7fb8e575684d 100644
--- a/meta_run.ml
+++ b/meta_run.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
@@ -20,6 +20,7 @@
(* *)
(**************************************************************************)
+open Meta_utils
open Meta_options
open Meta_parse
@@ -38,7 +39,7 @@ let generate flags =
(* Filter only specified ones (-meta-set) *)
let to_translate = match flags.target_set with
| None -> mps
- | Some set -> List.filter (fun mp -> StringSet.mem mp.mp_name set) mps
+ | Some set -> List.filter (fun mp -> StrSet.mem mp.mp_name set) mps
in
Self.feedback "Will process %d properties" (List.length to_translate);
(* Dispatch MPs according to their targets and context to ease annotation *)
@@ -79,7 +80,7 @@ let register () =
list_targets = List_targets.get ();
default_to_assert = Default_to_assert.get ();
target_set = if Targets.is_empty () then None else
- let set = Targets.fold StringSet.add StringSet.empty in
+ let set = Targets.fold StrSet.add StrSet.empty in
Some set;
} in
ignore @@ generate flags ;
diff --git a/meta_run.mli b/meta_run.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a69415a586e8fe1d4b67a8c48b52b15b04a80cb0
--- /dev/null
+++ b/meta_run.mli
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's MetACSL plug-in. *)
+(* *)
+(* Copyright (C) 2018-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* 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 2.1. *)
+(* *)
+(* 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 2.1 *)
+(* for more details (enclosed in the file LICENSE) *)
+(* *)
+(**************************************************************************)
+
+(** main entry point *)
+
+(** generate a new project in which the HILARE have been instantiated according
+ to the given flags.
+*)
+val generate: Meta_options.meta_flags -> Project.t
+
+
+(** same as above, but each option can be set individually. *)
+val translate:
+ ?check_external:bool ->
+ ?simpl: bool ->
+ ?target_set: Meta_utils.StrSet.t ->
+ ?number_assertions: bool ->
+ ?prefix_meta: bool ->
+ ?static_bindings: int ->
+ unit ->
+ Project.t
diff --git a/meta_simplify.ml b/meta_simplify.ml
index 76f52db87401d77830090dc082df887f08777edc..e62a8c21f962a81fa28102537a4dedc6e9db4ea7 100644
--- a/meta_simplify.ml
+++ b/meta_simplify.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/meta_simplify.mli b/meta_simplify.mli
index bd33ed1a5ce7ecde0c1d302d1213d134504caf7d..3c9156d020863379df5e1732de5d214a14368f9c 100644
--- a/meta_simplify.mli
+++ b/meta_simplify.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/meta_utils.ml b/meta_utils.ml
index 64cdcf03efb8afa9ae3916aa311062ddb61b853e..ffbfd148f0f6e7eaf3d9a5207c1dbb2beb8a9518 100644
--- a/meta_utils.ml
+++ b/meta_utils.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
-(* Copyright (C) 2018-2021 *)
+(* Copyright (C) 2018-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/meta_utils.mli b/meta_utils.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a534a3a9eaeff19c081d669f7d199722e57ac0fb
--- /dev/null
+++ b/meta_utils.mli
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's MetACSL plug-in. *)
+(* *)
+(* Copyright (C) 2018-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* 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 2.1. *)
+(* *)
+(* 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 2.1 *)
+(* for more details (enclosed in the file LICENSE) *)
+(* *)
+(**************************************************************************)
+
+(** Various utilities. *)
+
+(** {1 shortcuts} *)
+
+module StrSet: Datatype.Set with type elt = string
+
+module Str_Hashtbl: Datatype.Hashtbl with type key = string
+
+module Stmt_Hashtbl: Datatype.Hashtbl with type key = Cil_types.stmt
+
+module Fundec_Hashtbl: Datatype.Hashtbl with type key = Cil_types.fundec
+
+module Fundec_Set: Datatype.Set with type elt = Cil_types.fundec
+
+(** {1 Hashtbl utilities} *)
+
+(** [find_hash_list find_opt tbl key] tries to find [key] in [tbl] using
+ [find_opt] and returns the empty list if it is not found.
+*)
+val find_hash_list: ('a -> 'b -> 'c list option) -> 'a -> 'b -> 'c list
+
+(** [add_to_hash_list (find_opt, replace) tbl key v] adds [v] to the list
+ of elements associated to [key] in [tbl], using [find_opt] and
+ [replace] functions. *)
+val add_to_hash_list:
+ ('a -> 'b -> 'c list option) * ('a -> 'b -> 'c list -> unit) ->
+ 'a -> 'b -> 'c -> unit
diff --git a/share/model.slog b/share/model.slog
index 279ad1c7ca37aa49a19ce194be5526b63d14f06f..8d2339c0d585ccd326239ae84b461305bf91afd1 100644
--- a/share/model.slog
+++ b/share/model.slog
@@ -2,7 +2,7 @@
% %
% This file is part of the Frama-C's MetACSL plug-in. %
% %
-% Copyright (C) 2018-2021 %
+% Copyright (C) 2018-2022 %
% CEA (Commissariat à l'énergie atomique et aux énergies %
% alternatives) %
% %
diff --git a/share/run.pl b/share/run.pl
index 63f3207e42596d6cbb025781e9de40ba253eecf0..e6994e54fa38a82bcf1f352f68ef4c012b7a1e7e 100755
--- a/share/run.pl
+++ b/share/run.pl
@@ -4,7 +4,7 @@
% %
% This file is part of the Frama-C's MetACSL plug-in. %
% %
-% Copyright (C) 2018-2021 %
+% Copyright (C) 2018-2022 %
% CEA (Commissariat à l'énergie atomique et aux énergies %
% alternatives) %
% %