From e0fa3494bd8183353669dff775b7a5d141e80e60 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 24 Jan 2020 08:43:53 +0100
Subject: [PATCH] [kernel] Refs for ACSL extension and registration
---
src/kernel_services/ast_printing/cil_printer.ml | 9 +++++++++
src/kernel_services/ast_printing/cil_printer.mli | 11 +++++++++++
src/kernel_services/ast_queries/acsl_extension.ml | 14 ++++++++++++++
src/kernel_services/ast_queries/cil.ml | 9 +++++++++
src/kernel_services/ast_queries/cil.mli | 9 +++++++++
src/kernel_services/ast_queries/logic_env.ml | 12 ++++++++++++
src/kernel_services/ast_queries/logic_env.mli | 9 +++++++++
src/kernel_services/ast_queries/logic_typing.ml | 11 +++++++++++
src/kernel_services/ast_queries/logic_typing.mli | 12 ++++++++++++
9 files changed, 96 insertions(+)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 13259d5a56c..98b6fab58ce 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -27,6 +27,15 @@ open Cil_datatype
open Printer_api
open Format
+let initialized_extensions = ref false
+let ref_print_extension = ref (fun _ _ _ _ -> assert false)
+
+let set_extension_handler ~print =
+ assert (not !initialized_extensions) ;
+ ref_print_extension := print ;
+ initialized_extensions := true ;
+ ()
+
module Behavior_extensions = struct
let printer_tbl = Hashtbl.create 5
diff --git a/src/kernel_services/ast_printing/cil_printer.mli b/src/kernel_services/ast_printing/cil_printer.mli
index 3edbd8bc09e..04e4206ae37 100644
--- a/src/kernel_services/ast_printing/cil_printer.mli
+++ b/src/kernel_services/ast_printing/cil_printer.mli
@@ -73,6 +73,17 @@ val print_global: Cil_types.global -> bool
(** Is the given global displayed by the pretty-printer.
@since Aluminium-20160501 *)
+(**/**)
+
+val set_extension_handler:
+ print:(string -> Printer_api.extensible_printer_type -> Format.formatter ->
+ Cil_types.acsl_extension_kind -> unit) ->
+ unit
+(** Used to setup a reference related to the handling of ACSL extensions.
+ If your name is not [Acsl_extension], do not call this
+ @since Frama-C+dev
+*)
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 3354d9e42e6..f59ee45bf2f 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -103,3 +103,17 @@ let register_code_annot_next_loop =
Extensions.register (Ext_code_annot Ext_next_loop)
let register_code_annot_next_both =
Extensions.register (Ext_code_annot Ext_next_both)
+
+(* Setup global references *)
+
+let () =
+ Logic_env.set_extension_handler
+ ~category:Extensions.category
+ ~is_extension: Extensions.is_extension ;
+ Logic_typing.set_extension_handler
+ ~is_extension: Extensions.is_extension
+ ~typer: Extensions.typing ;
+ Cil.set_extension_handler
+ ~visit: Extensions.visit ;
+ Cil_printer.set_extension_handler
+ ~print: Extensions.print
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d52be341225..d17d73e3598 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -757,6 +757,15 @@ let alphatrue _ = true
let visitor_tbl = Hashtbl.create 5
+let initialized_extensions = ref false
+let ref_visit_extension = ref (fun _ _ _ -> assert false)
+
+let set_extension_handler ~visit =
+ assert (not !initialized_extensions) ;
+ ref_visit_extension := visit ;
+ initialized_extensions := true ;
+ ()
+
let register_behavior_extension name ext = Hashtbl.add visitor_tbl name ext
(* sm/gn: cil visitor interface for traversing Cil trees. *)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 71441398d0f..61d314736e2 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2283,6 +2283,15 @@ val pp_ikind_ref: (Format.formatter -> ikind -> unit) ref
val pp_attribute_ref: (Format.formatter -> attribute -> unit) ref
val pp_attributes_ref: (Format.formatter -> attribute list -> unit) ref
+val set_extension_handler:
+ visit:(string -> cilVisitor -> acsl_extension_kind ->
+ acsl_extension_kind visitAction) ->
+ unit
+(** Used to setup a reference related to the handling of ACSL extensions.
+ If your name is not [Acsl_extension], do not call this
+ @since Frama-C+dev
+*)
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index 5c09918e303..341ab6de574 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -24,6 +24,18 @@
open Cil_types
+let initialized_extensions = ref false
+let ref_is_extension = ref (fun _ -> assert false)
+let ref_extension_category = ref (fun _ -> assert false)
+
+let set_extension_handler ~category ~is_extension =
+ assert (not !initialized_extensions) ;
+ ref_is_extension := is_extension ;
+ ref_extension_category := category ;
+ initialized_extensions := true ;
+ ()
+
+
let extensions = ref Datatype.String.Map.empty
let is_extension s = Datatype.String.Map.mem s !extensions
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index afa488e5c8e..2207c731d99 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -204,6 +204,15 @@ val builtin_types_as_typenames: unit -> unit
(** {2 Internal use} *)
+val set_extension_handler:
+ category:(string -> ext_category option) ->
+ is_extension:(string -> bool) ->
+ unit
+(** Used to setup references related to the handling of ACSL extensions.
+ If your name is not [Acsl_extension], do not call this
+ @since Frama-C+dev
+*)
+
val init_dependencies: State.t -> unit
(** Used to postpone dependency of Lenv global tables wrt Cil_state, which
is initialized afterwards. *)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 08b217e0cc3..586294e2a0d 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -524,6 +524,17 @@ type typing_context = {
on_error: 'a 'b. ('a -> 'b) -> (unit -> unit) -> 'a -> 'b
}
+let initialized_extensions = ref false
+let ref_is_extension = ref (fun _ -> assert false)
+let ref_type_extension = ref (fun _ _ _ _ -> assert false)
+
+let set_extension_handler ~is_extension ~typer =
+ assert (not !initialized_extensions) ;
+ ref_is_extension := is_extension ;
+ ref_type_extension := typer ;
+ initialized_extensions := true ;
+ ()
+
module Extensions = struct
let typer_tbl = Hashtbl.create 5
let find_typer name = Hashtbl.find typer_tbl name
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index e6c6c5460f6..5d6bb73f7ff 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -371,6 +371,18 @@ val enter_post_state: Lenv.t -> termination_kind -> Lenv.t
val post_state_env: termination_kind -> logic_type -> Lenv.t
+(** {2 Internal use} *)
+
+val set_extension_handler:
+ is_extension:(string -> bool) ->
+ typer:(string -> typing_context -> location -> Logic_ptree.lexpr list ->
+ (bool * acsl_extension_kind)) ->
+ unit
+(** Used to setup references related to the handling of ACSL extensions.
+ If your name is not [Acsl_extension], do not call this
+ @since Frama-C+dev
+*)
+
(*
Local Variables:
compile-command: "make -C ../../.."
--
GitLab