Skip to content
Snippets Groups Projects
Commit e05d35a7 authored by Allan Blanchard's avatar Allan Blanchard Committed by Virgile Prevosto
Browse files

[kernel] Changes types definitions in Acsl_extension

parent 34f41ff7
No related branches found
No related tags found
No related merge requests found
...@@ -24,6 +24,15 @@ open Cil_types ...@@ -24,6 +24,15 @@ open Cil_types
open Logic_typing open Logic_typing
open Logic_ptree 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 = { type extension = {
category: ext_category ; category: ext_category ;
status: bool ; status: bool ;
...@@ -33,15 +42,6 @@ type extension = { ...@@ -33,15 +42,6 @@ type extension = {
printer: extension_printer ; printer: extension_printer ;
short_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 let default_printer printer fmt = function
| Ext_id i -> Format.fprintf fmt "%d" i | Ext_id i -> Format.fprintf fmt "%d" i
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment