Module Acsl_extension

type extension_preprocessor = Logic_ptree.lexpr list -> Logic_ptree.lexpr list
type extension_typer = Logic_typing.typing_context -> Logic_ptree.location -> Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind
type extension_visitor = Cil.cilVisitor -> Cil_types.acsl_extension_kind -> Cil_types.acsl_extension_kind Cil.visitAction
type extension_preprocessor_block = (string * Logic_ptree.extended_decl list) -> string * Logic_ptree.extended_decl list
type extension_typer_block = Logic_typing.typing_context -> Logic_ptree.location -> (string * Logic_ptree.extended_decl list) -> Cil_types.acsl_extension_kind
type extension_printer = Printer_api.extensible_printer_type -> Stdlib.Format.formatter -> Cil_types.acsl_extension_kind -> unit
val register_behavior : string -> ?⁠preprocessor:extension_preprocessor -> extension_typer -> ?⁠visitor:extension_visitor -> ?⁠printer:extension_printer -> ?⁠short_printer:extension_printer -> bool -> unit
val register_global : string -> ?⁠preprocessor:extension_preprocessor -> extension_typer -> ?⁠visitor:extension_visitor -> ?⁠printer:extension_printer -> ?⁠short_printer:extension_printer -> bool -> unit
val register_global_block : string -> ?⁠preprocessor:extension_preprocessor_block -> extension_typer_block -> ?⁠visitor:extension_visitor -> ?⁠printer:extension_printer -> ?⁠short_printer:extension_printer -> bool -> unit
val register_code_annot : string -> ?⁠preprocessor:extension_preprocessor -> extension_typer -> ?⁠visitor:extension_visitor -> ?⁠printer:extension_printer -> ?⁠short_printer:extension_printer -> bool -> unit
val register_code_annot_next_stmt : string -> ?⁠preprocessor:extension_preprocessor -> extension_typer -> ?⁠visitor:extension_visitor -> ?⁠printer:extension_printer -> ?⁠short_printer:extension_printer -> bool -> unit
val register_code_annot_next_loop : string -> ?⁠preprocessor:extension_preprocessor -> extension_typer -> ?⁠visitor:extension_visitor -> ?⁠printer:extension_printer -> ?⁠short_printer:extension_printer -> bool -> unit
val register_code_annot_next_both : string -> ?⁠preprocessor:extension_preprocessor -> extension_typer -> ?⁠visitor:extension_visitor -> ?⁠printer:extension_printer -> ?⁠short_printer:extension_printer -> bool -> unit