[kernel] Replace deprecated calls to old extension API

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 =

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

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
 

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

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 ();

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