Skip to content
Snippets Groups Projects
Commit 517cc90b authored by Thibault Martin's avatar Thibault Martin
Browse files

Merge branch 'fix/blanchard/doc/removed-parameter' into 'master'

[doc] remove references to a removed parameter

See merge request frama-c/frama-c!4372
parents 49876062 e02682f4
No related branches found
No related tags found
No related merge requests found
...@@ -65,9 +65,7 @@ val funspec: ...@@ -65,9 +65,7 @@ val funspec:
?emitter:Emitter.t -> kernel_function -> funspec ?emitter:Emitter.t -> kernel_function -> funspec
(** Get the contract associated to the given function. (** Get the contract associated to the given function.
If [emitter] is specified, return only the annotations that If [emitter] is specified, return only the annotations that
has been generated by this [emitter]. If [populate] is set to [true] has been generated by this [emitter].
(default is [true]), then the default contract of function declaration is
generated.
@raise No_funspec whenever the given function has no specification @raise No_funspec whenever the given function has no specification
@before Frama-C+dev the optional parameter [populate] was meant to generate @before Frama-C+dev the optional parameter [populate] was meant to generate
missing spec. Use {!Populate_spec.populate_funspec} instead. *) missing spec. Use {!Populate_spec.populate_funspec} instead. *)
...@@ -87,7 +85,7 @@ val behaviors: ...@@ -87,7 +85,7 @@ val behaviors:
val decreases: val decreases:
?emitter:Emitter.t -> kernel_function -> variant option ?emitter:Emitter.t -> kernel_function -> variant option
(** If any, get the decrease clause of the contract associated to the given (** 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 @raise No_funspec whenever the given function has no specification
@before Frama-C+dev the optional parameter [populate] was meant to generate @before Frama-C+dev the optional parameter [populate] was meant to generate
missing spec. Use {!Populate_spec.populate_funspec} instead. *) missing spec. Use {!Populate_spec.populate_funspec} instead. *)
...@@ -95,7 +93,7 @@ val decreases: ...@@ -95,7 +93,7 @@ val decreases:
val terminates: val terminates:
?emitter:Emitter.t -> kernel_function -> identified_predicate option ?emitter:Emitter.t -> kernel_function -> identified_predicate option
(** If any, get the terminates clause of the contract associated to the given (** 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 @raise No_funspec whenever the given function has no specification
@before Frama-C+dev the optional parameter [populate] was meant to generate @before Frama-C+dev the optional parameter [populate] was meant to generate
missing spec. Use {!Populate_spec.populate_funspec} instead. *) missing spec. Use {!Populate_spec.populate_funspec} instead. *)
...@@ -103,7 +101,7 @@ val terminates: ...@@ -103,7 +101,7 @@ val terminates:
val complete: val complete:
?emitter:Emitter.t -> kernel_function -> string list list ?emitter:Emitter.t -> kernel_function -> string list list
(** Get the complete behaviors clause of the contract associated to the given (** 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 @raise No_funspec whenever the given function has no specification
@before Frama-C+dev the optional parameter [populate] was meant to generate @before Frama-C+dev the optional parameter [populate] was meant to generate
missing spec. Use {!Populate_spec.populate_funspec} instead. *) missing spec. Use {!Populate_spec.populate_funspec} instead. *)
...@@ -111,8 +109,7 @@ val complete: ...@@ -111,8 +109,7 @@ val complete:
val disjoint: val disjoint:
?emitter:Emitter.t -> kernel_function -> string list list ?emitter:Emitter.t -> kernel_function -> string list list
(** If any, get the disjoint behavior clause of the contract associated to the (** If any, get the disjoint behavior clause of the contract associated to the
given function. Meaning of [emitter] and [populate] is similar to given function. Meaning of [emitter] is similar to {!funspec}.
{!funspec}.
@raise No_funspec whenever the given function has no specification @raise No_funspec whenever the given function has no specification
@before Frama-C+dev the optional parameter [populate] was meant to generate @before Frama-C+dev the optional parameter [populate] was meant to generate
missing spec. Use {!Populate_spec.populate_funspec} instead. *) missing spec. Use {!Populate_spec.populate_funspec} instead. *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment