diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml index 913ea0e95b7ad73a536665bdc2cbb7c8bd442c61..f5c221bc25b35440e4ce852ccbddce486aaf7169 100644 --- a/src/kernel_services/ast_queries/acsl_extension.ml +++ b/src/kernel_services/ast_queries/acsl_extension.ml @@ -320,8 +320,6 @@ module Extensions = struct let is_same_ext ~plugin name ext1 ext2 = let is_same = (find_common ~plugin name).is_same_ext in is_same ext1 ext2 - - let extension_from name = (find_common ~plugin:None name).plugin end (* Registration functions *) @@ -351,8 +349,7 @@ let () = ~is_extension: Extensions.is_extension ~preprocess: Extensions.preprocess ~is_extension_block: Extensions.is_extension_block - ~preprocess_block: Extensions.preprocess_block - ~extension_from:Extensions.extension_from; + ~preprocess_block: Extensions.preprocess_block; Logic_typing.set_extension_handler ~is_extension: Extensions.is_extension ~typer: Extensions.typing diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml index 8dc8dae1196fd2980f03912adcc6d54e0fa493b1..0f46da80c6c6c039755525713315af574154d4c9 100644 --- a/src/kernel_services/ast_queries/logic_env.ml +++ b/src/kernel_services/ast_queries/logic_env.ml @@ -31,17 +31,15 @@ module Extensions = struct let ref_preprocess = ref (fun ~plugin:_ _ -> assert false) let ref_is_extension_block = ref (fun ~plugin:_ _ -> assert false) let ref_preprocess_block = ref (fun ~plugin:_ _ -> assert false) - let ref_extension_from = ref (fun _ -> assert false) let set_extension_handler ~category ~is_extension ~preprocess - ~is_extension_block ~preprocess_block ~extension_from = + ~is_extension_block ~preprocess_block = assert (not !initialized) ; ref_is_extension := is_extension ; ref_category := category ; ref_preprocess := preprocess ; ref_is_extension_block := is_extension_block; ref_preprocess_block := preprocess_block; - ref_extension_from := extension_from; initialized := true ; () @@ -50,7 +48,6 @@ module Extensions = struct let category ~plugin name = !ref_category ~plugin name let preprocess ~plugin name = !ref_preprocess ~plugin name let preprocess_block ~plugin name = !ref_preprocess_block ~plugin name - let extension_from name = !ref_extension_from name end let set_extension_handler = Extensions.set_extension_handler let is_extension = Extensions.is_extension @@ -58,7 +55,6 @@ let is_extension_block = Extensions.is_extension_block let extension_category = Extensions.category let preprocess_extension = Extensions.preprocess let preprocess_extension_block = Extensions.preprocess_block -let extension_from = Extensions.extension_from let error (b,_e) fstring = Kernel.abort diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli index c82bcbe2a23b4ba158b30b7045670cc82fd2abfa..3f9907cc2d11921174c81c99a81f662becd021a2 100644 --- a/src/kernel_services/ast_queries/logic_env.mli +++ b/src/kernel_services/ast_queries/logic_env.mli @@ -62,9 +62,6 @@ val preprocess_extension_block: plugin:string option -> string -> string * Logic_ptree.extended_decl list -> string * Logic_ptree.extended_decl list -(** Return the plugin name of the extension. *) -val extension_from : string -> string - (** {2 Global Tables} *) module Logic_info: State_builder.Hashtbl with type key = string and type data = Cil_types.logic_info list @@ -255,7 +252,6 @@ val set_extension_handler: preprocess_block: (plugin:string option -> string -> string * Logic_ptree.extended_decl list -> string * Logic_ptree.extended_decl list) -> - extension_from:(string -> string) -> unit (** Used to setup references related to the handling of ACSL extensions. If your name is not [Acsl_extension], do not call this.