From 21337c8e22249221c78e8963cd3b43942bed4b06 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 16 Apr 2024 20:33:27 +0200
Subject: [PATCH] [kernel] Removes old impact pragma (now replaced by an ACSL
extension).
---
src/kernel_internals/parsing/logic_parser.mly | 10 ----------
src/kernel_services/analysis/logic_deps.ml | 5 ++---
src/kernel_services/ast_data/cil_types.ml | 6 ------
src/kernel_services/ast_printing/cil_printer.ml | 8 --------
.../ast_printing/cil_types_debug.ml | 6 ------
.../ast_printing/cil_types_debug.mli | 2 --
src/kernel_services/ast_printing/logic_print.ml | 6 ------
src/kernel_services/ast_queries/ast_diff.ml | 8 --------
src/kernel_services/ast_queries/cil.ml | 11 -----------
src/kernel_services/ast_queries/cil.mli | 1 -
src/kernel_services/ast_queries/logic_typing.ml | 7 -------
src/kernel_services/ast_queries/logic_utils.ml | 17 ++---------------
src/kernel_services/ast_queries/logic_utils.mli | 2 --
src/kernel_services/parsetree/logic_ptree.ml | 6 ------
src/plugins/impact/register.ml | 7 ++++---
src/plugins/metrics/metrics_pivot.ml | 1 -
16 files changed, 8 insertions(+), 95 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 79d29dce4a3..98c190c409a 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1475,7 +1475,6 @@ beg_pragma_or_code_annotation:
pragma_or_code_annotation:
| slice_pragma { APragma (Slice_pragma $1) }
-| impact_pragma { APragma (Impact_pragma $1) }
| code_annotation { $1 [] }
;
@@ -1527,15 +1526,6 @@ slice_pragma:
else raise (Not_well_formed (loc $sloc, "Unknown slice pragma")) }
;
-impact_pragma:
-| IMPACT PRAGMA any_identifier lexpr SEMICOLON
- { if $3 = "expr" then IPexpr $4
- else raise (Not_well_formed (loc $sloc, "Unknown impact pragma")) }
-| IMPACT PRAGMA any_identifier SEMICOLON
- { if $3 = "stmt" then IPstmt
- else raise (Not_well_formed (loc $sloc, "Unknown impact pragma")) }
-;
-
/*** declarations and logical definitions ***/
decl_list:
diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
index d416534d0ac..3eae6d298b6 100644
--- a/src/kernel_services/analysis/logic_deps.ml
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -452,7 +452,7 @@ let get_zone_from_annot a (ki,kf) loop_body_opt results =
add_results_from_pred ctx results pred
in
match a.annot_content with
- | APragma (Slice_pragma (SPexpr term) | Impact_pragma (IPexpr term)) ->
+ | APragma (Slice_pragma (SPexpr term)) ->
results |>
(* to preserve the interpretation of the pragma *)
get_zone_from_term ki term |>
@@ -461,7 +461,7 @@ let get_zone_from_annot a (ki,kf) loop_body_opt results =
| APragma (Slice_pragma SPctrl) ->
(* to select the reachability of the pragma *)
add_ctrl_pragma ki results
- | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt) ->
+ | APragma (Slice_pragma SPstmt) ->
(* to preserve the effect of the statement *)
add_stmt_pragma ki results
| AAssert (_behav,pred) ->
@@ -580,7 +580,6 @@ let code_annot_filter annot ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop
| AInvariant(_,false,_) -> others
| AAllocation _ -> others
| AAssigns _ -> others
- | APragma (Impact_pragma _) -> others
| AStmtSpec _ | AExtended _ (* TODO *) -> false
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 185a7fa68fe..7a75b1ed306 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1743,15 +1743,9 @@ and slice_pragma =
| SPctrl
| SPstmt
-(** Pragmas for the impact plugin of Frama-C. *)
-and impact_pragma =
- | IPexpr of term
- | IPstmt
-
(** The various kinds of pragmas. *)
and pragma =
| Slice_pragma of slice_pragma
- | Impact_pragma of impact_pragma
(** all annotations that can be found in the code.
This type shares the name of its constructors with
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 31ead251dbc..c266a037d23 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3185,10 +3185,6 @@ class cil_printer () = object (self)
| SPctrl -> Format.pp_print_string fmt "ctrl"
| SPstmt -> Format.pp_print_string fmt "stmt"
- method private impact_pragma fmt = function
- | IPexpr t -> fprintf fmt "expr @[%a@]" self#term t
- | IPstmt -> Format.pp_print_string fmt "stmt"
-
(* TODO: add the annot ID in debug mode?*)
method code_annotation fmt ca =
let pp_for_behavs fmt l =
@@ -3209,10 +3205,6 @@ class cil_printer () = object (self)
fprintf fmt "@[%a@ %a;@]"
self#pp_acsl_keyword "slice pragma"
self#slice_pragma sp
- | APragma (Impact_pragma sp) ->
- fprintf fmt "@[%a@ %a;@]"
- self#pp_acsl_keyword "impact pragma"
- self#impact_pragma sp
| AStmtSpec(for_bhv, spec) ->
fprintf fmt "@[<hv 2>%a%a@]"
pp_for_behavs for_bhv
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index f5892672e43..cae80c9951b 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -934,15 +934,9 @@ and pp_slice_pragma fmt = function
| SPctrl -> Format.fprintf fmt "SPctrl"
| SPstmt -> Format.fprintf fmt "SPstmt"
-and pp_impact_pragma fmt = function
- | IPexpr(term) -> Format.fprintf fmt "IPexpr(%a)" pp_term term
- | IPstmt -> Format.fprintf fmt "IPstmt"
-
and pp_pragma fmt = function
| Slice_pragma(term) ->
Format.fprintf fmt "Slice_pragma(%a)" pp_slice_pragma term
- | Impact_pragma(term) ->
- Format.fprintf fmt "Impact_pragma(%a)" pp_impact_pragma term
and pp_code_annotation_node fmt = function
| AAssert(string_list,p) ->
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index 7cc180218f3..b52279be3ea 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -142,8 +142,6 @@ val pp_termination_kind :
Format.formatter -> Cil_types.termination_kind -> unit
val pp_slice_pragma :
Format.formatter -> Cil_types.slice_pragma -> unit
-val pp_impact_pragma :
- Format.formatter -> Cil_types.impact_pragma -> unit
val pp_pragma :
Format.formatter -> Cil_types.pragma -> unit
val pp_code_annotation_node :
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 8eb0730f39d..eb5658c92af 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -456,15 +456,9 @@ let print_slice_pragma fmt p =
| SPctrl -> pp_print_string fmt "ctrl"
| SPstmt -> pp_print_string fmt "stmt"
-let print_impact_pragma fmt p =
- match p with
- | IPexpr e -> fprintf fmt "expr@ %a" print_lexpr e
- | IPstmt -> pp_print_string fmt "stmt"
-
let print_pragma fmt p =
match p with
| Slice_pragma p -> fprintf fmt "slice@ pragma@ %a;" print_slice_pragma p
- | Impact_pragma p -> fprintf fmt "impact@ pragma@ %a;" print_impact_pragma p
let print_extension fmt (name, ext) =
fprintf fmt "%s %a" name (pp_list ~sep:",@ " print_lexpr) ext
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index af74c4dd1fe..2b39631d71b 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -720,17 +720,9 @@ and is_same_slice_pragma p p' env =
| SPstmt, SPstmt -> true
| (SPexpr _ | SPctrl | SPstmt), _ -> false
-and is_same_impact_pragma p p' env =
- match p, p' with
- | IPexpr t, IPexpr t' -> is_same_term t t' env
- | IPstmt, IPstmt -> true
- | (IPexpr _ | IPstmt), _ -> false
-
and is_same_pragma p p' env =
match p,p' with
| Slice_pragma p, Slice_pragma p' -> is_same_slice_pragma p p' env
- | Impact_pragma p, Impact_pragma p' -> is_same_impact_pragma p p' env
- | (Slice_pragma _ | Impact_pragma _), _ -> false
and are_same_behaviors bhvs bhvs' env =
let treat_one_behavior acc b =
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index a35aaa54e6c..e784e979278 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -875,7 +875,6 @@ class type cilVisitor = object
allocation -> allocation visitAction
method vslice_pragma: slice_pragma -> slice_pragma visitAction
- method vimpact_pragma: impact_pragma -> impact_pragma visitAction
method vdeps:
deps -> deps visitAction
@@ -1010,7 +1009,6 @@ class internal_genericCilVisitor current_func behavior queue: cilVisitor =
method vallocation _s = DoChildren
method vslice_pragma _ = DoChildren
- method vimpact_pragma _ = DoChildren
method vdeps _ = DoChildren
@@ -1844,12 +1842,6 @@ and childrenSlicePragma vis p =
let t' = visitCilTerm vis t in if t' != t then SPexpr t' else p
| SPctrl | SPstmt -> p
-and visitCilImpactPragma vis p =
- doVisitCil vis id vis#vimpact_pragma childrenImpactPragma p
-
-and childrenImpactPragma vis p = match p with
- | IPexpr t -> let t' = visitCilTerm vis t in if t' != t then IPexpr t' else p
- | IPstmt -> p
and childrenModelInfo vis m =
let field_type = visitCilLogicType vis m.mi_field_type in
@@ -1963,9 +1955,6 @@ and childrenCodeAnnot vis ca =
let p' = vPred p in if p' != p then
change_content (AAssert (behav,p'))
else ca
- | APragma (Impact_pragma t) ->
- let t' = visitCilImpactPragma vis t in
- if t' != t then change_content (APragma (Impact_pragma t')) else ca
| APragma (Slice_pragma t) ->
let t' = visitCilSlicePragma vis t in
if t' != t then change_content (APragma (Slice_pragma t')) else ca
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index a7a2f7f0eaa..c43820f0bec 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1919,7 +1919,6 @@ class type cilVisitor = object
(** @since Oxygen-20120901 *)
method vslice_pragma: slice_pragma -> slice_pragma visitAction
- method vimpact_pragma: impact_pragma -> impact_pragma visitAction
method vdeps: deps -> deps visitAction
method vfrom: from -> from visitAction
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 7fbbc120b54..ace04011a2d 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3839,10 +3839,6 @@ struct
| SPctrl -> Cil_types.SPctrl
| SPstmt -> Cil_types.SPstmt
- let impact_pragma env = function
- IPexpr t -> Cil_types.IPexpr (term env t)
- | IPstmt -> Cil_types.IPstmt
-
let code_annot_env () =
let env = append_here_label (append_pre_label (append_init_label
(Lenv.empty()))) in
@@ -3860,9 +3856,6 @@ struct
let p = predicate (code_annot_env()) p in
let p = Logic_const.toplevel_predicate ~kind p in
Cil_types.AAssert(behav,p)
- | APragma (Impact_pragma sp) ->
- Cil_types.APragma
- (Cil_types.Impact_pragma (impact_pragma (code_annot_env()) sp))
| APragma (Slice_pragma sp) ->
Cil_types.APragma
(Cil_types.Slice_pragma (slice_pragma (code_annot_env()) sp))
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 690e9c8def3..c72b5dac60a 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -714,7 +714,7 @@ let is_trivially_true p =
let is_annot_next_stmt c =
match c.annot_content with
- | AStmtSpec _ | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt) -> true
+ | AStmtSpec _ | APragma (Slice_pragma SPstmt) -> true
| AExtended(_,is_loop,{ext_name}) ->
let warn_not_a_code_annot () =
Kernel.(
@@ -730,7 +730,6 @@ let is_annot_next_stmt c =
| AAssert _ | AInvariant _ | AVariant _
| AAssigns _ | AAllocation _
| APragma (Slice_pragma (SPctrl | SPexpr _))
- | APragma (Impact_pragma (IPexpr _))
-> false
let rec add_attribute_glob_annot a g =
@@ -1182,17 +1181,9 @@ let is_same_slice_pragma p1 p2 =
| SPctrl, SPctrl | SPstmt, SPstmt -> true
| (SPexpr _ | SPctrl | SPstmt), _ -> false
-let is_same_impact_pragma p1 p2 =
- match p1,p2 with
- | IPexpr t1, IPexpr t2 -> is_same_term t1 t2
- | IPstmt, IPstmt -> true
- | (IPexpr _ | IPstmt), _ -> false
-
let is_same_pragma p1 p2 =
match p1,p2 with
| Slice_pragma p1, Slice_pragma p2 -> is_same_slice_pragma p1 p2
- | Impact_pragma p1, Impact_pragma p2 -> is_same_impact_pragma p1 p2
- | (Slice_pragma _ | Impact_pragma _), _ -> false
let rec is_same_extension x1 x2 =
Datatype.String.equal x1.ext_name x2.ext_name &&
@@ -2273,9 +2264,6 @@ let is_pragma ca =
let is_slice_pragma ca =
match ca.annot_content with APragma (Slice_pragma _) -> true | _ -> false
-let is_impact_pragma ca =
- match ca.annot_content with APragma (Impact_pragma _) -> true | _ -> false
-
let is_loop_extension ca =
match ca.annot_content with AExtended (_,is_loop,_) -> is_loop | _ -> false
@@ -2291,8 +2279,7 @@ let is_trivial_annotation a =
-> false
let is_property_pragma = function
- | Slice_pragma (SPexpr _ | SPctrl | SPstmt)
- | Impact_pragma (IPexpr _ | IPstmt) -> false
+ | Slice_pragma (SPexpr _ | SPctrl | SPstmt) -> false
(* If at some time a pragma becomes something which should be proven,
update the pragma-related code in gui/property_navigator.ml *)
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 62ace3c9ccf..48436fb2286 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -374,7 +374,6 @@ val is_same_logic_type_def :
val is_same_logic_type_info :
logic_type_info -> logic_type_info -> bool
val is_same_slice_pragma : slice_pragma -> slice_pragma -> bool
-val is_same_impact_pragma : impact_pragma -> impact_pragma -> bool
val is_same_pragma : pragma -> pragma -> bool
val is_same_code_annotation : code_annotation -> code_annotation -> bool
val is_same_global_annotation : global_annotation -> global_annotation -> bool
@@ -460,7 +459,6 @@ val is_allocation: code_annotation -> bool
val is_assigns : code_annotation -> bool
val is_pragma : code_annotation -> bool
val is_slice_pragma : code_annotation -> bool
-val is_impact_pragma : code_annotation -> bool
val is_loop_annot : code_annotation -> bool
val is_trivial_annotation : code_annotation -> bool
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index aeb6da19615..a5e76ba1bad 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -326,15 +326,9 @@ and slice_pragma =
| SPctrl
| SPstmt
-(** Pragmas for the impact plugin of Frama-C. *)
-and impact_pragma =
- | IPexpr of lexpr
- | IPstmt
-
(** The various kinds of pragmas. *)
and pragma =
| Slice_pragma of slice_pragma
- | Impact_pragma of impact_pragma
(** all annotations that can be found in the code. This type shares the name of
its constructors with {!Cil_types.code_annotation_node}. *)
diff --git a/src/plugins/impact/register.ml b/src/plugins/impact/register.ml
index 5db8ea3d06d..ba41d38ea72 100644
--- a/src/plugins/impact/register.ml
+++ b/src/plugins/impact/register.ml
@@ -116,8 +116,9 @@ let is_impact_annot code_annot =
let compute_annots () =
Ast.compute ();
- (* fill [pragmas] with all the pragmas of all the selected functions *)
- let process kf acc =
+ (* Returns the list of statements of function [kf] that have an impact
+ annotation. *)
+ let compute_impact_stmts kf acc =
(* Pragma option only accept defined functions. *)
let fundec = Kernel_function.get_definition kf in
let has_impact_annot stmt =
@@ -128,7 +129,7 @@ let compute_annots () =
if impact_stmts = [] then acc
else (kf, impact_stmts) :: acc
in
- let impact_stmts = Options.Pragma.fold process [] in
+ let impact_stmts = Options.Pragma.fold compute_impact_stmts [] in
let skip = Compute_impact.skip () in
(* compute impact analyses on each kf *)
let nodes = List.fold_left
diff --git a/src/plugins/metrics/metrics_pivot.ml b/src/plugins/metrics/metrics_pivot.ml
index ad4dd73a432..bceb343d9ed 100644
--- a/src/plugins/metrics/metrics_pivot.ml
+++ b/src/plugins/metrics/metrics_pivot.ml
@@ -391,7 +391,6 @@ class full_visitor = object(self)
method! vallocates _ = Cil.DoChildren
method! vallocation _ = Cil.DoChildren
method! vslice_pragma _ = Cil.DoChildren
- method! vimpact_pragma _ = Cil.DoChildren
method! vdeps _ = Cil.DoChildren
method! vfrom _ = Cil.DoChildren
method! vcode_annot _ =
--
GitLab