From e05d35a7e4b4ceeabd731cabf202fd273280bea0 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 13 Feb 2020 07:44:18 +0100
Subject: [PATCH] [kernel] Changes types definitions in Acsl_extension
---
.../ast_queries/acsl_extension.ml | 18 +++++++++---------
1 file changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 9d03166f5ac..e82c29b554f 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
--
GitLab