From 1d043d3dc1d162bcc4b66fed6fa63e206c7f9946 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 17 Apr 2024 18:02:28 +0200
Subject: [PATCH] [kernel] remove loop_pragma
---
bin/frama-c.debug | 1 -
ivette/src/frama-c/kernel/Properties.tsx | 1 -
src/kernel_internals/parsing/logic_parser.mly | 11 ----------
src/kernel_services/analysis/logic_deps.ml | 11 +---------
src/kernel_services/ast_data/cil_types.ml | 5 -----
.../ast_printing/cil_printer.ml | 9 --------
.../ast_printing/cil_types_debug.ml | 6 ------
.../ast_printing/cil_types_debug.mli | 2 --
.../ast_printing/logic_print.ml | 5 -----
src/kernel_services/ast_queries/ast_diff.ml | 7 +------
src/kernel_services/ast_queries/cil.ml | 16 --------------
src/kernel_services/ast_queries/cil.mli | 1 -
.../ast_queries/logic_typing.ml | 7 -------
.../ast_queries/logic_utils.ml | 21 +++----------------
.../ast_queries/logic_utils.mli | 4 ----
src/kernel_services/parsetree/logic_ptree.ml | 5 -----
src/plugins/metrics/metrics_pivot.ml | 1 -
src/plugins/server/kernel_properties.ml | 4 ++--
src/plugins/wp/RefUsage.ml | 1 -
src/plugins/wp/RegionAccess.ml | 1 -
src/plugins/wp/wpReached.ml | 7 -------
21 files changed, 7 insertions(+), 119 deletions(-)
diff --git a/bin/frama-c.debug b/bin/frama-c.debug
index 14eab40782e..4140818cbff 100755
--- a/bin/frama-c.debug
+++ b/bin/frama-c.debug
@@ -124,7 +124,6 @@ install_printer Cil_types_debug.pp_predicate
install_printer Cil_types_debug.pp_spec
install_printer Cil_types_debug.pp_acsl_extension
install_printer Cil_types_debug.pp_acsl_extension_kind
-install_printer Cil_types_debug.pp_loop_pragma
install_printer Cil_types_debug.pp_slice_pragma
install_printer Cil_types_debug.pp_impact_pragma
install_printer Cil_types_debug.pp_pragma
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index cac61e927ed..7aa7f20eee3 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -210,7 +210,6 @@ function filterKind(
case 'behavior': return filter('kind.behavior');
case 'reachable': return filter('kind.reachable');
case 'axiomatic': return filter('kind.axiomatic');
- case 'loop_pragma': return filter('kind.pragma');
case 'assumes': return filter('kind.assumes');
default: return filter('kind.others');
}
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 5793c2feb49..bfe8101644b 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1402,8 +1402,6 @@ loop_annot_stack:
check_empty
(pos,"loop annotations can have at most one variant.") v ;
(i,fa,a,b,AVariant loop_variant::v,p,e) }
-| loop_pragma loop_annot_opt
- { let (i,fa,a,b,v,p,e) = $2 in (i,fa,a,b,v,APragma (Loop_pragma $1)::p,e) }
| loop_grammar_extension loop_annot_opt {
let (i,fa,a,b,v,p,e) = $2 in
(i,fa,a,b,v,p, $1::e)
@@ -1458,15 +1456,6 @@ loop_grammar_extension:
}
;
-loop_pragma:
-| LOOP PRAGMA any_identifier ne_lexpr_list SEMICOLON
- { if $3 = "UNROLL_LOOP" || $3 = "UNROLL" then
- (if $3 <> "UNROLL" then
- Format.eprintf "Warning: use of deprecated keyword '%s'.\nShould use 'UNROLL' instead.@." $3;
- Unroll_specs $4)
- else raise (Not_well_formed (loc $sloc,"Unknown loop pragma")) }
-;
-
/*** code annotations ***/
beg_pragma_or_code_annotation:
diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
index 65883a64ce2..58ebef5f16c 100644
--- a/src/kernel_services/analysis/logic_deps.ml
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -478,15 +478,6 @@ 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)) ->
- (* to select the declaration of the variables *)
- List.fold_left
- (fun results term -> {
- results with
- locals = Varinfo.Set.union (extract_locals_from_term term) results.locals;
- labels = Logic_label.Set.union (extract_labels_from_term term) results.labels
- })
- results terms
| AAllocation (_,FreeAllocAny) -> results
| AAllocation (_,FreeAlloc(f,a)) ->
let get_zone results x =
@@ -571,7 +562,7 @@ let code_annot_filter annot ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop
| AInvariant(_,false,_) -> others
| AAllocation _ -> others
| AAssigns _ -> others
- | APragma (Loop_pragma _)| APragma (Impact_pragma _) -> 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 8cb7318ad07..af831a23c67 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1735,10 +1735,6 @@ and behavior = {
(** extensions *)
}
-(** Pragmas for the value analysis plugin of Frama-C. *)
-and loop_pragma =
- | Unroll_specs of term list
-
(** Pragmas for the slicing plugin of Frama-C. *)
and slice_pragma =
| SPexpr of term
@@ -1752,7 +1748,6 @@ and impact_pragma =
(** The various kinds of pragmas. *)
and pragma =
- | Loop_pragma of loop_pragma
| Slice_pragma of slice_pragma
| Impact_pragma of impact_pragma
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 31b287429f8..cf4e8133a87 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3163,11 +3163,6 @@ class cil_printer () = object (self)
(pp_list nl_complete self#complete_behaviors) complete
(pp_list false self#disjoint_behaviors) disjoint
- method private loop_pragma fmt = function
- | Unroll_specs terms ->
- fprintf fmt "UNROLL @[%a@]"
- (Pretty_utils.pp_list ~sep:",@ " self#term) terms
-
method private slice_pragma fmt = function
|SPexpr t -> fprintf fmt "expr @[%a@]" self#term t
| SPctrl -> Format.pp_print_string fmt "ctrl"
@@ -3201,10 +3196,6 @@ class cil_printer () = object (self)
fprintf fmt "@[%a@ %a;@]"
self#pp_acsl_keyword "impact pragma"
self#impact_pragma sp
- | APragma (Loop_pragma lp) ->
- fprintf fmt "@[%a@ %a;@]"
- self#pp_acsl_keyword "loop pragma"
- self#loop_pragma lp
| 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 ed13828430d..a452c07e658 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -929,10 +929,6 @@ and pp_termination_kind fmt = function
| Continues -> Format.fprintf fmt "Continues"
| Returns -> Format.fprintf fmt "Returns"
-and pp_loop_pragma fmt = function
- | Unroll_specs(term_list) ->
- Format.fprintf fmt "Unroll_specs(%a)" (pp_list pp_term) term_list
-
and pp_slice_pragma fmt = function
| SPexpr(term) -> Format.fprintf fmt "SPexpr(%a)" pp_term term
| SPctrl -> Format.fprintf fmt "SPctrl"
@@ -943,8 +939,6 @@ and pp_impact_pragma fmt = function
| IPstmt -> Format.fprintf fmt "IPstmt"
and pp_pragma fmt = function
- | Loop_pragma(term) ->
- Format.fprintf fmt "Loop_pragma(%a)" pp_loop_pragma term
| Slice_pragma(term) ->
Format.fprintf fmt "Slice_pragma(%a)" pp_slice_pragma term
| Impact_pragma(term) ->
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index e9d3c6fb74a..3a0fbb3d918 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -140,8 +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_loop_pragma :
- Format.formatter -> Cil_types.loop_pragma -> unit
val pp_slice_pragma :
Format.formatter -> Cil_types.slice_pragma -> unit
val pp_impact_pragma :
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index f0aeef687ba..17808d4c970 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -450,10 +450,6 @@ let print_spec fmt spec =
~sep:"@\n" ~suf:"@\n" (pp_list ~sep:",@ " pp_print_string))
spec.spec_disjoint_behaviors
-let print_loop_pragma fmt p =
- match p with
- Unroll_specs l -> fprintf fmt "UNROLL@ %a" (pp_list ~sep:",@ " print_lexpr) l
-
let print_slice_pragma fmt p =
match p with
| SPexpr e -> fprintf fmt "expr@ %a" print_lexpr e
@@ -467,7 +463,6 @@ let print_impact_pragma fmt p =
let print_pragma fmt p =
match p with
- Loop_pragma p -> fprintf fmt "loop@ pragma@ %a;" print_loop_pragma p
| Slice_pragma p -> fprintf fmt "slice@ pragma@ %a;" print_slice_pragma p
| Impact_pragma p -> fprintf fmt "impact@ pragma@ %a;" print_impact_pragma p
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 35206eb8bd5..d5d4be2b0de 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -700,10 +700,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_loop_pragma p p' env =
- match p, p' with
- | 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
| SPexpr t, SPexpr t' -> is_same_term t t' env
@@ -719,10 +715,9 @@ and is_same_impact_pragma p p' env =
and is_same_pragma p p' env =
match p,p' with
- | Loop_pragma p, Loop_pragma p' -> is_same_loop_pragma p p' env
| 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
- | (Loop_pragma _ | Slice_pragma _ | Impact_pragma _), _ -> false
+ | (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 e287cf0048d..8b564568953 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1016,8 +1016,6 @@ class type cilVisitor = object
method vallocation:
allocation -> allocation visitAction
- method vloop_pragma: loop_pragma -> loop_pragma visitAction
-
method vslice_pragma: slice_pragma -> slice_pragma visitAction
method vimpact_pragma: impact_pragma -> impact_pragma visitAction
@@ -1153,8 +1151,6 @@ class internal_genericCilVisitor current_func behavior queue: cilVisitor =
method vallocates _s = DoChildren
method vallocation _s = DoChildren
- method vloop_pragma _ = DoChildren
-
method vslice_pragma _ = DoChildren
method vimpact_pragma _ = DoChildren
@@ -2041,15 +2037,6 @@ 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 visitCilLoopPragma vis p =
- doVisitCil vis
- id vis#vloop_pragma childrenLoopPragma p
-
-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
-
and childrenModelInfo vis m =
let field_type = visitCilLogicType vis m.mi_field_type in
let base_type = visitCilType vis m.mi_base_type in
@@ -2168,9 +2155,6 @@ and childrenCodeAnnot vis ca =
| APragma (Slice_pragma t) ->
let t' = visitCilSlicePragma vis t in
if t' != t then change_content (APragma (Slice_pragma t')) else ca
- | APragma (Loop_pragma p) ->
- let p' = visitCilLoopPragma vis p in
- if p' != p then change_content (APragma (Loop_pragma p')) 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 ca938f4a42d..c0e5ba3f954 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2013,7 +2013,6 @@ class type cilVisitor = object
method vallocation: allocation -> allocation visitAction
(** @since Oxygen-20120901 *)
- method vloop_pragma: loop_pragma -> loop_pragma visitAction
method vslice_pragma: slice_pragma -> slice_pragma visitAction
method vimpact_pragma: impact_pragma -> impact_pragma visitAction
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 9c5eddcfe4c..1ad0b7ba8fa 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3632,10 +3632,6 @@ struct
let plain_logic_type loc env t = logic_type (base_ctxt env) loc env t
- let loop_pragma env p =
- match p with
- | Unroll_specs l -> Cil_types.Unroll_specs (List.map (term env) l)
-
let model_annot loc ti =
let env = Lenv.empty() in
let model_for_type =
@@ -3870,9 +3866,6 @@ struct
| APragma (Slice_pragma sp) ->
Cil_types.APragma
(Cil_types.Slice_pragma (slice_pragma (code_annot_env()) sp))
- | APragma (Loop_pragma lp) ->
- Cil_types.APragma
- (Cil_types.Loop_pragma (loop_pragma (code_annot_env()) lp))
| 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 6846b6e7114..06e5268adf3 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -731,7 +731,7 @@ let is_annot_next_stmt c =
| AAssigns _ | AAllocation _
| APragma (Slice_pragma (SPctrl | SPexpr _))
| APragma (Impact_pragma (IPexpr _))
- | APragma (Loop_pragma _) -> false
+ -> false
let rec add_attribute_glob_annot a g =
match g with
@@ -1176,10 +1176,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_loop_pragma p1 p2 =
- match p1,p2 with
- Unroll_specs l1, Unroll_specs l2 -> is_same_list is_same_term l1 l2
-
let is_same_slice_pragma p1 p2 =
match p1,p2 with
SPexpr t1, SPexpr t2 -> is_same_term t1 t2
@@ -1194,10 +1190,9 @@ let is_same_impact_pragma p1 p2 =
let is_same_pragma p1 p2 =
match p1,p2 with
- | Loop_pragma p1, Loop_pragma p2 -> is_same_loop_pragma p1 p2
| Slice_pragma p1, Slice_pragma p2 -> is_same_slice_pragma p1 p2
| Impact_pragma p1, Impact_pragma p2 -> is_same_impact_pragma p1 p2
- | (Loop_pragma _ | Slice_pragma _ | Impact_pragma _), _ -> false
+ | (Slice_pragma _ | Impact_pragma _), _ -> false
let rec is_same_extension x1 x2 =
Datatype.String.equal x1.ext_name x2.ext_name &&
@@ -2275,9 +2270,6 @@ let is_assigns ca =
let is_pragma ca =
match ca.annot_content with APragma _ -> true | _ -> false
-let is_loop_pragma ca =
- match ca.annot_content with APragma (Loop_pragma _) -> true | _ -> false
-
let is_slice_pragma ca =
match ca.annot_content with APragma (Slice_pragma _) -> true | _ -> false
@@ -2289,7 +2281,7 @@ let is_loop_extension ca =
let is_loop_annot s =
is_loop_invariant s || is_assigns s || is_allocation s ||
- is_variant s || is_loop_pragma s || is_loop_extension s
+ is_variant s || is_loop_extension s
let is_trivial_annotation a =
match a.annot_content with
@@ -2299,18 +2291,11 @@ let is_trivial_annotation a =
-> false
let is_property_pragma = function
- | 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,
update the pragma-related code in gui/property_navigator.ml *)
-
-let extract_loop_pragma l =
- List.fold_right
- (fun ca l -> match ca.annot_content with
- APragma (Loop_pragma lp) -> lp::l | _ -> l) l []
-
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 f17f5537f1b..e59cab55aae 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -373,7 +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_loop_pragma : loop_pragma -> loop_pragma -> 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
@@ -460,7 +459,6 @@ 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_loop_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
@@ -470,8 +468,6 @@ val is_trivial_annotation : code_annotation -> bool
val is_property_pragma : pragma -> bool
(** Should this pragma be proved by plugins *)
-val extract_loop_pragma :
- code_annotation list -> loop_pragma list
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 d123c416326..ce029977c03 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -321,10 +321,6 @@ type spec = {
(** Pragmas for the value analysis plugin of Frama-C. *)
-type loop_pragma =
- | Unroll_specs of lexpr list
-
-(** Pragmas for the slicing plugin of Frama-C. *)
and slice_pragma =
| SPexpr of lexpr
| SPctrl
@@ -337,7 +333,6 @@ and impact_pragma =
(** The various kinds of pragmas. *)
and pragma =
- | Loop_pragma of loop_pragma
| Slice_pragma of slice_pragma
| Impact_pragma of impact_pragma
diff --git a/src/plugins/metrics/metrics_pivot.ml b/src/plugins/metrics/metrics_pivot.ml
index 62f57e9b0f6..4a291642b00 100644
--- a/src/plugins/metrics/metrics_pivot.ml
+++ b/src/plugins/metrics/metrics_pivot.ml
@@ -390,7 +390,6 @@ class full_visitor = object(self)
method! vfrees _ = Cil.DoChildren
method! vallocates _ = Cil.DoChildren
method! vallocation _ = Cil.DoChildren
- method! vloop_pragma _ = Cil.DoChildren
method! vslice_pragma _ = Cil.DoChildren
method! vimpact_pragma _ = Cil.DoChildren
method! vdeps _ = Cil.DoChildren
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index b7e821e4906..191ed903731 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -70,7 +70,7 @@ struct
let t_loop_assigns = t_loop "assigns"
let t_loop_variant = t_loop "variant"
let t_loop_allocates = t_loop "allocates"
- let t_loop_pragma = t_loop "pragma"
+ 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 +119,7 @@ struct
| AVariant _ -> t_loop_variant
| AAssigns _ -> t_loop_assigns
| AAllocation _ -> t_loop_allocates
- | APragma _ -> t_loop_pragma
+ | APragma _ -> t_pragma
| AExtended(_,_,{ext_name=_}) -> t_ext
end
| IPAllocation _ -> t_allocates
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 1771bbd362d..4f33131c032 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -649,7 +649,6 @@ let cfun_code env kf = (* Visits term/pred of code annotations and C exp *)
method !vpredicate p = do_pred p ; Cil.SkipChildren
method !vterm t = do_term t ; Cil.SkipChildren
(* speed up: skip non interesting subtrees *)
- method! vloop_pragma _ = Cil.SkipChildren (* no need *)
method! vvdec _ = Cil.SkipChildren (* done via stmt *)
method! vexpr _ = Cil.SkipChildren (* done via stmt *)
method! vlval _ = Cil.SkipChildren (* done via stmt *)
diff --git a/src/plugins/wp/RegionAccess.ml b/src/plugins/wp/RegionAccess.ml
index 4d1da962951..e79b487cdd3 100644
--- a/src/plugins/wp/RegionAccess.ml
+++ b/src/plugins/wp/RegionAccess.ml
@@ -392,7 +392,6 @@ class visitor map =
(* vpredicate and vterm are called from vcode_annot *)
(* speed up: skip non interesting subtrees *)
- method! vloop_pragma _ = Cil.SkipChildren (* no need *)
method! vvdec _ = Cil.SkipChildren (* done via stmt *)
method! vexpr _ = Cil.SkipChildren (* done via stmt *)
method! vlval _ = Cil.SkipChildren (* done via stmt *)
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index 8c968ef9650..71c4ebf29a7 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -59,11 +59,6 @@ let node () =
(* --- Unrolled Loop --- *)
(* -------------------------------------------------------------------------- *)
-let is_unrolled_completely spec =
- match spec.term_node with
- | TConst (LStr "completely") -> true
- | _ -> false
-
let rec is_predicate cond p =
match p.pred_content with
| Pfalse -> not cond
@@ -88,8 +83,6 @@ let rec is_predicate cond p =
let is_dead_annot ca =
match ca.annot_content with
- | APragma (Loop_pragma (Unroll_specs [ spec ; _ ])) ->
- is_unrolled_completely spec
| AAssert([],p)
| AInvariant([],_,p) ->
Logic_utils.use_predicate p.tp_kind && is_predicate false p.tp_statement
--
GitLab