From 34f41ff77a4ac9eae924c557bd8df38332cd4301 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 12 Feb 2020 16:26:30 +0100
Subject: [PATCH] [kernel] Change default ACSL extension short printer
---
.../examples/acsl_extension_ext_types.ml | 3 ++-
.../ast_queries/acsl_extension.ml | 20 +++++++++++--------
tests/spec/Extend_short_print.i | 2 +-
tests/spec/Extend_short_print.ml | 4 ++--
.../spec/oracle/Extend_short_print.res.oracle | 2 +-
5 files changed, 18 insertions(+), 13 deletions(-)
diff --git a/doc/developer/examples/acsl_extension_ext_types.ml b/doc/developer/examples/acsl_extension_ext_types.ml
index 504b903633e..a387bad3fef 100644
--- a/doc/developer/examples/acsl_extension_ext_types.ml
+++ b/doc/developer/examples/acsl_extension_ext_types.ml
@@ -30,7 +30,8 @@ let visitor _ _ = Cil.SkipChildren
let gen_printer s _pp fmt = function
| Ext_id i ->
- Format.fprintf fmt "%s%s" (if s then "" else "load: ") (Ts.find i).lt_name
+ Format.fprintf fmt "%s: %s"
+ (if s then "ext_type" else "load") (Ts.find i).lt_name
| _ -> assert false
let printer = gen_printer false
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index ade873ecd95..9d03166f5ac 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -31,7 +31,7 @@ type extension = {
typer: extension_typer ;
visitor: extension_visitor ;
printer: extension_printer ;
- short_printer: extension_printer option
+ short_printer: extension_printer ;
}
and extension_preprocessor =
lexpr list -> lexpr list
@@ -48,12 +48,17 @@ let default_printer printer fmt = function
| Ext_terms ts -> Pretty_utils.pp_list ~sep:",@ " printer#term fmt ts
| Ext_preds ps -> Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt ps
+let default_short_printer name _printer fmt _ext_kind =
+ Format.fprintf fmt "%s" name
+
let make
- category
+ name category
?(preprocessor=Extlib.id)
typer
?(visitor=fun _ _ -> Cil.DoChildren)
- ?(printer=default_printer) ?short_printer status =
+ ?(printer=default_printer)
+ ?(short_printer=default_short_printer name)
+ status =
{ category; status; preprocessor; typer; visitor; printer; short_printer }
module Extensions = struct
@@ -73,7 +78,7 @@ module Extensions = struct
let register
cat name ?preprocessor typer ?visitor ?printer ?short_printer status =
let info =
- make cat ?preprocessor typer ?visitor ?printer ?short_printer status
+ make name cat ?preprocessor typer ?visitor ?printer ?short_printer status
in
if is_extension name then
Kernel.warning ~wkey:Kernel.wkey_acsl_extension
@@ -106,9 +111,8 @@ module Extensions = struct
Format.fprintf fmt "@[<hov 2>%s %a;@]" name pp kind
let short_print name printer fmt kind =
- match (find name).short_printer with
- | None -> Format.fprintf fmt "%s" name
- | Some pp -> Format.fprintf fmt "%s: %a" name (pp printer) kind
+ let pp = (find name).short_printer in
+ Format.fprintf fmt "%a" (pp printer) kind
end
(* Registration functions *)
@@ -155,7 +159,7 @@ let deprecated_find ?(strong=true) name cat op_name =
match Hashtbl.find_opt Extensions.ext_tbl name with
| None ->
if strong then Hashtbl.add strong_cat name cat ;
- (make cat default_typer false)
+ (make name cat default_typer false)
| Some ext ->
if strong && Hashtbl.mem strong_cat name then begin
if ext.category = cat then ext
diff --git a/tests/spec/Extend_short_print.i b/tests/spec/Extend_short_print.i
index 62da2756985..568f3561f8b 100644
--- a/tests/spec/Extend_short_print.i
+++ b/tests/spec/Extend_short_print.i
@@ -5,5 +5,5 @@ OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
/*@
without_short \true ;
- with_short \true ;
+ has_short \true ;
*/
\ No newline at end of file
diff --git a/tests/spec/Extend_short_print.ml b/tests/spec/Extend_short_print.ml
index de0cb70361f..386cc1080b5 100644
--- a/tests/spec/Extend_short_print.ml
+++ b/tests/spec/Extend_short_print.ml
@@ -1,11 +1,11 @@
open Cil_types
let typer _context _loc _tree = Ext_id 42
-let short_printer _printer fmt _kind = Format.fprintf fmt "some content"
+let short_printer _printer fmt _kind = Format.fprintf fmt "HS: some content"
let () =
Acsl_extension.register_global "without_short" typer false ;
- Acsl_extension.register_global "with_short" typer ~short_printer false
+ Acsl_extension.register_global "has_short" typer ~short_printer false
let process_global _ = function
| Dextended(e, _, _) -> Kernel.feedback "%a" Cil_printer.pp_short_extended e
diff --git a/tests/spec/oracle/Extend_short_print.res.oracle b/tests/spec/oracle/Extend_short_print.res.oracle
index fe5db7f43bb..a44980575a8 100644
--- a/tests/spec/oracle/Extend_short_print.res.oracle
+++ b/tests/spec/oracle/Extend_short_print.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing tests/spec/Extend_short_print.i (no preprocessing)
-[kernel] with_short: some content
+[kernel] HS: some content
[kernel] without_short
--
GitLab