package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

  • since 28.0-Nickel
type clause = [
  1. | `Exits
  2. | `Assigns
  3. | `Requires
  4. | `Allocates
  5. | `Terminates
]

Different types of clauses which can be generated via populate_funspec.

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 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.

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct