diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml index 9d03166f5ac198336f0341a59af300c7880cd65b..e82c29b554f4acfc0e56a08282a5a8924b214326 100644 --- a/src/kernel_services/ast_queries/acsl_extension.ml +++ b/src/kernel_services/ast_queries/acsl_extension.ml @@ -24,6 +24,15 @@ open Cil_types open Logic_typing open Logic_ptree +type extension_preprocessor = + lexpr list -> lexpr list +type extension_typer = + typing_context -> location -> lexpr list -> acsl_extension_kind +type extension_visitor = + Cil.cilVisitor -> acsl_extension_kind -> acsl_extension_kind Cil.visitAction +type extension_printer = + Printer_api.extensible_printer_type -> Format.formatter -> + acsl_extension_kind -> unit type extension = { category: ext_category ; status: bool ; @@ -33,15 +42,6 @@ type extension = { printer: extension_printer ; short_printer: extension_printer ; } -and extension_preprocessor = - lexpr list -> lexpr list -and extension_typer = - typing_context -> location -> lexpr list -> acsl_extension_kind -and extension_visitor = - Cil.cilVisitor -> acsl_extension_kind -> acsl_extension_kind Cil.visitAction -and extension_printer = - Printer_api.extensible_printer_type -> Format.formatter -> - acsl_extension_kind -> unit let default_printer printer fmt = function | Ext_id i -> Format.fprintf fmt "%d" i