diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml index de79082709f3d342e78ddc6d5155a0f1f54584a9..12af98e3b6dcb4ed74098961dd63be4c80a2e86b 100644 --- a/src/plugins/rte/register.ml +++ b/src/plugins/rte/register.ml @@ -56,49 +56,40 @@ let compute () = Globals.Functions.iter (fun kf -> if include_function kf then !Db.RteGen.annotate_kf kf) - -(* journal utilities *) - -let journal_register ?comment is_dyn name ty_arg fctref fct = - let ty = Datatype.func ty_arg Datatype.unit in - Db.register fctref fct; - if is_dyn then - let _ignore = - Dynamic.register ?comment ~plugin:"RteGen" name ty fct - in - () - -let nojournal_register fctref fct = - Db.register fctref (fun () -> fct) - let () = - journal_register false - "annotate_kf" Kernel_function.ty Db.RteGen.annotate_kf Visit.annotate; - journal_register false "compute" Datatype.unit Db.RteGen.compute compute; - journal_register true - ~comment:"Generate all RTE annotations in the \ - given function." - "do_all_rte" Kernel_function.ty Db.RteGen.do_all_rte do_all_rte; - journal_register false - ~comment:"Generate all RTE annotations except pre-conditions \ - in the given function." - "do_rte" Kernel_function.ty Db.RteGen.do_rte do_rte; + Db.register Db.RteGen.annotate_kf Visit.annotate; + Db.register Db.RteGen.compute compute; + Db.register Db.RteGen.do_rte do_rte; + + Db.register Db.RteGen.do_all_rte do_all_rte; + let _ignore = + Dynamic.register + ~comment:"Generate all RTE annotations in the given function." + ~plugin:"RteGen" + "do_all_rte" + (Datatype.func Kernel_function.ty Datatype.unit) + do_all_rte + in + let open Generator in let open Db.RteGen in - nojournal_register get_signedOv_status Signed_overflow.accessor; - nojournal_register get_divMod_status Div_mod.accessor; - nojournal_register get_initialized_status Initialized.accessor; - nojournal_register get_signed_downCast_status Signed_downcast.accessor; - nojournal_register get_memAccess_status Mem_access.accessor; - nojournal_register get_pointerCall_status Pointer_call.accessor; - nojournal_register get_unsignedOv_status Unsigned_overflow.accessor; - nojournal_register get_unsignedDownCast_status Unsigned_downcast.accessor; - nojournal_register get_pointer_downcast_status Pointer_downcast.accessor; - nojournal_register get_float_to_int_status Float_to_int.accessor; - nojournal_register get_finite_float_status Finite_float.accessor; - nojournal_register get_pointer_value_status Pointer_value.accessor; - nojournal_register get_bool_value_status Bool_value.accessor ; - nojournal_register get_all_status all_statuses; + let register_getter fctref fct = + Db.register fctref (fun () -> fct) + in + register_getter get_signedOv_status Signed_overflow.accessor; + register_getter get_divMod_status Div_mod.accessor; + register_getter get_initialized_status Initialized.accessor; + register_getter get_signed_downCast_status Signed_downcast.accessor; + register_getter get_memAccess_status Mem_access.accessor; + register_getter get_pointerCall_status Pointer_call.accessor; + register_getter get_unsignedOv_status Unsigned_overflow.accessor; + register_getter get_unsignedDownCast_status Unsigned_downcast.accessor; + register_getter get_pointer_downcast_status Pointer_downcast.accessor; + register_getter get_float_to_int_status Float_to_int.accessor; + register_getter get_finite_float_status Finite_float.accessor; + register_getter get_pointer_value_status Pointer_value.accessor; + register_getter get_bool_value_status Bool_value.accessor ; + register_getter get_all_status all_statuses; ;; (* dynamic registration *)