[eacsl] Move annotation_kind to Analyses_types

src/plugins/e-acsl/src/analyses/analyses_datatype.ml

@@ -25,6 +25,24 @@
 open Cil_datatype
 open Analyses_types
 
+module Annotation_kind =
+  Datatype.Make
+    (struct
+      type t = annotation_kind
+      let name = "E_ACSL.Annotation_kind"
+      let reprs = [ Assertion ]
+      include Datatype.Undefined
+
+      let pretty fmt akind =
+        match akind with
+        | Assertion -> Format.fprintf fmt "Assertion"
+        | Precondition -> Format.fprintf fmt "Precondition"
+        | Postcondition -> Format.fprintf fmt "Postcondition"
+        | Invariant -> Format.fprintf fmt "Invariant"
+        | Variant -> Format.fprintf fmt "Variant"
+        | RTE -> Format.fprintf fmt "RTE"
+    end)
+
 module PredOrTerm =
   Datatype.Make_with_collections
     (struct

src/plugins/e-acsl/src/analyses/analyses_datatype.mli

@@ -24,4 +24,6 @@
 
 open Analyses_types
 
+module Annotation_kind: Datatype.S with type t = annotation_kind
+
 module PredOrTerm: Datatype.S_with_collections with type t = pred_or_term

src/plugins/e-acsl/src/analyses/analyses_types.mli

@@ -35,3 +35,11 @@ type lscope = lscope_var list
 type pred_or_term =
   | PoT_pred of predicate
   | PoT_term of term
+
+type annotation_kind =
+  | Assertion
+  | Precondition
+  | Postcondition
+  | Invariant
+  | Variant
+  | RTE

src/plugins/e-acsl/src/code_generator/assert.ml

@@ -24,6 +24,8 @@
     general functions to create assertion statements. *)
 
 open Cil_types
+open Analyses_types
+open Analyses_datatype
 
 (** Type holding information about the C variable representing the assertion
     data. *)
@@ -186,7 +188,7 @@ let register_term ~loc env ?force t e adata =
   register ~loc env name ?force e adata
 
 let register_pred ~loc env ?force p e adata =
-  if Env.annotation_kind env == Smart_stmt.RTE then
+  if Env.annotation_kind env == RTE then
     (* When translating RTE, we do not want to print the result of the predicate
        because they should be the only predicate in an assertion clause. *)
     adata, env
@@ -197,13 +199,7 @@ let register_pred ~loc env ?force p e adata =
 let kind_to_string loc k =
   Cil.mkString
     ~loc
-    (match k with
-     | Smart_stmt.Assertion -> "Assertion"
-     | Smart_stmt.Precondition -> "Precondition"
-     | Smart_stmt.Postcondition -> "Postcondition"
-     | Smart_stmt.Invariant -> "Invariant"
-     | Smart_stmt.Variant -> "Variant"
-     | Smart_stmt.RTE -> "RTE")
+    (Format.asprintf "%a" Annotation_kind.pretty k)
 
 let runtime_check_with_msg ~adata ~loc ?(name="") msg ~pred_kind kind kf env predicate_e =
   let env = Env.push env in

src/plugins/e-acsl/src/code_generator/assert.mli

@@ -24,6 +24,7 @@
     general functions to create assertion statements. *)
 
 open Cil_types
+open Analyses_types
 
 type t
 (** Type to hold the data contributing to an assertion. *)
@@ -99,7 +100,7 @@ val register_pred:
 val runtime_check:
   adata:t ->
   pred_kind:predicate_kind ->
-  Smart_stmt.annotation_kind ->
+  annotation_kind ->
   kernel_function ->
   Env.t ->
   exp ->
@@ -121,7 +122,7 @@ val runtime_check_with_msg:
   ?name:string ->
   string ->
   pred_kind:predicate_kind ->
-  Smart_stmt.annotation_kind ->
+  annotation_kind ->
   kernel_function ->
   Env.t ->
   exp ->

src/plugins/e-acsl/src/code_generator/contract.ml

@@ -374,7 +374,7 @@ let check_other_requires kf env contract =
                    Assert.runtime_check
                      ~adata
                      ~pred_kind
-                     Smart_stmt.Precondition
+                     Precondition
                      kf
                      env
                      requires_e
@@ -697,7 +697,7 @@ let check_post_conds kf env contract =
                        Assert.runtime_check
                          ~adata
                          ~pred_kind
-                         Smart_stmt.Postcondition
+                         Postcondition
                          kf
                          env
                          post_cond_e
@@ -754,7 +754,7 @@ let check_post_conds kf env contract =
     contract.spec.spec_behavior
 
 let translate_preconditions kf env contract =
-  let env = Env.set_annotation_kind env Smart_stmt.Precondition in
+  let env = Env.set_annotation_kind env Precondition in
   let env = Env.push_contract env contract in
   let env = init kf env contract in
   (* Start with translating the requires predicate of the default behavior. *)
@@ -775,7 +775,7 @@ let translate_preconditions kf env contract =
   Env.handle_error do_it env
 
 let translate_postconditions kf env =
-  let env = Env.set_annotation_kind env Smart_stmt.Postcondition in
+  let env = Env.set_annotation_kind env Postcondition in
   let contract, env = Env.pop_and_get_contract env in
   let do_it env =
     let env = check_post_conds kf env contract in

src/plugins/e-acsl/src/code_generator/env.ml

@@ -23,6 +23,7 @@
 module E_acsl_label = Label
 open Cil_types
 open Cil_datatype
+open Analyses_types
 open Contract_types
 module Error = Translation_error
 
@@ -63,7 +64,7 @@ type loop_env = {
 type t = {
   lscope: Lscope.t;
   lscope_reset: bool;
-  annotation_kind: Smart_stmt.annotation_kind;
+  annotation_kind: annotation_kind;
   new_global_vars: (varinfo * localized_scope) list;
   (* generated variables. The scope indicates the level where the variable
      should be added. *)
@@ -104,7 +105,7 @@ let empty_loop_env =
 let empty =
   { lscope = Lscope.empty;
     lscope_reset = true;
-    annotation_kind = Smart_stmt.Assertion;
+    annotation_kind = Assertion;
     new_global_vars = [];
     global_mp_tbl = empty_mp_tbl;
     env_stack = [];

src/plugins/e-acsl/src/code_generator/env.mli

@@ -152,8 +152,8 @@ end
 (** {2 Current annotation kind} *)
 (* ************************************************************************** *)
 
-val annotation_kind: t -> Smart_stmt.annotation_kind
-val set_annotation_kind: t -> Smart_stmt.annotation_kind -> t
+val annotation_kind: t -> annotation_kind
+val set_annotation_kind: t -> annotation_kind -> t
 
 (* ************************************************************************** *)
 (** {2 Loop annotations} *)

src/plugins/e-acsl/src/code_generator/libc.ml

@@ -229,7 +229,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
           Assert.runtime_check
             ~adata
             ~pred_kind:Assert
-            Smart_stmt.RTE
+            RTE
             kf
             env
             lower_guard
@@ -256,7 +256,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
           Assert.runtime_check
             ~adata
             ~pred_kind:Assert
-            Smart_stmt.RTE
+            RTE
             kf
             env
             upper_guard

src/plugins/e-acsl/src/code_generator/logic_array.ml

@@ -249,7 +249,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
         Assert.register ~loc env "current length" len_orig adata
       in
       let stmt, env =
-        Assert.runtime_check ~adata ~pred_kind:Assert Smart_stmt.RTE kf env e p
+        Assert.runtime_check ~adata ~pred_kind:Assert RTE kf env e p
       in
       stmt :: stmts, env
   in

src/plugins/e-acsl/src/code_generator/loops.ml

@@ -64,7 +64,7 @@ let handle_annotations env kf stmt =
         (fun (stmts, env, _) ->
            match Env.top_loop_variant env with
            | Some (t, measure_opt) ->
-             let env = Env.set_annotation_kind env Smart_stmt.Variant in
+             let env = Env.set_annotation_kind env Variant in
              let env = Env.push env in
              (* There cannot be bound logical variables since we cannot write
                 loops inside logic functions or predicates, hence lenv is []*)
@@ -98,7 +98,7 @@ let handle_annotations env kf stmt =
     let rec aux (stmts, env) = function
       | [] -> begin
           (* No statements remaining in the loop: variant check *)
-          let env = Env.set_annotation_kind env Smart_stmt.Variant in
+          let env = Env.set_annotation_kind env Variant in
           let lenv = Env.Local_vars.get env in
           match variant with
           | Some (t, e_old, Some measure) ->
@@ -153,7 +153,7 @@ let handle_annotations env kf stmt =
                 ~loc
                 msg
                 ~pred_kind:Assert
-                Smart_stmt.Variant
+                Variant
                 kf
                 env
                 e_tapp
@@ -194,7 +194,7 @@ let handle_annotations env kf stmt =
                 ~loc
                 msg1
                 ~pred_kind:Assert
-                Smart_stmt.Variant
+                Variant
                 kf
                 env
                 variant_pos_e
@@ -236,7 +236,7 @@ let handle_annotations env kf stmt =
                 ~loc
                 msg2
                 ~pred_kind:Assert
-                Smart_stmt.Variant
+                Variant
                 kf
                 env
                 variant_dec_e
@@ -258,7 +258,7 @@ let handle_annotations env kf stmt =
         (* Last statement of the loop: invariant check *)
         (* Optimisation to only verify invariant on a non-empty body loop. *)
         let invariants = Env.top_loop_invariants env in
-        let env = Env.set_annotation_kind env Smart_stmt.Invariant in
+        let env = Env.set_annotation_kind env Invariant in
         let env = Env.push env in
         let env =
           let translate_named_predicate = !translate_predicate_ref in
@@ -392,7 +392,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
           Assert.runtime_check
             ~adata
             ~pred_kind:Assert
-            Smart_stmt.RTE
+            RTE
             kf
             env
             e

src/plugins/e-acsl/src/code_generator/smart_stmt.ml

@@ -210,14 +210,6 @@ let mark_readonly vi =
   let loc = vi.vdecl in
   rtl_call ~loc "mark_readonly" [ Cil.evar ~loc vi ]
 
-type annotation_kind =
-  | Assertion
-  | Precondition
-  | Postcondition
-  | Invariant
-  | Variant
-  | RTE
-
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

src/plugins/e-acsl/src/code_generator/smart_stmt.mli

@@ -109,14 +109,6 @@ val mark_readonly: varinfo -> stmt
 (** Same as [store_stmt] for [__e_acsl_markreadonly] that observes the
     read-onlyness of the given varinfo. *)
 
-type annotation_kind =
-  | Assertion
-  | Precondition
-  | Postcondition
-  | Invariant
-  | Variant
-  | RTE
-
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

src/plugins/e-acsl/src/code_generator/translate_annots.ml

@@ -70,7 +70,7 @@ let pre_code_annotation kf stmt env annot =
     | AAssert(l, p) ->
       if Translate_utils.must_translate
           (Property.ip_of_code_annot_single kf stmt annot) then
-        let env = Env.set_annotation_kind env Smart_stmt.Assertion in
+        let env = Env.set_annotation_kind env Assertion in
         if l <> [] then
           Env.not_yet env "@[assertion applied only on some behaviors@]";
         Env.with_params
@@ -93,7 +93,7 @@ let pre_code_annotation kf stmt env annot =
     | AInvariant(l, loop_invariant, p) ->
       if Translate_utils.must_translate
           (Property.ip_of_code_annot_single kf stmt annot) then
-        let env = Env.set_annotation_kind env Smart_stmt.Invariant in
+        let env = Env.set_annotation_kind env Invariant in
         if l <> [] then
           Env.not_yet env "@[invariant applied only on some behaviors@]";
         let env =

src/plugins/e-acsl/src/code_generator/translate_rtes.ml

@@ -27,7 +27,7 @@ let dkey = Options.Dkey.translation
 
 let rte_annots pp elt kf env l =
   let old_kind = Env.annotation_kind env in
-  let env = Env.set_annotation_kind env Smart_stmt.RTE in
+  let env = Env.set_annotation_kind env RTE in
   let env =
     List.fold_left
       (fun env a -> match a.annot_content with

src/plugins/e-acsl/src/code_generator/translate_terms.ml

@@ -525,7 +525,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
           Assert.runtime_check
             ~adata:adata2
             ~pred_kind:Assert
-            Smart_stmt.RTE
+            RTE
             kf
             env
             coerce_guard
@@ -605,7 +605,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
               Assert.runtime_check
                 ~adata:adata1
                 ~pred_kind:Assert
-                Smart_stmt.RTE
+                RTE
                 kf
                 env
                 e1_guard

src/plugins/e-acsl/src/code_generator/translate_utils.ml

@@ -100,7 +100,7 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
         Assert.runtime_check
           ~adata:adata_lower_guard
           ~pred_kind:Assert
-          Smart_stmt.RTE
+          RTE
           kf
           env
           lower_guard
@@ -130,7 +130,7 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
     Assert.runtime_check
       ~adata:adata_upper_guard
       ~pred_kind:Assert
-      Smart_stmt.RTE
+      RTE
       kf
       env
       upper_guard