diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 98b6fab58ce1955d19dcccb283aefa15013c40a9..ab8aea9acf16656c6ce84c8cb09682526a4c4f6b 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -36,37 +36,30 @@ let set_extension_handler ~print =
initialized_extensions := true ;
()
-module Behavior_extensions = struct
-
- let printer_tbl = Hashtbl.create 5
-
- let register name printer =
- Hashtbl.add printer_tbl name printer
+let ref_deprecated_extension_handler = ref (fun _ _ _ -> assert false)
+let set_deprecated_extension_handler ~handler =
+ ref_deprecated_extension_handler := handler
- let default_pp printer fmt ext =
- match ext with
- | Ext_id i -> Format.pp_print_int fmt i
- | Ext_terms terms ->
- Pretty_utils.pp_list ~sep:",@ " printer#term fmt terms
- | Ext_preds preds ->
- Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt preds
+module Behavior_extensions = struct
+ let deprecated_register name =
+ !ref_deprecated_extension_handler name
let pp (printer) fmt {ext_name; ext_kind} =
- let pp =
- try
- Hashtbl.find printer_tbl ext_name
- with Not_found -> default_pp
- in
+ let pp = !ref_print_extension ext_name in
Format.fprintf fmt "@[<hov 2>%s %a;@]" ext_name (pp printer) ext_kind
end
-let register_behavior_extension = Behavior_extensions.register
+let register_behavior_extension name =
+ Behavior_extensions.deprecated_register name Ext_contract
-let register_code_annot_extension = Behavior_extensions.register
+let register_code_annot_extension name =
+ Behavior_extensions.deprecated_register name (Ext_code_annot Ext_here)
-let register_loop_annot_extension = Behavior_extensions.register
+let register_loop_annot_extension name =
+ Behavior_extensions.deprecated_register name (Ext_code_annot Ext_next_loop)
-let register_global_extension = Behavior_extensions.register
+let register_global_extension name =
+ Behavior_extensions.deprecated_register name Ext_global
(* Internal attributes. Won't be pretty-printed *)
let reserved_attributes = ref []
diff --git a/src/kernel_services/ast_printing/cil_printer.mli b/src/kernel_services/ast_printing/cil_printer.mli
index 04e4206ae373e21068b9c5668a19b3b1e35cf37c..3c7260976c27f9451335904d3dad188469fe58b9 100644
--- a/src/kernel_services/ast_printing/cil_printer.mli
+++ b/src/kernel_services/ast_printing/cil_printer.mli
@@ -41,31 +41,39 @@ val register_behavior_extension:
Cil_types.acsl_extension_kind -> unit) -> unit
(** Register a pretty-printer used for behavior extension.
@plugin development guide
+ @deprecated Frama-C+dev
*)
+[@@ deprecated "Use Acsl_extension.register_behavior 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 behavior extension.
+(** Register a pretty-printer used for global extension.
@plugin development guide
+ @deprecated Frama-C+dev
*)
+[@@ deprecated "Use Acsl_extension.register_global 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 behavior extension.
+(** Register a pretty-printer used for code annotation extension.
@plugin development guide
+ @deprecated Frama-C+dev
*)
+[@@ deprecated "Use Acsl_extension.register_code_annot_<kind> 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 behavior extension.
+(** Register a pretty-printer used for loop annotation extension.
@plugin development guide
+ @deprecated Frama-C+dev
*)
+[@@ deprecated "Use Acsl_extension.register_loop_annot instead"]
val state: Printer_api.state
@@ -84,6 +92,12 @@ val set_extension_handler:
@since Frama-C+dev
*)
+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 f59ee45bf2ffff79fc074cb3b48b8c8d7c7227a9..6bc7422068481c991e275cf5c138e21ea267edeb 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -117,3 +117,48 @@ let () =
~visit: Extensions.visit ;
Cil_printer.set_extension_handler
~print: Extensions.print
+
+(* For Deprecation: *)
+
+let deprecated_replace name ext = Hashtbl.add Extensions.ext_tbl name ext
+
+let strong_cat = Hashtbl.create 5
+
+let deprecated_find ?(strong=true) name cat op_name =
+ match Hashtbl.find_opt Extensions.ext_tbl name with
+ | None ->
+ if strong then Hashtbl.add strong_cat name cat ;
+ (cat, default)
+ | Some (found_cat, ext) ->
+ if strong && Hashtbl.mem strong_cat name then begin
+ if found_cat = cat then (cat, ext)
+ 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 ;
+ (cat, ext)
+ end else
+ (found_cat, ext)
+
+let deprecated_register_typing name cat ext_status ext_typing =
+ let cat, ext = deprecated_find name cat "typing" in
+ let ext = { ext with ext_status ; ext_typing } in
+ deprecated_replace name (cat, ext)
+
+let deprecated_register_printing name cat ext_printing =
+ let cat, ext = deprecated_find ~strong:false name cat "printing" in
+ let ext = { ext with ext_printing } in
+ deprecated_replace name (cat, ext)
+
+let deprecated_register_visit name cat ext_visit =
+ let cat, ext = deprecated_find name cat "visit" in
+ let ext = { ext with ext_visit } in
+ deprecated_replace name (cat, ext)
+
+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 d17d73e3598e21292f648b5dded85be2158cc58f..dc24efcd495cb444fdc92fef5ca0e95121cdb7c9 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -755,8 +755,6 @@ let alphabetabeta _ x = x
let alphabetafalse _ _ = false
let alphatrue _ = true
-let visitor_tbl = Hashtbl.create 5
-
let initialized_extensions = ref false
let ref_visit_extension = ref (fun _ _ _ -> assert false)
@@ -766,7 +764,12 @@ let set_extension_handler ~visit =
initialized_extensions := true ;
()
-let register_behavior_extension name ext = Hashtbl.add visitor_tbl name ext
+let ref_deprecated_extension_handler = ref (fun _ _ _ -> assert false)
+let set_deprecated_extension_handler ~handler =
+ ref_deprecated_extension_handler := handler
+
+let register_behavior_extension name ext =
+ !ref_deprecated_extension_handler name Ext_contract ext
(* sm/gn: cil visitor interface for traversing Cil trees. *)
(* Use visitCilStmt and/or visitCilFile to use this. *)
@@ -1898,10 +1901,7 @@ and childrenBehavior vis b =
b
and visitCilExtended vis orig =
- let visit =
- try Hashtbl.find visitor_tbl orig.ext_name
- with Not_found -> (fun _ _ -> DoChildren)
- in
+ let visit = !ref_visit_extension orig.ext_name in
let e' = doVisitCil vis id (visit vis) childrenCilExtended orig.ext_kind in
if Visitor_behavior.is_fresh vis#behavior then
Logic_const.new_acsl_extension orig.ext_name orig.ext_loc
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 61d314736e209f61c78a373b35d0cb16518fba85..186a826e2423daa1ce8ef18b968491b4dae8c184 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1725,11 +1725,13 @@ end
@since Sodium-20150201
@modify Silicon-20161101
+ @deprecated Frama-C+dev
*)
val register_behavior_extension:
string ->
(cilVisitor -> acsl_extension_kind -> (acsl_extension_kind) visitAction)
-> unit
+[@@ deprecated "Use Acsl_extension.register_behavior instead"]
(**/**)
class internal_genericCilVisitor:
@@ -2292,6 +2294,11 @@ val set_extension_handler:
@since Frama-C+dev
*)
+val set_deprecated_extension_handler:
+ handler:(string -> ext_category ->
+ (cilVisitor -> acsl_extension_kind -> acsl_extension_kind visitAction) ->
+ unit) -> unit
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index 341ab6de574c2ce265ae27ad0967dabb87b8df99..0d7f4da3712940fb262d82ad35515c231c347978 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -35,16 +35,8 @@ let set_extension_handler ~category ~is_extension =
initialized_extensions := true ;
()
-
-let extensions = ref Datatype.String.Map.empty
-
-let is_extension s = Datatype.String.Map.mem s !extensions
-
-let extension_category s = Datatype.String.Map.find_opt s !extensions
-
-let register_extension s cat =
- if not (is_extension s) then
- extensions := Datatype.String.Map.add s cat !extensions
+let is_extension s = !ref_is_extension s
+let extension_category s = !ref_extension_category s
module CurrentLoc = Cil_const.CurrentLoc
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index 2207c731d99d57431e2bd4288bdb245e71f658e1..bc9cf490523ad561e48afac0e2a35cd43645119d 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -28,9 +28,6 @@ open Cil_types
(** {2 registered ACSL extensions } *)
-(** register a given name as a clause name for extended category. *)
-val register_extension: string -> ext_category -> unit
-
val is_extension: string -> bool
val extension_category: string -> ext_category option
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 586294e2a0d73ae0a4c62d8198be4fab76fea915..57775843694f86152917c9b86cc5bf81c8882a66 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -535,33 +535,25 @@ let set_extension_handler ~is_extension ~typer =
initialized_extensions := true ;
()
+let ref_deprecated_extension_handler = ref (fun _ _ _ _ -> assert false)
+let set_deprecated_extension_handler ~handler =
+ ref_deprecated_extension_handler := handler
+
module Extensions = struct
- let typer_tbl = Hashtbl.create 5
- let find_typer name = Hashtbl.find typer_tbl name
- let is_extension name = Hashtbl.mem typer_tbl name
- let register name category status typer =
- if is_extension name then
- Kernel.warning ~wkey:Kernel.wkey_acsl_extension
- "Trying to register ACSL extension %s twice. Ignoring second extension"
- name
- else begin
- Logic_env.register_extension name category;
- Hashtbl.add typer_tbl name (status,typer)
- end
+ let is_extension name = !ref_is_extension name
+
+ let deprecated_register name category status typer =
+ let typer typing_context loc = typer ~typing_context ~loc in
+ !ref_deprecated_extension_handler name category status typer
let typer name ~typing_context:typing_context ~loc p =
- let status,typer =
- try find_typer name
- with Not_found ->
- Kernel.fatal ~source:(fst loc) "unsupported clause of name '%s'" name
- in
+ let typer = !ref_type_extension name in
let normal_error = ref false in
let has_error () = normal_error := true in
let wrapper =
- typing_context.on_error (typer ~typing_context ~loc) has_error
+ typing_context.on_error (typer typing_context loc) has_error
in
- try
- status, wrapper p
+ try wrapper p
with
| (Log.AbortError _ | Log.AbortFatal _) as exn -> raise exn
| exn when not !normal_error ->
@@ -570,22 +562,22 @@ module Extensions = struct
end
let register_behavior_extension name f =
- Extensions.register name Ext_contract f
+ Extensions.deprecated_register name Ext_contract f
let register_global_extension name f =
- Extensions.register name Ext_global f
+ Extensions.deprecated_register name Ext_global f
let register_code_annot_extension name f =
- Extensions.register name (Ext_code_annot Ext_here) f
+ Extensions.deprecated_register name (Ext_code_annot Ext_here) f
let register_code_annot_next_stmt_extension name f =
- Extensions.register name (Ext_code_annot Ext_next_stmt) f
+ Extensions.deprecated_register name (Ext_code_annot Ext_next_stmt) f
let register_code_annot_next_loop_extension name f =
- Extensions.register name (Ext_code_annot Ext_next_loop) f
+ Extensions.deprecated_register name (Ext_code_annot Ext_next_loop) f
let register_code_annot_next_both_extension name f =
- Extensions.register name (Ext_code_annot Ext_next_both) 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
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 5d6bb73f7ff2eeded39bcf4c86e8050985d15757..f46cc6b0da8a7359476759a6da55db466fb963a7 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -177,22 +177,26 @@ type typing_context = {
@since Carbon-20101201
@modify Silicon-20161101 change type of the function
@modify 19.0-Potassium add [status] argument
+ @deprecated Frama-C+dev
*)
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 Frama-C+dev
*)
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.
@@ -200,11 +204,13 @@ val register_global_extension:
@plugin development guide
@since 18.0-Argon
+ @deprecated Frama-C+dev
*)
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.
@@ -212,22 +218,26 @@ val register_code_annot_extension:
@plugin development guide
@since 18.0-Argon
+ @deprecated Frama-C+dev
*)
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 Frama-C+dev
*)
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.
@@ -235,11 +245,13 @@ val register_code_annot_next_loop_extension:
@plugin development guide
@since 18.0-Argon
+ @deprecated Frama-C+dev
*)
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 :
@@ -383,6 +395,14 @@ val set_extension_handler:
@since Frama-C+dev
*)
+(**/**)
+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 ../../.."