From 00662eb7038ecded793fe59e4e1716634c98280b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 16 Apr 2024 15:54:01 +0200
Subject: [PATCH] [kernel] Removes loop pragma WIDEN_VARIABLES and WIDEN_HINTS.
---
src/kernel_internals/parsing/logic_parser.mly | 4 ----
src/kernel_internals/typing/unroll_loops.ml | 1 -
src/kernel_services/analysis/logic_deps.ml | 4 +---
src/kernel_services/ast_data/cil_types.ml | 2 --
.../ast_printing/cil_printer.ml | 6 ------
.../ast_printing/cil_types_debug.ml | 4 ----
.../ast_printing/logic_print.ml | 4 ----
src/kernel_services/ast_queries/ast_diff.ml | 6 +-----
src/kernel_services/ast_queries/cil.ml | 4 ----
.../ast_queries/logic_typing.ml | 20 -------------------
.../ast_queries/logic_utils.ml | 5 +----
src/kernel_services/parsetree/logic_ptree.ml | 2 --
12 files changed, 3 insertions(+), 59 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index cafa0e96b6b..5793c2feb49 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1464,10 +1464,6 @@ loop_pragma:
(if $3 <> "UNROLL" then
Format.eprintf "Warning: use of deprecated keyword '%s'.\nShould use 'UNROLL' instead.@." $3;
Unroll_specs $4)
- else if $3 = "WIDEN_VARIABLES" then
- Widen_variables $4
- else if $3 = "WIDEN_HINTS" then
- Widen_hints $4
else raise (Not_well_formed (loc $sloc,"Unknown loop pragma")) }
;
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index 4bc1d09e391..9a307759483 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -82,7 +82,6 @@ let extract_from_pragmas global_find_init s =
match a.annot_content with
| APragma (Loop_pragma (Unroll_specs specs)) ->
List.fold_left (update_info global_find_init e) info specs
- | APragma (Loop_pragma _) -> info
| _ -> assert false (* should have been filtered above. *)
in
List.fold_left get_infos empty_info pragmas
diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
index 874fb849426..65883a64ce2 100644
--- a/src/kernel_services/analysis/logic_deps.ml
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -478,9 +478,7 @@ let get_zone_from_annot a (ki,kf) loop_body_opt results =
| AVariant (term,_) ->
(* to preserve the interpretation of the variant *)
get_zone_from_term (Option.get loop_body_opt) term results
- | APragma (Loop_pragma (Unroll_specs terms))
- | APragma (Loop_pragma (Widen_hints terms))
- | APragma (Loop_pragma (Widen_variables terms)) ->
+ | APragma (Loop_pragma (Unroll_specs terms)) ->
(* to select the declaration of the variables *)
List.fold_left
(fun results term -> {
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 0b27f448cc4..0ae3f376d5a 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1738,8 +1738,6 @@ and behavior = {
(** Pragmas for the value analysis plugin of Frama-C. *)
and loop_pragma =
| Unroll_specs of term list
- | Widen_hints of term list
- | Widen_variables of term list
(** Pragmas for the slicing plugin of Frama-C. *)
and slice_pragma =
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index a9d7c981037..31b287429f8 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3164,12 +3164,6 @@ class cil_printer () = object (self)
(pp_list false self#disjoint_behaviors) disjoint
method private loop_pragma fmt = function
- | Widen_hints terms ->
- fprintf fmt "WIDEN_HINTS @[%a@]"
- (Pretty_utils.pp_list ~sep:",@ " self#term) terms
- | Widen_variables terms ->
- fprintf fmt "WIDEN_VARIABLES @[%a@]"
- (Pretty_utils.pp_list ~sep:",@ " self#term) terms
| Unroll_specs terms ->
fprintf fmt "UNROLL @[%a@]"
(Pretty_utils.pp_list ~sep:",@ " self#term) terms
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index bdd64597f86..ed13828430d 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -932,10 +932,6 @@ and pp_termination_kind fmt = function
and pp_loop_pragma fmt = function
| Unroll_specs(term_list) ->
Format.fprintf fmt "Unroll_specs(%a)" (pp_list pp_term) term_list
- | Widen_hints(term_list) ->
- Format.fprintf fmt "Widen_hints(%a)" (pp_list pp_term) term_list
- | Widen_variables(term_list) ->
- Format.fprintf fmt "Widen_variables(%a)" (pp_list pp_term) term_list
and pp_slice_pragma fmt = function
| SPexpr(term) -> Format.fprintf fmt "SPexpr(%a)" pp_term term
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 9509cb045c4..f0aeef687ba 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -453,10 +453,6 @@ let print_spec fmt spec =
let print_loop_pragma fmt p =
match p with
Unroll_specs l -> fprintf fmt "UNROLL@ %a" (pp_list ~sep:",@ " print_lexpr) l
- | Widen_hints l ->
- fprintf fmt "WIDEN_HINTS@ %a" (pp_list ~sep:",@ " print_lexpr) l
- | Widen_variables l ->
- fprintf fmt "WIDEN_VARIABLES@ %a" (pp_list ~sep:",@ " print_lexpr) l
let print_slice_pragma fmt p =
match p with
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 58fe0aa05cd..35206eb8bd5 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -702,11 +702,7 @@ and is_same_variant (v,m) (v',m') env =
and is_same_loop_pragma p p' env =
match p, p' with
- | Unroll_specs l, Unroll_specs l'
- | Widen_hints l, Widen_hints l'
- | Widen_variables l, Widen_variables l' ->
- is_same_list is_same_term l l' env
- | (Unroll_specs _ | Widen_hints _ | Widen_variables _), _ -> false
+ | Unroll_specs l, Unroll_specs l' -> is_same_list is_same_term l l' env
and is_same_slice_pragma p p' env =
match p, p' with
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 891b2fb3a4b..7eb80e74d5a 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -2049,10 +2049,6 @@ and childrenLoopPragma vis p =
match p with
| Unroll_specs lt -> let lt' = mapNoCopy (visitCilTerm vis) lt in
if lt' != lt then Unroll_specs lt' else p
- | Widen_hints lt -> let lt' = mapNoCopy (visitCilTerm vis) lt in
- if lt' != lt then Widen_hints lt' else p
- | Widen_variables lt -> let lt' = mapNoCopy (visitCilTerm vis) lt in
- if lt' != lt then Widen_variables lt' else p
and childrenModelInfo vis m =
let field_type = visitCilLogicType vis m.mi_field_type in
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 3377cdbb68d..9c5eddcfe4c 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3632,29 +3632,9 @@ struct
let plain_logic_type loc env t = logic_type (base_ctxt env) loc env t
- (* For Widen_hints and Widen_variables, we check that the arguments of the
- pragma can be understood later. Keep this code synchronized with
- src/plugins/eva/utils/widen.ml. *)
let loop_pragma env p =
- let accept_int = function
- { term_node = TConst (Integer _)} -> true | _ -> false
- in
- let accept_var = function
- { term_node = TLval (TVar {lv_origin = Some _}, _)} -> true | _ -> false
- in
- (* fail when the translation of [p] does not verify the predicate [accept]*)
- let term_accept accept p =
- let t = term env p in
- if not (accept t) then
- C.error t.term_loc "invalid pragma '%a'" Cil_printer.pp_term t;
- t
- in
match p with
| Unroll_specs l -> Cil_types.Unroll_specs (List.map (term env) l)
- | Widen_variables l -> Cil_types.Widen_variables (List.map (term_accept accept_var) l)
- | Widen_hints l ->
- let accept t = accept_int t || accept_var t in
- Cil_types.Widen_hints (List.map (term_accept accept) l)
let model_annot loc ti =
let env = Lenv.empty() in
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index cd74caa5993..6846b6e7114 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1179,9 +1179,6 @@ let is_same_logic_type_info t1 t2 =
let is_same_loop_pragma p1 p2 =
match p1,p2 with
Unroll_specs l1, Unroll_specs l2 -> is_same_list is_same_term l1 l2
- | Widen_hints l1, Widen_hints l2 -> is_same_list is_same_term l1 l2
- | Widen_variables l1, Widen_variables l2 -> is_same_list is_same_term l1 l2
- | (Unroll_specs _ | Widen_hints _ | Widen_variables _), _ -> false
let is_same_slice_pragma p1 p2 =
match p1,p2 with
@@ -2302,7 +2299,7 @@ let is_trivial_annotation a =
-> false
let is_property_pragma = function
- | Loop_pragma (Unroll_specs _ | Widen_hints _ | Widen_variables _)
+ | Loop_pragma (Unroll_specs _)
| Slice_pragma (SPexpr _ | SPctrl | SPstmt)
| Impact_pragma (IPexpr _ | IPstmt) -> false
(* If at some time a pragma becomes something which should be proven,
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index 0dfa4830806..d123c416326 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -323,8 +323,6 @@ type spec = {
type loop_pragma =
| Unroll_specs of lexpr list
- | Widen_hints of lexpr list
- | Widen_variables of lexpr list
(** Pragmas for the slicing plugin of Frama-C. *)
and slice_pragma =
--
GitLab