From b647224e8914d6262fe084e6a6dc129e6e0079e4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 18 Apr 2024 10:21:03 +0200
Subject: [PATCH] [kernel] Removes slice pragmas.
---
src/kernel_internals/parsing/logic_parser.mly | 11 -------
src/kernel_internals/typing/cabs2cil.ml | 1 -
src/kernel_internals/typing/cfg.ml | 2 +-
src/kernel_internals/typing/oneret.ml | 2 +-
src/kernel_services/analysis/logic_deps.ml | 13 --------
src/kernel_services/ast_data/annotations.ml | 2 +-
src/kernel_services/ast_data/cil_types.ml | 10 ------
src/kernel_services/ast_data/property.ml | 9 +-----
src/kernel_services/ast_data/property.mli | 2 +-
.../ast_printing/cil_printer.ml | 8 -----
.../ast_printing/cil_types_debug.ml | 11 -------
.../ast_printing/cil_types_debug.mli | 4 ---
.../ast_printing/description.ml | 1 -
.../ast_printing/logic_print.ml | 11 -------
src/kernel_services/ast_printing/printer.ml | 5 +--
.../ast_printing/printer_tag.ml | 5 +--
src/kernel_services/ast_queries/ast_diff.ml | 14 +-------
src/kernel_services/ast_queries/cil.ml | 19 +----------
src/kernel_services/ast_queries/cil.mli | 2 --
.../ast_queries/cil_datatype.ml | 2 +-
src/kernel_services/ast_queries/filecheck.ml | 2 +-
.../ast_queries/logic_const.ml | 2 +-
.../ast_queries/logic_typing.ml | 8 -----
.../ast_queries/logic_utils.ml | 32 +++----------------
.../ast_queries/logic_utils.mli | 7 ----
src/kernel_services/parsetree/logic_ptree.ml | 12 -------
.../e-acsl/src/analyses/e_acsl_visitor.ml | 1 -
.../src/code_generator/translate_annots.ml | 2 --
src/plugins/eva/engine/transfer_logic.ml | 3 +-
src/plugins/eva/legacy/eval_annots.ml | 4 +--
src/plugins/gui/property_navigator.ml | 2 --
src/plugins/metrics/metrics_acsl.ml | 2 +-
src/plugins/metrics/metrics_pivot.ml | 2 --
src/plugins/report/classify.ml | 1 -
src/plugins/security_slicing/components.ml | 1 -
src/plugins/server/kernel_properties.ml | 2 --
src/plugins/sparecode/spare_marks.ml | 1 -
src/plugins/wp/cfgCalculus.ml | 2 +-
src/plugins/wp/cfgGenerator.ml | 2 +-
src/plugins/wp/wpPropId.ml | 2 +-
40 files changed, 23 insertions(+), 201 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 98c190c409a..e233ab3d15b 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1474,7 +1474,6 @@ beg_pragma_or_code_annotation:
;
pragma_or_code_annotation:
-| slice_pragma { APragma (Slice_pragma $1) }
| code_annotation { $1 [] }
;
@@ -1516,16 +1515,6 @@ code_annotation:
}
;
-slice_pragma:
-| SLICE PRAGMA any_identifier lexpr SEMICOLON
- { if $3 = "expr" then SPexpr $4
- else raise (Not_well_formed (loc $sloc, "Unknown slice pragma")) }
-| SLICE PRAGMA any_identifier SEMICOLON
- { if $3 = "ctrl" then SPctrl
- else if $3 = "stmt" then SPstmt
- else raise (Not_well_formed (loc $sloc, "Unknown slice pragma")) }
-;
-
/*** declarations and logical definitions ***/
decl_list:
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 8317846aaa3..4bc7199b1be 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9823,7 +9823,6 @@ and doBody local_env (blk: Cabs.block) : chunk =
(fun x -> x.Logic_ptree.b_name)
s.Logic_ptree.spec_behavior,
true
- | CODE_ANNOT(Logic_ptree.APragma _,_) -> [], true
| CODE_ANNOT
(Logic_ptree.AExtended(_,is_loop,(name,_)),loc) ->
let source = fst loc in
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index d7c54a7de77..6a5bb2caf6c 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -363,7 +363,7 @@ let xform_switch_block ?(keepSwitch=false) b =
let assert_of_clause f ca =
match ca.annot_content with
| AAssert _ | AInvariant _ | AVariant _
- | AAssigns _ | AAllocation _ | APragma _ | AExtended _ -> Logic_const.ptrue
+ | AAssigns _ | AAllocation _ | AExtended _ -> Logic_const.ptrue
| AStmtSpec (_bhv,s) ->
let open Logic_const in
List.fold_left
diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml
index c514e975488..6f805da8dae 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -242,7 +242,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit =
let assert_of_returns ca =
match ca.annot_content with
| AAssert _ | AInvariant _ | AVariant _
- | AAssigns _ | AAllocation _ | APragma _ | AExtended _ -> ptrue
+ | AAssigns _ | AAllocation _ | AExtended _ -> ptrue
| AStmtSpec (_bhvs,s) ->
let res =
List.fold_left
diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
index c465ce14c60..57de8321c49 100644
--- a/src/kernel_services/analysis/logic_deps.ml
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -498,18 +498,6 @@ 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)) ->
- results |>
- (* to preserve the interpretation of the pragma *)
- get_zone_from_term ki term |>
- (* to select the reachability of the pragma *)
- add_ctrl_slice ki
- | APragma (Slice_pragma SPctrl) ->
- (* to select the reachability of the pragma *)
- add_ctrl_slice ki results
- | APragma (Slice_pragma SPstmt) ->
- (* to preserve the effect of the statement *)
- add_stmt_slice ki results
| AAssert (_behav,pred) ->
(* to preserve the interpretation of the assertion *)
get_zone_from_pred ki pred.tp_statement results
@@ -635,7 +623,6 @@ let from_func_annots iter_on_kf_stmt code_annot_filter kf =
(** To quickly build a annotation filter *)
let code_annot_filter annot ~threat ~user_assert ~slicing_annot ~loop_inv ~loop_var ~others =
match annot.annot_content with
- | APragma (Slice_pragma _) -> slicing_annot
| AAssert _ ->
(match Alarms.find annot with
| None -> user_assert
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 44e170a7060..db1b59e51d9 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -1637,7 +1637,7 @@ let do_add_code_annot ~keep_empty emitter ?kf stmt ca =
Kernel.fatal
"More than one loop assigns clause for a statement. \
Annotations internal state broken.")
- | APragma _ | AExtended _ ->
+ | AExtended _ ->
fill_tables ca (Property.ip_of_code_annot kf stmt ca)
let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 7a75b1ed306..e144f4363da 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1737,15 +1737,6 @@ and behavior = {
(** extensions *)
}
-(** Pragmas for the slicing plugin of Frama-C. *)
-and slice_pragma =
- | SPexpr of term
- | SPctrl
- | SPstmt
-
-(** The various kinds of pragmas. *)
-and pragma =
- | Slice_pragma of slice_pragma
(** all annotations that can be found in the code.
This type shares the name of its constructors with
@@ -1778,7 +1769,6 @@ and code_annotation_node =
At most one clause associated to a given (statement, behavior) couple.
@since Oxygen-20120901 when [b_allocation] has been added. *)
- | APragma of pragma (** pragma. *)
| AExtended of string list * bool * acsl_extension
(** extension in a code or loop annotation.
Boolean flag is true for loop extensions and false for code extensions
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 4789db180f6..1e5f0f1fdd9 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -419,7 +419,7 @@ let get_for_behaviors = function
| AStmtSpec(bhvs,_)
| AAssigns(bhvs,_)
| AAllocation(bhvs,_) -> bhvs
- | AVariant _ | APragma _ | AExtended _ -> []
+ | AVariant _ | AExtended _ -> []
end
| IPAxiomatic _
@@ -445,7 +445,6 @@ let has_status_ca = function
| AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _ | AAllocation _
| AAssigns _ -> true
| AExtended(_,_,e) -> has_status_ext e
- | APragma _ -> false
let has_status_pkind = function
| PKAssumes _ -> false
@@ -804,7 +803,6 @@ module Ordered_by_function = Datatype.Make_with_collections(
| IPPredicate { ip_kind = PKEnsures _ } -> 10
| IPCodeAnnot { ica_ca = { annot_content = AAssert _ }} -> 11
| IPCodeAnnot { ica_ca = { annot_content = AInvariant _ }} -> 12
- | IPCodeAnnot { ica_ca = { annot_content = APragma _ }} -> 13
| IPAssigns _ -> 14
| IPFrom _ -> 15
| IPAllocation _ -> 16
@@ -1184,8 +1182,6 @@ struct
| IPCodeAnnot {ica_kf=kf; ica_stmt=stmt; ica_ca={annot_content=AStmtSpec _}} ->
[ K kf ; A "contract" ; S stmt ]
- | IPCodeAnnot {ica_kf=kf; ica_stmt=stmt; ica_ca={annot_content=APragma _}} ->
- [ K kf ; A "pragma" ; S stmt ]
| IPCodeAnnot {ica_kf=kf; ica_stmt=stmt;
ica_ca={annot_content=AExtended (_, _, {ext_name})}} ->
[ K kf ; A ext_name ; S stmt ]
@@ -1468,9 +1464,6 @@ let ip_of_code_annot kf stmt ca =
| AAssigns _ ->
Option.to_list (ip_assigns_of_code_annot kf ki ca)
@ ip_from_of_code_annot kf ki ca
- | APragma p when Logic_utils.is_property_pragma p ->
- [ IPCodeAnnot {ica_kf=kf; ica_stmt=stmt; ica_ca=ca} ]
- | APragma _ -> []
| AExtended(_,_,ext) ->
if ext.ext_has_status then
[IPExtended {ie_loc=ELStmt(kf,stmt); ie_ext=ext}]
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 90d5044211b..2b86486b245 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -47,7 +47,7 @@ type behavior_or_loop = (* private *)
based on different sets of active behaviors. *)
| Id_loop of code_annotation
-(** Only AAssert, AInvariant, or APragma. Other code annotations are
+(** Only AAssert or AInvariant. Other code annotations are
dispatched as identified_property of their own. *)
type identified_code_annotation = {
ica_kf : kernel_function;
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index c266a037d23..75c2da8a093 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3180,10 +3180,6 @@ class cil_printer () = object (self)
(pp_list nl_complete self#complete_behaviors) complete
(pp_list false self#disjoint_behaviors) disjoint
- method private slice_pragma fmt = function
- |SPexpr t -> fprintf fmt "expr @[%a@]" self#term t
- | SPctrl -> Format.pp_print_string fmt "ctrl"
- | SPstmt -> Format.pp_print_string fmt "stmt"
(* TODO: add the annot ID in debug mode?*)
method code_annotation fmt ca =
@@ -3201,10 +3197,6 @@ class cil_printer () = object (self)
pp_for_behavs behav
self#pp_acsl_keyword (string_of_assert p.tp_kind)
self#predicate p.tp_statement
- | APragma (Slice_pragma sp) ->
- fprintf fmt "@[%a@ %a;@]"
- self#pp_acsl_keyword "slice pragma"
- self#slice_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 cae80c9951b..12e2557c256 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -929,15 +929,6 @@ and pp_termination_kind fmt = function
| Continues -> Format.fprintf fmt "Continues"
| Returns -> Format.fprintf fmt "Returns"
-and pp_slice_pragma fmt = function
- | SPexpr(term) -> Format.fprintf fmt "SPexpr(%a)" pp_term term
- | SPctrl -> Format.fprintf fmt "SPctrl"
- | SPstmt -> Format.fprintf fmt "SPstmt"
-
-and pp_pragma fmt = function
- | Slice_pragma(term) ->
- Format.fprintf fmt "Slice_pragma(%a)" pp_slice_pragma term
-
and pp_code_annotation_node fmt = function
| AAssert(string_list,p) ->
Format.fprintf fmt "AAssert(%a,%a)"
@@ -956,8 +947,6 @@ and pp_code_annotation_node fmt = function
| AAllocation(string_list,allocation) ->
Format.fprintf fmt "AAllocation(%a,%a)" (pp_list pp_string) string_list
pp_allocation allocation
- | APragma(pragma) ->
- Format.fprintf fmt "APragma(%a)" pp_pragma pragma
| AExtended(string_list,is_loop,acsl_extension) ->
Format.fprintf fmt "AExtended(%a,%B,%a)"
(pp_list pp_string) string_list is_loop pp_acsl_extension acsl_extension
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index b52279be3ea..dea0ff2b928 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -140,10 +140,6 @@ val pp_acsl_extension_kind :
val pp_behavior : Format.formatter -> Cil_types.behavior -> unit
val pp_termination_kind :
Format.formatter -> Cil_types.termination_kind -> unit
-val pp_slice_pragma :
- Format.formatter -> Cil_types.slice_pragma -> unit
-val pp_pragma :
- Format.formatter -> Cil_types.pragma -> unit
val pp_code_annotation_node :
Format.formatter -> Cil_types.code_annotation_node -> unit
val pp_funspec : Format.formatter -> Cil_types.funspec -> unit
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index 53d007c1f2d..ab7ccf849a4 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -126,7 +126,6 @@ let pp_code_annot fmt ca =
Format.fprintf fmt "invariant%a%a" pp_for bs pp_top tp
| AAssigns(bs,_) -> Format.fprintf fmt "assigns%a" pp_for bs
| AAllocation(bs,_) -> Format.fprintf fmt "allocates_frees%a" pp_for bs
- | APragma _ -> Format.pp_print_string fmt "pragma"
| AVariant _ -> Format.pp_print_string fmt "variant"
| AStmtSpec _ -> Format.pp_print_string fmt "block contract"
| AExtended _ -> Format.pp_print_string fmt "extension"
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index eb5658c92af..aeba051d5cd 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -450,16 +450,6 @@ let print_spec fmt spec =
~sep:"@\n" ~suf:"@\n" (pp_list ~sep:",@ " pp_print_string))
spec.spec_disjoint_behaviors
-let print_slice_pragma fmt p =
- match p with
- | SPexpr e -> fprintf fmt "expr@ %a" print_lexpr e
- | SPctrl -> pp_print_string fmt "ctrl"
- | SPstmt -> 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
-
let print_extension fmt (name, ext) =
fprintf fmt "%s %a" name (pp_list ~sep:",@ " print_lexpr) ext
@@ -488,7 +478,6 @@ let print_code_annot fmt ca =
fprintf fmt "%aloop@ %a" print_behaviors bhvs print_assigns a
| AAllocation (bhvs,fa) ->
fprintf fmt "%a%a" print_behaviors bhvs (print_allocation ~isloop:true) fa
- | APragma p -> print_pragma fmt p
| AExtended (bhvs, is_loop, e) ->
fprintf fmt "%a%s%a"
print_behaviors bhvs
diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml
index 7c50dafb7ad..dd9d31dca51 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/src/kernel_services/ast_printing/printer.ml
@@ -74,12 +74,9 @@ let compare_annotations la1 la2 =
| AAllocation _, AAllocation _ -> total_order
| AAllocation _, _ -> -1
- | AVariant _, (APragma _ | AExtended _) -> -1
+ | AVariant _, AExtended _ -> -1
| AVariant _, AVariant _ -> total_order
| AVariant _, _ -> 1
- | APragma _, AExtended _ -> -1
- | APragma _, APragma _ -> total_order
- | APragma _, _ -> 1
| AExtended _, AExtended _ -> total_order
| AExtended _, _ -> 1
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index b849b8f00b6..f23eb2643d9 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -823,10 +823,7 @@ struct
method! code_annotation fmt ca =
match ca.annot_content with
- | APragma p when not (Logic_utils.is_property_pragma p) ->
- (* Not currently localizable. Will be linked to the next stmt *)
- super#code_annotation fmt ca
- | AAssert _ | AInvariant _ | APragma _ | AVariant _ ->
+ | AAssert _ | AInvariant _ | AVariant _ ->
let ip =
Property.ip_of_code_annot_single
(Option.get self#current_kf)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 2b39631d71b..9dc42b8d8cf 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -713,17 +713,6 @@ and is_same_behavior b b' env =
and is_same_variant (v,m) (v',m') env =
is_same_term v v' env && is_same_opt is_matching_logic_info m m' env
-and is_same_slice_pragma p p' env =
- match p, p' with
- | SPexpr t, SPexpr t' -> is_same_term t t' env
- | SPctrl, SPctrl -> true
- | SPstmt, SPstmt -> true
- | (SPexpr _ | SPctrl | SPstmt), _ -> 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
-
and are_same_behaviors bhvs bhvs' env =
let treat_one_behavior acc b =
match List.partition (fun b' -> b.b_name = b'.b_name) acc with
@@ -761,13 +750,12 @@ and is_same_code_annotation a a' env =
is_same_behavior_set bhvs bhvs' && is_same_assigns a a' env
| AAllocation(bhvs, a), AAllocation(bhvs',a') ->
is_same_behavior_set bhvs bhvs' && is_same_allocation a a' env
- | APragma p, APragma p' -> is_same_pragma p p' env
| AExtended (bhvs, is_next, ext),
AExtended (bhvs', is_next', ext') ->
is_same_behavior_set bhvs bhvs' && is_next = is_next' &&
is_same_acsl_extension ext ext' env
| (AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _ | AAssigns _
- | AAllocation _ | APragma _ | AExtended _), _ -> false
+ | AAllocation _ | AExtended _), _ -> false
and is_same_logic_type t t' env =
match t,t' with
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index e784e979278..1b3ace6387f 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -874,8 +874,6 @@ class type cilVisitor = object
method vallocation:
allocation -> allocation visitAction
- method vslice_pragma: slice_pragma -> slice_pragma visitAction
-
method vdeps:
deps -> deps visitAction
@@ -1008,8 +1006,6 @@ class internal_genericCilVisitor current_func behavior queue: cilVisitor =
method vallocates _s = DoChildren
method vallocation _s = DoChildren
- method vslice_pragma _ = DoChildren
-
method vdeps _ = DoChildren
method vfrom _ = DoChildren
@@ -1086,7 +1082,7 @@ let flatten_transient_sub_blocks b =
| None -> false
| Some {
skind =
- Instr (Code_annot ({ annot_content = AStmtSpec _ | APragma _}, _))}
+ Instr (Code_annot ({ annot_content = AStmtSpec _ }, _))}
-> true
| Some _ -> false
in
@@ -1833,16 +1829,6 @@ and childrenSpec vis s =
*)
s
-and visitCilSlicePragma vis p =
- doVisitCil vis id vis#vslice_pragma childrenSlicePragma p
-
-and childrenSlicePragma vis p =
- match p with
- | SPexpr t ->
- let t' = visitCilTerm vis t in if t' != t then SPexpr t' else p
- | SPctrl | SPstmt -> p
-
-
and childrenModelInfo vis m =
let field_type = visitCilLogicType vis m.mi_field_type in
let base_type = visitCilType vis m.mi_base_type in
@@ -1955,9 +1941,6 @@ and childrenCodeAnnot vis ca =
let p' = vPred p in if p' != p then
change_content (AAssert (behav,p'))
else ca
- | APragma (Slice_pragma t) ->
- let t' = visitCilSlicePragma vis t in
- if t' != t then change_content (APragma (Slice_pragma t')) else ca
| AStmtSpec (behav,s) ->
let s' = vSpec s in
if s' != s then change_content (AStmtSpec (behav,s')) else ca
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index c43820f0bec..e54b77b2f41 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1918,8 +1918,6 @@ class type cilVisitor = object
method vallocation: allocation -> allocation visitAction
(** @since Oxygen-20120901 *)
- method vslice_pragma: slice_pragma -> slice_pragma visitAction
-
method vdeps: deps -> deps visitAction
method vfrom: from -> from visitAction
method vcode_annot: code_annotation -> code_annotation visitAction
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 799e52d1780..f11de6f809e 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2471,7 +2471,7 @@ module Code_annotation = struct
| AAssert(_,{ tp_statement = {pred_loc=loc}})
| AInvariant(_,_,{tp_statement = {pred_loc=loc}})
| AVariant({term_loc=loc},_) -> Some loc
- | AAssigns _ | AAllocation _ | APragma _ | AExtended _
+ | AAssigns _ | AAllocation _ | AExtended _
| AStmtSpec _ -> None
end
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 0c6abfa91ee..855cce6149e 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -651,7 +651,7 @@ module Base_checker = struct
"%s is not a code annotation extension" ext_name);
my_labels)
| AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _
- | AAssigns _ | AAllocation _ | APragma _ -> my_labels
+ | AAssigns _ | AAllocation _ -> my_labels
in
logic_labels <- my_labels @ logic_labels;
(* on non-normalized code, we can't really check the scope of behavior
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index a537c6ab681..5b66f11b696 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -106,7 +106,7 @@ let refresh_spec s =
let refresh_code_annotation annot =
let content =
match annot.annot_content with
- | AAssert _ | AInvariant _ | AAllocation _ | AVariant _ | APragma _
+ | AAssert _ | AInvariant _ | AAllocation _ | AVariant _
| AExtended _ as c -> c
| AStmtSpec(l,spec) -> AStmtSpec(l, refresh_spec spec)
| AAssigns(l,a) -> AAssigns(l, refresh_assigns a)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index ace04011a2d..2d75c19ccdf 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3834,11 +3834,6 @@ struct
List.fold_left add_formal env formals
in type_spec old_behaviors vi.vdecl false log_return_typ env s
- let slice_pragma env = function
- SPexpr t -> Cil_types.SPexpr (term env t)
- | SPctrl -> Cil_types.SPctrl
- | SPstmt -> Cil_types.SPstmt
-
let code_annot_env () =
let env = append_here_label (append_pre_label (append_init_label
(Lenv.empty()))) in
@@ -3856,9 +3851,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 (Slice_pragma sp) ->
- Cil_types.APragma
- (Cil_types.Slice_pragma (slice_pragma (code_annot_env()) sp))
| AStmtSpec (behav,s) ->
(* function behaviors and statement behaviors are not at the
same level. Do not mix them in a complete or disjoint clause
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index c72b5dac60a..4fbd3210b47 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) -> true
+ | AStmtSpec _ -> true
| AExtended(_,is_loop,{ext_name}) ->
let warn_not_a_code_annot () =
Kernel.(
@@ -728,9 +728,7 @@ let is_annot_next_stmt c =
| Ext_code_annot Ext_next_both-> not is_loop
| Ext_contract | Ext_global -> warn_not_a_code_annot () ; false)
| AAssert _ | AInvariant _ | AVariant _
- | AAssigns _ | AAllocation _
- | APragma (Slice_pragma (SPctrl | SPexpr _))
- -> false
+ | AAssigns _ | AAllocation _ -> false
let rec add_attribute_glob_annot a g =
match g with
@@ -1175,16 +1173,6 @@ let is_same_logic_type_info t1 t2 =
is_same_attributes t1.lt_attr t2.lt_attr &&
is_same_opt is_same_logic_type_def t1.lt_def t2.lt_def
-let is_same_slice_pragma p1 p2 =
- match p1,p2 with
- SPexpr t1, SPexpr t2 -> is_same_term t1 t2
- | SPctrl, SPctrl | SPstmt, SPstmt -> true
- | (SPexpr _ | SPctrl | SPstmt), _ -> false
-
-let is_same_pragma p1 p2 =
- match p1,p2 with
- | Slice_pragma p1, Slice_pragma p2 -> is_same_slice_pragma p1 p2
-
let rec is_same_extension x1 x2 =
Datatype.String.equal x1.ext_name x2.ext_name &&
(x1.ext_has_status = x2.ext_has_status) &&
@@ -1212,11 +1200,10 @@ let is_same_code_annotation (ca1:code_annotation) (ca2:code_annotation) =
| AAllocation(l1,fa1), AAllocation(l2,fa2) ->
is_same_list (=) l1 l2 &&
is_same_allocation fa1 fa2
- | APragma p1, APragma p2 -> is_same_pragma p1 p2
| AExtended (l1,b1,e1), AExtended(l2,b2,e2) ->
is_same_list (=) l1 l2 && ((b1:bool) = b2) && is_same_extension e1 e2
| (AAssert _ | AStmtSpec _ | AInvariant _ | AExtended _
- | AVariant _ | AAssigns _ | AAllocation _ | APragma _ ), _ -> false
+ | AVariant _ | AAssigns _ | AAllocation _), _ -> false
let is_same_model_info mi1 mi2 =
mi1.mi_name = mi2.mi_name &&
@@ -2258,12 +2245,6 @@ let is_allocation ca =
let is_assigns ca =
match ca.annot_content with AAssigns _ -> true | _ -> false
-let is_pragma ca =
- match ca.annot_content with APragma _ -> true | _ -> false
-
-let is_slice_pragma ca =
- match ca.annot_content with APragma (Slice_pragma _) -> true | _ -> false
-
let is_loop_extension ca =
match ca.annot_content with AExtended (_,is_loop,_) -> is_loop | _ -> false
@@ -2274,15 +2255,10 @@ let is_loop_annot s =
let is_trivial_annotation a =
match a.annot_content with
| AAssert (_,a) -> is_trivially_true a.tp_statement
- | APragma _ | AStmtSpec _ | AInvariant _ | AVariant _
+ | AStmtSpec _ | AInvariant _ | AVariant _
| AAssigns _| AAllocation _ | AExtended _
-> false
-let is_property_pragma = function
- | 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 *)
-
let extract_contract l =
List.fold_right
(fun ca l -> match ca.annot_content with
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 48436fb2286..9ef563d8833 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -373,8 +373,6 @@ val is_same_logic_type_def :
logic_type_def -> logic_type_def -> bool
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_pragma : pragma -> pragma -> bool
val is_same_code_annotation : code_annotation -> code_annotation -> bool
val is_same_global_annotation : global_annotation -> global_annotation -> bool
val is_same_axiomatic :
@@ -457,15 +455,10 @@ val is_invariant : code_annotation -> bool
val is_variant : code_annotation -> bool
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_loop_annot : code_annotation -> bool
val is_trivial_annotation : code_annotation -> bool
-val is_property_pragma : pragma -> bool
-(** Should this pragma be proved by plugins *)
-
val extract_contract :
code_annotation list -> (string list * funspec) list
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index a5e76ba1bad..79b07e9374d 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -319,17 +319,6 @@ type spec = {
It is possible to have more than one set of disjoint behaviors *)
}
-(** Pragmas for the value analysis plugin of Frama-C. *)
-
-and slice_pragma =
- | SPexpr of lexpr
- | SPctrl
- | SPstmt
-
-(** The various kinds of pragmas. *)
-and pragma =
- | Slice_pragma of slice_pragma
-
(** all annotations that can be found in the code. This type shares the name of
its constructors with {!Cil_types.code_annotation_node}. *)
type code_annot =
@@ -360,7 +349,6 @@ type code_annot =
At most one clause associated to a given (statement, behavior) couple.
@since Oxygen-20120901 when [b_allocation] has been added. *)
- | APragma of pragma (** pragma. *)
| AExtended of string list * bool * extension
(** extension in a code or loop (when boolean flag is true) annotation.
@since Silicon-20161101
diff --git a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
index 8674b84187c..343634fd4b6 100644
--- a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
+++ b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
@@ -520,7 +520,6 @@ class visitor cat
~not_yet:"allocates"
~f:self#visit_allocates
allocates
- | APragma _ -> ()
| AExtended _ -> ()
)
stmt;
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 439c2dba354..3f484c98307 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -131,7 +131,6 @@ let pre_code_annotation kf stmt env annot =
then Env.not_yet env "allocation")
ppts;
env
- | APragma _ -> Env.not_yet env "pragma"
| AExtended _ -> env (* never translate extensions. *)
in
Env.handle_error convert env
@@ -150,7 +149,6 @@ let post_code_annotation kf stmt env annot =
| AVariant _
| AAssigns _
| AAllocation _
- | APragma _
| AExtended _ -> env
in
Env.handle_error convert env
diff --git a/src/plugins/eva/engine/transfer_logic.ml b/src/plugins/eva/engine/transfer_logic.ml
index 41aa1bc0dcc..94a4ff04fdf 100644
--- a/src/plugins/eva/engine/transfer_logic.ml
+++ b/src/plugins/eva/engine/transfer_logic.ml
@@ -162,7 +162,7 @@ let pp_code_annot fmt ca =
Format.fprintf fmt "loop invariant%a" Description.pp_named tp_statement
| AExtended (_, _, extension) ->
Format.fprintf fmt "%s annotation" extension.ext_name;
- | APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _ ->
+ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _ ->
assert false (* currently not treated by Eva *)
(* location of the given code annotation. If unknown, use the location of the
@@ -690,7 +690,6 @@ module Make
let record = record && p.tp_kind <> Admit in
let reduce = p.tp_kind <> Check in
aux ~record ~reduce code_annot behav p.tp_statement
- | APragma _
| AInvariant (_, false, _)
| AVariant _ | AAssigns _ | AAllocation _
| AStmtSpec _ (*TODO*) -> states
diff --git a/src/plugins/eva/legacy/eval_annots.ml b/src/plugins/eva/legacy/eval_annots.ml
index beff72440d8..e82b85b231c 100644
--- a/src/plugins/eva/legacy/eval_annots.ml
+++ b/src/plugins/eva/legacy/eval_annots.ml
@@ -32,7 +32,7 @@ let code_annotation_text ca =
match ca.annot_content with
| AAssert (_, {tp_kind}) -> Cil_printer.name_of_assert tp_kind
| AInvariant _ -> "loop invariant"
- | APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
+ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
| AExtended _ ->
assert false (* currently not treated by Value *)
@@ -210,7 +210,7 @@ let mark_green_and_red () =
| Eval_terms.Unknown -> ()
end
| AInvariant (_, false, _) | AStmtSpec _ | AVariant _ | AAssigns _
- | AAllocation _ | APragma _ | AExtended _ -> ()
+ | AAllocation _ | AExtended _ -> ()
in
Annotations.iter_all_code_annot do_code_annot
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 1381ced216a..5592bd188cd 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -654,8 +654,6 @@ let make_panel (main_ui:main_window_extension_points) =
end
| IPCodeAnnot {ica_ca={annot_content = AInvariant _}} ->
invariant.get ()
- | IPCodeAnnot {ica_ca={annot_content = APragma p}} ->
- Logic_utils.is_property_pragma p (* currently always false. *)
| IPCodeAnnot _ -> false (* status of inner nodes *)
| IPAllocation {ial_kinstr=Kglobal} -> allocations.get ()
| IPAllocation {ial_kinstr=Kstmt _;ial_bhv=Id_loop _} ->
diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml
index cd3bd66a369..073fdad49b4 100644
--- a/src/plugins/metrics/metrics_acsl.ml
+++ b/src/plugins/metrics/metrics_acsl.ml
@@ -249,7 +249,7 @@ let add_code_annot_stats stmt _ ca =
List.iter
(function (_,FromAny) -> () | (_,From _) -> incr_all incr_loop_froms) l
| AAllocation _ -> () (* TODO *)
- | APragma _ | AExtended _ -> ()
+ | AExtended _ -> ()
let compute () =
if not (Computed.get()) then begin
diff --git a/src/plugins/metrics/metrics_pivot.ml b/src/plugins/metrics/metrics_pivot.ml
index bceb343d9ed..11e68d855c3 100644
--- a/src/plugins/metrics/metrics_pivot.ml
+++ b/src/plugins/metrics/metrics_pivot.ml
@@ -91,7 +91,6 @@ let node_of_code_annotation_node = function
| AVariant _ -> "variant"
| AAssigns _ -> "assigns"
| AAllocation _ -> "allocation"
- | APragma _ -> "ca_pragma"
| AExtended _ -> "extended"
let node_of_global_annotation = function
@@ -390,7 +389,6 @@ class full_visitor = object(self)
method! vfrees _ = Cil.DoChildren
method! vallocates _ = Cil.DoChildren
method! vallocation _ = Cil.DoChildren
- method! vslice_pragma _ = Cil.DoChildren
method! vdeps _ = Cil.DoChildren
method! vfrom _ = Cil.DoChildren
method! vcode_annot _ =
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index 98cf1b9b351..5ff525c353c 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -421,7 +421,6 @@ let rec monitored_property ip =
| IPFrom _-> true
| IPDecrease _ -> true
| IPCodeAnnot {ica_ca = { annot_content = AStmtSpec _ }} -> false
- | IPCodeAnnot {ica_ca = { annot_content = APragma _ }} -> false
| IPCodeAnnot {ica_ca = { annot_content = AExtended _ }} -> true
| IPCodeAnnot {ica_ca = { annot_content = AAssert _ }} -> true
| IPCodeAnnot {ica_ca = { annot_content = AInvariant _ }} -> true
diff --git a/src/plugins/security_slicing/components.ml b/src/plugins/security_slicing/components.ml
index 74349068d99..d7850728124 100644
--- a/src/plugins/security_slicing/components.ml
+++ b/src/plugins/security_slicing/components.ml
@@ -70,7 +70,6 @@ let search_security_requirements () =
| AStmtSpec { spec_requires = l } ->
List.exists
(is_security_predicate $ Logic_const.pred_of_id_pred) l
- | APragma _
| AInvariant _ (* | ALoopBehavior _ *)
(* [JS 2008/02/26] may contain a security predicate *)
| AVariant _ | AAssigns _
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 8d84bb2874a..c80c97892fa 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -70,7 +70,6 @@ struct
let t_loop_assigns = t_loop "assigns"
let t_loop_variant = t_loop "variant"
let t_loop_allocates = t_loop "allocates"
- let t_pragma = t_loop "pragma"
let t_reachable = t_kind "reachable" "Reachable statement"
let t_code_contract = t_kind "code_contract" "Statement contract"
@@ -119,7 +118,6 @@ struct
| AVariant _ -> t_loop_variant
| AAssigns _ -> t_loop_assigns
| AAllocation _ -> t_loop_allocates
- | APragma _ -> t_pragma
| AExtended(_,_,{ext_name=_}) -> t_ext
end
| IPAllocation _ -> t_allocates
diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml
index a376b69751a..b37fe42620e 100644
--- a/src/plugins/sparecode/spare_marks.ml
+++ b/src/plugins/sparecode/spare_marks.ml
@@ -330,7 +330,6 @@ let select_annotations ~select_annot ~select_slice_pragma proj =
then debug 1 "pdg bottom: skip annotations"
else begin
match annot.Cil_types.annot_content with
- | Cil_types.APragma (Cil_types.Slice_pragma _) -> select_slice_pragma
| Cil_types.AAssert _-> (* Never select alarms, they are not useful *)
(match Alarms.find annot with
| None -> select_annot
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index e063a84fe15..ec6b9b0cf75 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -76,7 +76,7 @@ let is_selected_ca (m: mode) ~goal (ca: code_annotation) =
| AInvariant(forb,_,_)
-> is_selected_for m ~goal forb
| AVariant _ -> is_default_bhv m
- | AExtended _ | AStmtSpec _ | APragma _ ->
+ | AExtended _ | AStmtSpec _ ->
assert false (* n/a *)
let is_active_mode ~mode ~goal (p: Property.t) =
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index bf683b0c973..f9c0980cbdc 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -163,7 +163,7 @@ let rec strategy_ip model pool target =
-> add_fun_task model pool ~kf ~bhvs:[bhv] ~target ()
| IPCodeAnnot { ica_kf = kf ; ica_ca = ca } ->
begin match ca.annot_content with
- | AExtended _ | APragma _ -> ()
+ | AExtended _ -> ()
| AStmtSpec(fors,_) ->
(*TODO*) notyet target ;
add_fun_task model pool ~kf ~bhvs:(select kf fors) ()
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index e9a8931cb1a..0d00f2dc2ef 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -644,7 +644,7 @@ let annot_hints hs = function
List.iter (add_hint hs) bs ;
assigns_hints hs froms
| AAllocation _ | AAssigns(_,WritesAny) | AStmtSpec _
- | AVariant _ | APragma _ | AExtended _ -> ()
+ | AVariant _ | AExtended _ -> ()
let property_hints hs =
let open Property in function
--
GitLab