diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index a4ee7f3882e02ae8cf6d4ea3038de785fcbf24eb..eb920a51c908ceb0db8dc38638bc32db2d169db3 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1675,13 +1675,8 @@ and spec = {
Each extension is associated with a keyword, and can be either a global
annotation, the clause of a function contract, a code annotation,
or a loop annotation.
- An extension can be registered through the following functions:
- - [Logic_typing.register_xxx_extension] for parsing and type-checking
- - [Cil_printer.register_xxx_extension] for pretty-printing an
- extended clause
- - [Cil.register_xxx_extension] for visiting an extended clause
- where xxx can be either [global], [behavior], [code_annot] or
- [loop annot] depending on the level at which the extension should be seen.
+ An extension can be registered through the function
+ [Acsl_extension.register_xxx].
It is _not_ possible to register the same keyword for annotations at two
different levels (e.g. [global] and [behavior]), as this would make the
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 951787b536a0f476d6946932eab7f175cad825d6..10e359d4b91f4b15b4365918dc2ad4b1a54a86c9 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -92,12 +92,6 @@ module Extensions = struct
let pp_short (printer) fmt {ext_name; ext_kind} =
!ref_short_print ext_name printer fmt ext_kind
- let ref_deprecated_handler = ref (fun _ _ _ -> assert false)
- let set_deprecated_handler ~handler =
- ref_deprecated_handler := handler
-
- let deprecated_register name =
- !ref_deprecated_handler name
end
let set_extension_handler = Extensions.set_handler
@@ -115,21 +109,6 @@ let () =
"__fc_sig_err", "SIG_ERR";
]
-(* Deprecated functions *)
-let set_deprecated_extension_handler = Extensions.set_deprecated_handler
-
-let register_behavior_extension name =
- Extensions.deprecated_register name Ext_contract
-
-let register_code_annot_extension name =
- Extensions.deprecated_register name (Ext_code_annot Ext_here)
-
-let register_loop_annot_extension name =
- Extensions.deprecated_register name (Ext_code_annot Ext_next_loop)
-
-let register_global_extension name =
- Extensions.deprecated_register name Ext_global
-
(* Internal attributes. Won't be pretty-printed *)
let reserved_attributes = ref []
let register_shallow_attribute s =
diff --git a/src/kernel_services/ast_printing/cil_printer.mli b/src/kernel_services/ast_printing/cil_printer.mli
index 7e0b5fd02905c3441575f96375a3d1be1574db85..cb6802b1bf576b4ec49d4b609898ae2dd03b71f9 100644
--- a/src/kernel_services/ast_printing/cil_printer.mli
+++ b/src/kernel_services/ast_printing/cil_printer.mli
@@ -63,46 +63,6 @@ val get_termination_kind_name: Cil_types.termination_kind -> string
val register_shallow_attribute: string -> unit
(** Register an attribute that will never be pretty printed. *)
-val register_behavior_extension:
- string ->
- (Printer_api.extensible_printer_type -> Format.formatter ->
- Cil_types.acsl_extension_kind -> unit) -> unit
-(** Register a pretty-printer used for behavior extension.
- @plugin development guide
- @deprecated 21.0-Scandium
-*)
-[@@ deprecated "Use Acsl_extension.register_behavior (arg: ~printer) instead"]
-
-val register_global_extension:
- string ->
- (Printer_api.extensible_printer_type -> Format.formatter ->
- Cil_types.acsl_extension_kind -> unit) -> unit
-(** Register a pretty-printer used for global extension.
- @plugin development guide
- @deprecated 21.0-Scandium
-*)
-[@@ deprecated "Use Acsl_extension.register_global (arg: ~printer) instead"]
-
-val register_code_annot_extension:
- string ->
- (Printer_api.extensible_printer_type -> Format.formatter ->
- Cil_types.acsl_extension_kind -> unit) -> unit
-(** Register a pretty-printer used for code annotation extension.
- @plugin development guide
- @deprecated 21.0-Scandium
-*)
-[@@ deprecated "Use Acsl_extension.register_code_annot_<kind> (arg: ~printer) instead"]
-
-val register_loop_annot_extension:
- string ->
- (Printer_api.extensible_printer_type -> Format.formatter ->
- Cil_types.acsl_extension_kind -> unit) -> unit
-(** Register a pretty-printer used for loop annotation extension.
- @plugin development guide
- @deprecated 21.0-Scandium
-*)
-[@@ deprecated "Use Acsl_extension.register_loop_annot (arg: ~printer) instead"]
-
val state: Printer_api.state
val print_global: Cil_types.global -> bool
@@ -122,12 +82,6 @@ val set_extension_handler:
@since 21.0-Scandium
*)
-val set_deprecated_extension_handler:
- handler:(string -> Cil_types.ext_category ->
- (Printer_api.extensible_printer_type -> Format.formatter ->
- Cil_types.acsl_extension_kind -> unit) ->
- unit) -> unit
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 450fd797e13a085e92cdf1469e8d89f14705fd2e..7445dddc90a485832dd140ab261abfcbebba5f02 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -53,15 +53,6 @@ type extension_common = {
printer: extension_printer ;
short_printer: extension_printer ;
}
-type extension = {
- preprocessor: extension_preprocessor ;
- typer: extension_typer ;
- status: bool ;
- category: ext_category ;
- visitor: extension_visitor ;
- printer: extension_printer ;
- short_printer: extension_printer ;
-}
let default_printer printer fmt = function
| Ext_id i -> Format.fprintf fmt "%d" i
@@ -238,72 +229,3 @@ let () =
Cil_printer.set_extension_handler
~print: Extensions.print
~short_print:Extensions.short_print
-
-(* For Deprecation: *)
-
-let deprecated_replace name ext =
- let info1:extension_single = {
- preprocessor = ext.preprocessor ;
- typer = ext.typer ;
- status = ext.status ;
- }
- in
- let info2:extension_common = {
- category = ext.category ;
- visitor = ext.visitor ;
- printer = ext.printer ;
- short_printer = ext.printer ;
- }
- in
- Hashtbl.add Extensions.ext_single_tbl name info1;
- Hashtbl.add Extensions.ext_tbl name info2
-
-let strong_cat = Hashtbl.create 5
-
-let default_typer _typing_context _loc _l = assert false
-
-let merge ((info1:extension_single),(info2:extension_common)) :extension =
- {preprocessor = info1.preprocessor ;
- typer = info1.typer ;
- status = info1.status ;
- category = info2.category ;
- visitor = info2.visitor ;
- printer = info2.printer ;
- short_printer = info2.printer}
-
-let deprecated_find ?(strong=true) name cat op_name =
- match Hashtbl.find_opt Extensions.ext_single_tbl name with
- | None ->
- if strong then Hashtbl.add strong_cat name cat ;
- merge (make name cat default_typer false)
- | Some ext1 ->
- let ext2 = Extensions.find_common name in
- if strong && Hashtbl.mem strong_cat name then begin
- if ext2.category = cat then merge (ext1,ext2)
- else
- Kernel.fatal
- "Registring %s for %s: this extension already exists for another \
- category"
- op_name name
- end else if strong then begin
- Hashtbl.add strong_cat name cat ;
- let ext2 = { ext2 with category = cat } in
- merge (ext1,ext2)
- end else merge (ext1,ext2)
-
-let deprecated_register_typing name cat status typer =
- deprecated_replace name
- { (deprecated_find name cat "typing") with status ; typer }
-
-let deprecated_register_printing name cat printer =
- deprecated_replace name
- { (deprecated_find ~strong:false name cat "printing") with printer }
-
-let deprecated_register_visit name cat visitor =
- deprecated_replace name
- { (deprecated_find name cat "visit") with visitor }
-
-let () =
- Logic_typing.set_deprecated_extension_handler deprecated_register_typing ;
- Cil.set_deprecated_extension_handler deprecated_register_visit ;
- Cil_printer.set_deprecated_extension_handler deprecated_register_printing
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 9989a671d839911fefad80bd78d5184f41161a6e..c566dfb1b33c36ce1285de910e2ce710ff1d6775 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -837,20 +837,9 @@ module Extensions = struct
let visit name = !ref_visit name
- let ref_deprecated_handler = ref (fun _ _ _ -> assert false)
- let set_deprecated_handler ~handler =
- ref_deprecated_handler := handler
-
- let register_behavior name ext =
- !ref_deprecated_handler name Ext_contract ext
end
let set_extension_handler = Extensions.set_handler
-(* Deprecated *)
-let set_deprecated_extension_handler = Extensions.set_deprecated_handler
-let register_behavior_extension = Extensions.register_behavior
-
-
(* sm/gn: cil visitor interface for traversing Cil trees. *)
(* Use visitCilStmt and/or visitCilFile to use this. *)
(* Some of the nodes are changed in place if the children are changed. Use
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index df4e0e12389593b8b0423c1bf6d46e91dd878bc5..02f54e2f020e25934ad25cddffb08a467da39b65 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1789,22 +1789,6 @@ class type cilVisitor = object
end
-(** Indicates how an extended behavior clause is supposed to be visited.
- The default behavior is [DoChildren], which ends up visiting
- each identified predicate in the list and leave the id as is.
-
- @plugin development guide
-
- @since Sodium-20150201
- @modify Silicon-20161101
- @deprecated 21.0-Scandium
-*)
-val register_behavior_extension:
- string ->
- (cilVisitor -> acsl_extension_kind -> (acsl_extension_kind) visitAction)
- -> unit
-[@@ deprecated "Use Acsl_extension.register_behavior instead (arg: ~visitor)"]
-
(**/**)
class internal_genericCilVisitor:
fundec option ref -> Visitor_behavior.t -> (unit->unit) Queue.t -> cilVisitor
@@ -2378,11 +2362,6 @@ val set_extension_handler:
@since 21.0-Scandium
*)
-val set_deprecated_extension_handler:
- handler:(string -> ext_category ->
- (cilVisitor -> acsl_extension_kind -> acsl_extension_kind visitAction) ->
- unit) -> unit
-
(* ***********************************************************************)
(** {2 Forward references} *)
(* ***********************************************************************)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 10e1c9714402301d3b9d452b19c3c6c9ab804a92..177bb48546c3d0fb3e8253674bd6c053cca8e62b 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -544,42 +544,11 @@ module Extensions = struct
let typer_block name ~typing_context:typing_context ~loc =
!ref_typer_block name typing_context loc
- (* For deprecated functions *)
- let ref_deprecated_handler = ref (fun _ _ _ _ -> assert false)
-
- let set_deprecated_handler ~handler =
- ref_deprecated_handler := handler
-
- let deprecated_register name category status typer =
- let typer typing_context loc = typer ~typing_context ~loc in
- !ref_deprecated_handler name category status typer
end
let set_extension_handler = Extensions.set_handler
let get_typer = Extensions.typer
let get_typer_block = Extensions.typer_block
-(* Deprecated ACSL extensions functions *)
-let set_deprecated_extension_handler =
- Extensions.set_deprecated_handler
-
-let register_behavior_extension name f =
- Extensions.deprecated_register name Ext_contract f
-
-let register_global_extension name f =
- Extensions.deprecated_register name Ext_global f
-
-let register_code_annot_extension name f =
- Extensions.deprecated_register name (Ext_code_annot Ext_here) f
-
-let register_code_annot_next_stmt_extension name f =
- Extensions.deprecated_register name (Ext_code_annot Ext_next_stmt) f
-
-let register_code_annot_next_loop_extension name f =
- Extensions.deprecated_register name (Ext_code_annot Ext_next_loop) f
-
-let register_code_annot_next_both_extension name f =
- Extensions.deprecated_register name (Ext_code_annot Ext_next_both) f
-
let rec arithmetic_conversion ty1 ty2 =
match unroll_type ty1, unroll_type ty2 with
| Ctype ty1, Ctype ty2 ->
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index bd1fe2010f104e110c4271ea1d0471d192db5817..9db60f4b059866436d82d192083d0e22c07fcb95 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -151,108 +151,6 @@ type typing_context = {
on_error: 'a 'b. ('a -> 'b) -> (unit -> unit) -> 'a -> 'b
}
-(** [register_behavior_extension name status f] registers a
- typing function [f] to
- be used to type function contract clause with name [name].
- The boolean flags specifies if the extension can be assigned
- a property status or not.
-
- Here is a basic example:
-
- let count = ref 0 in
- let foo_typer ~typing_context ~loc ps =
- match ps with p::[] ->
- Ext_preds
- [
- (typing_context.type_predicate
- typing_context
- (typing_context.post_state [Normal])
- p)])
- | [] -> let id = !count in incr count; Ext_id id
- | _ -> typing_context.error loc "expecting a predicate after keyword FOO"
- let () = register_behavior_extension "FOO" false foo_typer
-
- @plugin development guide
-
- @since Carbon-20101201
- @modify Silicon-20161101 change type of the function
- @modify 19.0-Potassium add [status] argument
- @deprecated 21.0-Scandium
-*)
-val register_behavior_extension:
- string -> bool ->
- (typing_context:typing_context -> loc:location ->
- Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
-[@@ deprecated "Use Acsl_extension.register_behavior instead"]
-
-(** register an extension for global annotation.
-
- @plugin development guide
-
- @since 18.0-Argon
- @deprecated 21.0-Scandium
-*)
-val register_global_extension:
- string -> bool ->
- (typing_context:typing_context -> loc: location ->
- Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
-[@@ deprecated "Use Acsl_extension.register_global instead"]
-
-(** register an extension for code annotation to be evaluated at _current_
- program point.
-
- @plugin development guide
-
- @since 18.0-Argon
- @deprecated 21.0-Scandium
-*)
-val register_code_annot_extension:
- string -> bool ->
- (typing_context: typing_context -> loc: location ->
- Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
-[@@ deprecated "Use Acsl_extension.register_code_annot instead"]
-
-(** register an extension for code annotation to be evaluated for the _next_
- statement.
-
- @plugin development guide
-
- @since 18.0-Argon
- @deprecated 21.0-Scandium
-*)
-val register_code_annot_next_stmt_extension:
- string -> bool ->
- (typing_context: typing_context -> loc: location ->
- Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
-[@@ deprecated "Use Acsl_extension.register_code_annot_next_stmt instead"]
-
-(** register an extension for loop annotation.
-
- @plugin development guide
-
- @since 18.0-Argon
- @deprecated 21.0-Scandium
-*)
-val register_code_annot_next_loop_extension:
- string -> bool ->
- (typing_context: typing_context -> loc: location ->
- Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
-[@@ deprecated "Use Acsl_extension.register_code_annot_next_loop instead"]
-
-
-(** register an extension both for code and loop annotations.
-
- @plugin development guide
-
- @since 18.0-Argon
- @deprecated 21.0-Scandium
-*)
-val register_code_annot_next_both_extension:
- string -> bool ->
- (typing_context: typing_context -> loc: location ->
- Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
-[@@ deprecated "Use Acsl_extension.register_code_annot_next_both instead"]
-
module Make
(C :
sig
@@ -412,14 +310,6 @@ val get_typer_block:
string * Logic_ptree.extended_decl list ->
bool * Cil_types.acsl_extension_kind
-(**/**)
-val set_deprecated_extension_handler:
- handler:(string -> ext_category -> bool ->
- (typing_context -> location -> Logic_ptree.lexpr list ->
- acsl_extension_kind) ->
- unit) ->
- unit
-
(*
Local Variables:
compile-command: "make -C ../../.."