diff --git a/src/plugins/rte/RteGen.mli b/src/plugins/rte/RteGen.mli index fb3e32553ca4014f94426d46d9103522c87a7766..a191e61ffb46c4f288a85b9191dd0bcb51731fa3 100644 --- a/src/plugins/rte/RteGen.mli +++ b/src/plugins/rte/RteGen.mli @@ -124,16 +124,7 @@ sig *) type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit - (** Low-level iterators - - The [on_alarm ki ?status alarm] callback is invoked with - the k-instruction originating the alarm and the already known status, - if any. - - Potential alarms can be specified by the provided flags, - with defaults from the Kernel and RTE plug-in options. - *) - + (** Type of low-level iterators visiting an element ['a] of the AST *) type 'a iterator = ?flags:flags -> on_alarm -> Kernel_function.t -> Cil_types.stmt -> 'a -> unit diff --git a/src/plugins/rte/visit.mli b/src/plugins/rte/visit.mli index 4c7f5fc71030ec45ed203a5f00936d146994f052..1f75de9bd222c330dcaff8e224781f593ddfb688 100644 --- a/src/plugins/rte/visit.mli +++ b/src/plugins/rte/visit.mli @@ -120,16 +120,7 @@ val flags_none : flags *) type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit -(** Low-level iterators - - The [on_alarm ki ?status alarm] callback is invoked with - the k-instruction originating the alarm and the already known status, - if any. - - Potential alarms can be specified by the provided flags, - with defaults from the Kernel and RTE plug-in options. -*) - +(** Type of low-level iterators visiting an element ['a] of the AST *) type 'a iterator = ?flags:flags -> on_alarm -> Kernel_function.t -> Cil_types.stmt -> 'a -> unit