Add missing mli files

remove Meta_options.StringSet in favor of Meta_utils.StrSet

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

meta_annotate.mli

+(** 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

meta_deduce.mli

+(** 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

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;

meta_options.mli

+(** 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;
+}

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 ;

meta_run.mli

+(** 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

meta_utils.mli

+(** 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