From 73ca4d87a9df86899fe27806580c57535a8997eb Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 16 Feb 2022 14:39:09 +0100
Subject: [PATCH] [eacsl] Move annotation_kind to Analyses_types
---
.../e-acsl/src/analyses/analyses_datatype.ml | 18 ++++++++++++++++++
.../e-acsl/src/analyses/analyses_datatype.mli | 2 ++
.../e-acsl/src/analyses/analyses_types.mli | 8 ++++++++
.../e-acsl/src/code_generator/assert.ml | 12 ++++--------
.../e-acsl/src/code_generator/assert.mli | 5 +++--
.../e-acsl/src/code_generator/contract.ml | 8 ++++----
src/plugins/e-acsl/src/code_generator/env.ml | 5 +++--
src/plugins/e-acsl/src/code_generator/env.mli | 4 ++--
src/plugins/e-acsl/src/code_generator/libc.ml | 4 ++--
.../e-acsl/src/code_generator/logic_array.ml | 2 +-
src/plugins/e-acsl/src/code_generator/loops.ml | 14 +++++++-------
.../e-acsl/src/code_generator/smart_stmt.ml | 8 --------
.../e-acsl/src/code_generator/smart_stmt.mli | 8 --------
.../src/code_generator/translate_annots.ml | 4 ++--
.../src/code_generator/translate_rtes.ml | 2 +-
.../src/code_generator/translate_terms.ml | 4 ++--
.../src/code_generator/translate_utils.ml | 4 ++--
17 files changed, 61 insertions(+), 51 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index b638097ad1f..ffb90408735 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 212b5887cd5..481963ab89c 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/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
diff --git a/src/plugins/e-acsl/src/analyses/analyses_types.mli b/src/plugins/e-acsl/src/analyses/analyses_types.mli
index d670f9d0e20..e2aafb100a6 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_types.mli
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml
index f2528e9c6df..578413dccb4 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/assert.mli b/src/plugins/e-acsl/src/code_generator/assert.mli
index 30ae0b268d0..787c5854c02 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.mli
+++ b/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 ->
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index 69d7b48a5e6..879ee0ceadf 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index a090072fb28..95a7715b97a 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/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 = [];
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 29e34613a77..13e604e25c7 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/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} *)
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index 9214791359c..2121d714196 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
index d9a75dce635..a156e946340 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_array.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 0166604f9e7..44d5e8fdc77 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
index 6bcc645ed33..e76366fa4ce 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+++ b/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 ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
index 165e8152589..887cf852e0a 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
+++ b/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 ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
index a1d1cfb14b6..bc00c99360a 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/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 =
diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
index cb05e6165e8..8e76febe0cc 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index a1e55e5d0eb..c569adf41cd 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
index 89fe539c7f5..9a26a8cc21a 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml
+++ b/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
--
GitLab