diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 98c190c409a9d7f9a37b739deaed02aa8bb777a4..e233ab3d15bda459bbaddef8ba9011cf9c9d3c50 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 8317846aaa3afd18818c62b2c846b9d249e2b6e8..4bc7199b1bedb2b59684124bda7553ac9e29bffc 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 d7c54a7de7794c97971f49d2583fb3ab05846771..6a5bb2caf6c7c787a94beeb7079e78908c65524e 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 c514e9754880be110af5a5e4faf9d1d29bad1c64..6f805da8dae22ea573d8f57a5f9c0b26090a3741 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 c465ce14c607ea3426128ee2032e881d4eb7b0aa..57de8321c4952ae06bffd6e5fe65b7bca5b7f7fb 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 44e170a706037d3d1d0a4f36b195dba00521578a..db1b59e51d962777c8b56d9aee89a83b27ae068d 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 7a75b1ed306cc98e63572fdee317d35058f33196..e144f4363dab7a06b41b6e72937efaf958a754b0 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 4789db180f66dcdf1ec164bde8bea36fa34bbfa3..1e5f0f1fdd9386c51f91aed243da5b9cc0b87773 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 90d5044211b9ed9383c2cc9e4f3b3b10ad8402b0..2b86486b245ddf26f934aac34d84d1caad3beb60 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 c266a037d2392a55a120e127a180eefa254df78e..75c2da8a093025837852d9a46bbc43b64ae07202 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 cae80c9951b95a8fda14e2b35fe50044ddf2cfeb..12e2557c25673e2f412019ae8ad0207db1f2a6f4 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 b52279be3ea0efe4c119767779738e8565f8a088..dea0ff2b9283d65eb132df06a7186fcf4b01f9db 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 53d007c1f2dc87132ae953d738b5068e3faa4a0d..ab7ccf849a401267dd85d551593fafb5c2775f68 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 eb5658c92af7a9172b8a52b07dff898fbaf45760..aeba051d5cd8d428079a2888c9794c4bc94ddbf6 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 7c50dafb7adbc9f6fec297c626b63d1495ef7077..dd9d31dca5152467450b0a5f4459abb2946c960b 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 b849b8f00b613b59d8d9d04d9e29bbbeb10fde06..f23eb2643d9d177222152c0621f0b10dcc1f40fa 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 2b39631d71b32df4d594e5035b3030ba45652b24..9dc42b8d8cfa752ef4fa4d1e0c7d7cc3ce097da3 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 e784e97927873c23a5197e0aadf9bd62191b15d3..1b3ace6387f1f46102ea851ef3dc07653c483e40 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 c43820f0bec7a9e17da551b570c41126204c17fd..e54b77b2f41f90b065bff3bf11166ff3ae83879d 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 799e52d1780be8acb3b81c5e2cea92f2c4bf2abe..f11de6f809ec1404417c390aa3bfab294568466b 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 0c6abfa91eee04c1aebe5455b06b9903ffebdca2..855cce6149e5c8ddf39243b88212fb84162cc3d9 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 a537c6ab681949f36b0ae11f1cef72af5892d371..5b66f11b696ed3809673e9bd66235797a7df8f05 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 ace04011a2dc67ce13a2ef170d181997f385dd4b..2d75c19ccdfa05074319c0587459e1b23cdb4f82 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 c72b5dac60a9980ddfe4d7334a61846cbec4c125..4fbd3210b4737feca4e9ad1d7cfe8046d17a4fc4 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 48436fb22868c1a24bfba5278d52f8bc0b72bc52..9ef563d8833f901ce18594e055e4804f26f8a9ab 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 a5e76ba1bade2346f7cc1b954eef56b2c9a1df22..79b07e9374dd3a3be35a5aebec6f5efd0c58be1b 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 8674b84187cc5d586773767364663c238334b52a..343634fd4b6c6b6b8dcf53940a22de1b89ba2108 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 439c2dba354e069fc2c3b7dff100d048f7fee5c0..3f484c98307adf09c9b9432267a43fbe7166b3d6 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 41aa1bc0dcc998b4bc84eaf8866910479fe1784f..94a4ff04fdfe2b3cd26bcc6019db097056f0d09e 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 beff72440d8f151342f6500feb010aec0b244fea..e82b85b231c25a2deaac5c861805bbfe24b9efcf 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 1381ced216afa36c447485daceaa6e24e8c3af73..5592bd188cd1a9245116289196699706a367acfe 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 cd3bd66a369de8bca84eb87d54445bd10f180511..073fdad49b4425f2b10f5e98b44014da074d1f01 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 bceb343d9edbc9a7f2407c95a35334cb5d3587c2..11e68d855c32d780f93e60a3b152a23569527608 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 98cf1b9b3514e00447f62d03052cdd8d4ced82ac..5ff525c353c9baabd13989e9543ddd309b50fbb1 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 74349068d997ef140efa8e179dca5482a075810a..d78507281249ac7b058d68a30e9d969c4042e929 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 8d84bb2874a334504e69b69415ce4f252d27f479..c80c97892fae77886d3fa6410c586ee651e25b4c 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 a376b69751a7a4bf97bc360cc97ebdd77d59f7ca..b37fe42620e130d52acfe29fbad191e8e659be10 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 e063a84fe1583955ab8919ef691f2be0bbdc2f2a..ec6b9b0cf758c9241e9564daf8d9588654bcf6e3 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 bf683b0c97377bf8b756add8cfb2ea6fb62b72b1..f9c0980cbdcfa8621efb2a6a624a2d575c48d36a 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 e9a8931cb1a8a0383c4b994156c16b8b2e40a8e3..0d00f2dc2ef00c1d74def350ac92407f724c98a1 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