diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli index f255ff01310a4bf30814439a93f04858423f1333..e546d25b13e9bc5a76b1cbff9bf497dfbe954c8e 100644 --- a/src/kernel_services/ast_data/annotations.mli +++ b/src/kernel_services/ast_data/annotations.mli @@ -65,9 +65,7 @@ val funspec: ?emitter:Emitter.t -> kernel_function -> funspec (** Get the contract associated to the given function. If [emitter] is specified, return only the annotations that - has been generated by this [emitter]. If [populate] is set to [true] - (default is [true]), then the default contract of function declaration is - generated. + has been generated by this [emitter]. @raise No_funspec whenever the given function has no specification @before Frama-C+dev the optional parameter [populate] was meant to generate missing spec. Use {!Populate_spec.populate_funspec} instead. *) @@ -87,7 +85,7 @@ val behaviors: val decreases: ?emitter:Emitter.t -> kernel_function -> variant option (** If any, get the decrease clause of the contract associated to the given - function. Meaning of [emitter] and [populate] is similar to {!funspec}. + function. Meaning of [emitter] is similar to {!funspec}. @raise No_funspec whenever the given function has no specification @before Frama-C+dev the optional parameter [populate] was meant to generate missing spec. Use {!Populate_spec.populate_funspec} instead. *) @@ -95,7 +93,7 @@ val decreases: val terminates: ?emitter:Emitter.t -> kernel_function -> identified_predicate option (** If any, get the terminates clause of the contract associated to the given - function. Meaning of [emitter] and [populate] is similar to {!funspec}. + function. Meaning of [emitter] is similar to {!funspec}. @raise No_funspec whenever the given function has no specification @before Frama-C+dev the optional parameter [populate] was meant to generate missing spec. Use {!Populate_spec.populate_funspec} instead. *) @@ -103,7 +101,7 @@ val terminates: val complete: ?emitter:Emitter.t -> kernel_function -> string list list (** Get the complete behaviors clause of the contract associated to the given - function. Meaning of [emitter] and [populate] is similar to {!funspec}. + function. Meaning of [emitter] is similar to {!funspec}. @raise No_funspec whenever the given function has no specification @before Frama-C+dev the optional parameter [populate] was meant to generate missing spec. Use {!Populate_spec.populate_funspec} instead. *) @@ -111,8 +109,7 @@ val complete: val disjoint: ?emitter:Emitter.t -> kernel_function -> string list list (** If any, get the disjoint behavior clause of the contract associated to the - given function. Meaning of [emitter] and [populate] is similar to - {!funspec}. + given function. Meaning of [emitter] is similar to {!funspec}. @raise No_funspec whenever the given function has no specification @before Frama-C+dev the optional parameter [populate] was meant to generate missing spec. Use {!Populate_spec.populate_funspec} instead. *)