diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index 767cf487636ff235b6e01cd46d9b498eb3c9c624..7424276f091edd55f04ec42b52f3cc91e49d1483 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -69,22 +69,20 @@ module Register (M : Annotation) =
struct
include M
- let typing_ext ~typing_context ~loc args =
+ let ext_typing typing_context loc args =
try export (parse ~typing_context args)
with Parse_error ->
typing_context.Logic_typing.error loc "Invalid %s directive" name
- let printer_ext _pp fmt lp =
+ let ext_printing _pp fmt lp =
print fmt (import lp)
let () =
- if is_loop_annot then begin
- Logic_typing.register_code_annot_next_loop_extension name false typing_ext;
- Cil_printer.register_loop_annot_extension name printer_ext
- end else begin
- Logic_typing.register_code_annot_next_stmt_extension name false typing_ext;
- Cil_printer.register_code_annot_extension name printer_ext
- end
+ let ext = { Acsl_extension.default with ext_typing ; ext_printing } in
+ if is_loop_annot then
+ Acsl_extension.register_code_annot_next_loop name ext
+ else
+ Acsl_extension.register_code_annot_next_stmt name ext
let get stmt =
let filter_add _emitter annot acc =
diff --git a/src/plugins/value/utils/widen_hints_ext.ml b/src/plugins/value/utils/widen_hints_ext.ml
index 743fc237c94b8db4fe15f4689cf34d6b9ec2da5c..b86b353196abd68a13be2d96727e6a8ff07f9b9c 100644
--- a/src/plugins/value/utils/widen_hints_ext.ml
+++ b/src/plugins/value/utils/widen_hints_ext.ml
@@ -137,30 +137,30 @@ let widen_hint_terms_of_terms terms =
with
Invalid_hint -> None
-let () = Logic_typing.register_code_annot_next_both_extension "widen_hints" false
- (fun ~typing_context ~loc args ->
- let var_term, hint_terms =
- terms_of_parsed_widen_hints typing_context loc args
- in
- let terms = var_term :: hint_terms in
- Ext_terms terms
- )
-
-let () = Cil_printer.register_code_annot_extension "widen_hints"
- (fun _pp fmt ext ->
- match ext with
- | Ext_id _ -> assert false
- | Ext_preds _ -> assert false
- | Ext_terms terms ->
- match widen_hint_terms_of_terms terms with
- | Some (hint_lval, hint_terms) ->
- Format.fprintf fmt "%a%a, %a"
- (Pretty_utils.pp_list ~sep:" " ~suf:":" Format.pp_print_string)
- hint_lval.names pp_hvars hint_lval.vars
- (Pretty_utils.pp_list ~sep:", " Printer.pp_term) hint_terms
- | None ->
- Format.fprintf fmt "<invalid widen_hints>"
- )
+let ext_typing typing_context loc args =
+ let var_term, hint_terms =
+ terms_of_parsed_widen_hints typing_context loc args
+ in
+ let terms = var_term :: hint_terms in
+ Ext_terms terms
+
+let ext_printing _pp fmt ext =
+ match ext with
+ | Ext_id _ -> assert false
+ | Ext_preds _ -> assert false
+ | Ext_terms terms ->
+ match widen_hint_terms_of_terms terms with
+ | Some (hint_lval, hint_terms) ->
+ Format.fprintf fmt "%a%a, %a"
+ (Pretty_utils.pp_list ~sep:" " ~suf:":" Format.pp_print_string)
+ hint_lval.names pp_hvars hint_lval.vars
+ (Pretty_utils.pp_list ~sep:", " Printer.pp_term) hint_terms
+ | None ->
+ Format.fprintf fmt "<invalid widen_hints>"
+
+let () =
+ Acsl_extension.register_code_annot_next_both "widen_hints"
+ { Acsl_extension.default with ext_typing ; ext_printing }
let get_widen_hints_annots stmt =
Annotations.fold_code_annot
diff --git a/src/plugins/wp/RegionAnnot.ml b/src/plugins/wp/RegionAnnot.ml
index 5ada4f4dc9434380e19dfa9d69147f562c6ecb12..2287453b699bed94d09f9237006b11f84024434a 100644
--- a/src/plugins/wp/RegionAnnot.ml
+++ b/src/plugins/wp/RegionAnnot.ml
@@ -440,7 +440,7 @@ let rec parse_region env p =
let path = parse_lpath env p in
env.paths <- path :: env.paths
-let typecheck ~typing_context ~loc:_loc ps =
+let typecheck typing_context _loc ps =
let env = {
name = None ;
declared = [] ;
@@ -482,12 +482,12 @@ let specified =
let register () =
if Wp.Region.get () || Wp.Region_annot.get () ||
- List.exists specified (Wp.Model.get ())
+ List.exists specified (Wp.Model.get ())
then
- begin
- Logic_typing.register_behavior_extension "region" true typecheck ;
- Cil_printer.register_behavior_extension "region" pp_extension ;
- end
+ Acsl_extension.register_behavior "region"
+ { Acsl_extension.default with ext_status=true;
+ ext_typing=typecheck;
+ ext_printing=pp_extension}
let () = Cmdline.run_after_configuring_stage register
diff --git a/src/plugins/wp/dyncall.ml b/src/plugins/wp/dyncall.ml
index 8b0dedf82a8033484a5732a5f6ae3d59563ff7c9..83aeeb8578a2ce842d5fe99da91a609afdd03ef5 100644
--- a/src/plugins/wp/dyncall.ml
+++ b/src/plugins/wp/dyncall.ml
@@ -37,7 +37,7 @@ let find_call env loc f =
with Not_found ->
env.error loc "Unknown function '%s'" f
-let typecheck ~typing_context ~loc ps =
+let typecheck typing_context loc ps =
ignore loc ;
let fs =
List.map
@@ -261,8 +261,11 @@ let register =
if (not !once) &&
Wp_parameters.DynCall.get () then begin
once := true;
- Logic_typing.register_code_annot_next_stmt_extension "calls" true typecheck;
- Logic_typing.register_behavior_extension "instanceof" true typecheck ;
+ let ext =
+ { Acsl_extension.default with ext_status=true; ext_typing=typecheck }
+ in
+ Acsl_extension.register_code_annot_next_stmt "calls" ext;
+ Acsl_extension.register_behavior "instanceof" ext;
end
let () = Cmdline.run_after_configuring_stage register
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index af9696e583520f9dcabb3cbdf15118eeb53e1d7d..ce95063c1e0f6a60514768cf3799be280c399b5e 100644
--- a/tests/spec/Extend.ml
+++ b/tests/spec/Extend.ml
@@ -2,8 +2,7 @@ open Logic_ptree
open Cil_types
open Logic_typing
-let type_foo ~typing_context ~loc l =
- let _loc = loc in
+let type_foo typing_context _loc l =
let preds =
List.map
(typing_context.type_predicate
@@ -24,8 +23,7 @@ module Bar_table =
let size = 3
end)
-let type_bar ~typing_context ~loc l =
- let _loc = loc in
+let type_bar typing_context _loc l =
let i = Count.next() in
let p =
List.map
@@ -61,7 +59,7 @@ let visit_bar vis ext =
| Ext_terms _ | Ext_preds _ ->
Kernel.fatal "bar extension should have ids as arguments"
-let type_baz ~typing_context ~loc:_loc l =
+let type_baz typing_context _loc l =
let t =
List.map
(typing_context.type_term typing_context typing_context.pre_state) l
@@ -88,7 +86,7 @@ let add_builtin () =
let () = add_builtin ()
-let type_bla ~typing_context ~loc:_loc l =
+let type_bla typing_context _loc l =
let type_predicate ctxt env p =
match p.lexpr_node with
| PLapp("\\trace", [], [pred]) ->
@@ -107,16 +105,26 @@ let type_bla ~typing_context ~loc:_loc l =
Ext_preds l
let () =
- Logic_typing.register_behavior_extension "foo" false type_foo;
- Logic_typing.register_behavior_extension "bar" false type_bar;
- Logic_typing.register_behavior_extension "bla" false type_bla;
- Cil_printer.register_behavior_extension "bar" print_bar;
- Cil.register_behavior_extension "bar" visit_bar;
- Logic_typing.register_code_annot_next_both_extension "baz" false type_baz;
- Logic_typing.register_code_annot_next_loop_extension "lfoo" false type_foo;
- Logic_typing.register_code_annot_extension "ca_foo" false type_foo;
- Logic_typing.register_code_annot_next_stmt_extension "ns_foo" false type_foo;
- Logic_typing.register_global_extension "global_foo" false type_foo
+ Acsl_extension.register_behavior "foo"
+ { Acsl_extension.default with ext_typing = type_foo } ;
+ Acsl_extension.register_code_annot_next_loop "lfoo"
+ { Acsl_extension.default with ext_typing = type_foo } ;
+ Acsl_extension.register_code_annot "ca_foo"
+ { Acsl_extension.default with ext_typing = type_foo } ;
+ Acsl_extension.register_code_annot_next_stmt "ns_foo"
+ { Acsl_extension.default with ext_typing = type_foo } ;
+ Acsl_extension.register_global "global_foo"
+ { Acsl_extension.default with ext_typing = type_foo } ;
+ Acsl_extension.register_behavior "bar"
+ { Acsl_extension.default with
+ ext_typing = type_bar ;
+ ext_printing = print_bar ;
+ ext_visit = visit_bar
+ } ;
+ Acsl_extension.register_behavior "bla"
+ { Acsl_extension.default with ext_typing = type_bla } ;
+ Acsl_extension.register_code_annot_next_both "baz"
+ { Acsl_extension.default with ext_typing = type_baz }
let run () =
Ast.compute ();
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
index c60a714b9bf921abd03047c7e87337548365b108..09714efad25fa90d283e529c0ae1e3f7d6a9ea84 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -6,7 +6,7 @@ let load_theory = function
raise Not_found
| _ -> assert false
-let typing ~typing_context ~loc lexprs =
+let ext_typing typing_context loc lexprs =
ignore loc ;
let type_predicate =
typing_context.type_predicate typing_context (Lenv.empty ())
@@ -17,7 +17,7 @@ let typing ~typing_context ~loc lexprs =
let () =
- Logic_typing.register_global_extension "why3" false typing
+ Acsl_extension.(register_global "why3" { default with ext_typing })
let main () =
try