Frama_c_kernel.Populate_spec
This module is used to generate missing specifications. Options Kernel
.GeneratedDefaultSpec, Kernel.GeneratedSpecMode
and Kernel.GeneratedSpecCustom
can be used to choose precisely which clause to generate in which case.
Different types of clauses which can be generated via populate_funspec
.
type t_exits =
(Cil_types.termination_kind * Cil_types.identified_predicate) list
Represents exits clause in the sense of Cil_types.behavior.b_post_cond
.
type t_assigns = Cil_types.assigns
Assigns clause
type t_allocates = Cil_types.allocation
Allocation clause
type t_requires = Cil_types.identified_predicate list
Represents requires clause in the sense of Cil_types.behavior.b_requires
.
type t_terminates = Cil_types.identified_predicate option
Represents terminates clause in the sense of Cil_types.spec.spec_terminates
.
type 'a gen = Cil_types.kernel_function -> Cil_types.spec -> 'a
Type of a function that, given a Kernel_function.t
and a Cil_types.spec
, returns a clause. Accepted clause types include t_exits
, t_assigns
, t_requires
, t_allocates
and t_terminates
.
type status = Property_status.emitted_status
Alias for brevity, status emitted for properties.
val register :
?gen_exits:t_exits gen ->
?status_exits:status ->
?gen_assigns:t_assigns gen ->
?status_assigns:status ->
?gen_requires:t_requires gen ->
?gen_allocates:t_allocates gen ->
?status_allocates:status ->
?gen_terminates:t_terminates gen ->
?status_terminates:status ->
string ->
unit
register ?gen_exits ?gen_requires ?status_allocates ... name
registers a new mode called name
which can then be used for specification generation (see Kernel.GeneratedSpecMode
and Kernel.GeneratedSpecCustom
). All parameters except name
are optional, meaning default action (mode Frama_C) will be performed if left unspecified (triggers a warning).
val populate_funspec :
?loc:Cil_types.location ->
?do_body:bool ->
Cil_types.kernel_function ->
clause list ->
unit
populate_funspec ~loc ~do_body kf clauses
generates missing specifications for kf
according to selected clauses
. loc
is set to Kernel_function.get_location kf
by default, and is used to specify warnings locations. By default do_body
is false, meaning only specification of prototypes will be generated.