diff --git a/MetAcsl.mli b/MetAcsl.mli
index 14274bb2f47d5d0e13b27de174c40a1b82f92e51..6dc95c93d1c93171cd6415ba2d5178627f887e22 100644
--- a/MetAcsl.mli
+++ b/MetAcsl.mli
@@ -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/meta_annotate.mli b/meta_annotate.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bbe9025f8dd5245de782d5f4141dc7d5b80c929d
--- /dev/null
+++ b/meta_annotate.mli
@@ -0,0 +1,8 @@
+(** 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_deduce.mli b/meta_deduce.mli
new file mode 100644
index 0000000000000000000000000000000000000000..252952f0a0bf7f814da627d42bed874dac568899
--- /dev/null
+++ b/meta_deduce.mli
@@ -0,0 +1,16 @@
+(** 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_options.ml b/meta_options.ml
index d0e8c762fbdaec6a3fb3e9084638df85a586e284..20efaa49cf2c753ecb0172fabc1e6170f13f5c07 100644
--- a/meta_options.ml
+++ b/meta_options.ml
@@ -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..19c91eafd8ad89eb5728975ab410a52a25b6f6c9
--- /dev/null
+++ b/meta_options.mli
@@ -0,0 +1,54 @@
+(** 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_run.ml b/meta_run.ml
index ab057a24cd52e697b9e1a1c35520c40c77ceef3e..282eb2519c118ad817ba0249ca4d869a0bd4daf6 100644
--- a/meta_run.ml
+++ b/meta_run.ml
@@ -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..476b79d8f4f128ecfae82fe55eb3d13dce26cd3d
--- /dev/null
+++ b/meta_run.mli
@@ -0,0 +1,18 @@
+(** 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_utils.mli b/meta_utils.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5574dc92bfdc94762bceb1aaf79c0f47cf7c8590
--- /dev/null
+++ b/meta_utils.mli
@@ -0,0 +1,27 @@
+(** 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