package frama-c

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

What we call a Signature a mapping between keys that represent either a * function input or output, and some information.

type 'a t

type of a signature where 'a is the type of the information that we * want to store for each input/output.

type in_key = private
  1. | InCtrl
    (*

    input control point

    *)
  2. | InNum of int
    (*

    parameters numbered from 1

    *)
  3. | InImpl of Frama_c_kernel.Locations.Zone.t
    (*

    key for implicit inputs. Used in function signatures only

    *)

key for input elements

type out_key = private
  1. | OutRet
    (*

    key for the output corresponding to the return

    *)
  2. | OutLoc of Frama_c_kernel.Locations.Zone.t
    (*

    key for output locations. used in call signatures only

    *)
type key = private
  1. | In of in_key
  2. | Out of out_key

a key represents either an input or an output of a function.

val empty : 'a t

build a new, empty signature

val mk_undef_in_key : Frama_c_kernel.Locations.Zone.t -> in_key
val cmp_in_key : in_key -> in_key -> int
val cmp_out_key : out_key -> out_key -> int
val equal_out_key : out_key -> out_key -> bool
val find_info : 'a t -> key -> 'a
val find_input : 'a t -> int -> 'a
val find_in_ctrl : 'info t -> 'info
val find_in_top : 'info t -> 'info
val find_in_info : 'info t -> in_key -> 'info
val find_out_ret : 'a t -> 'a
val find_out_info : 'info t -> out_key -> 'info
val fold : ('a -> (key * 'b) -> 'a) -> 'a -> 'b t -> 'a
val fold_num_inputs : ('a -> (int * 'b) -> 'a) -> 'a -> 'b t -> 'a
val fold_impl_inputs : ('a -> (Frama_c_kernel.Locations.Zone.t * 'b) -> 'a) -> 'a -> 'b t -> 'a
val fold_matching_impl_inputs : Frama_c_kernel.Locations.Zone.t -> ('a -> (Frama_c_kernel.Locations.Zone.t * 'b) -> 'a) -> 'a -> 'b t -> 'a
val fold_all_inputs : ('a -> (in_key * 'b) -> 'a) -> 'a -> 'b t -> 'a
val fold_all_outputs : ('a -> (out_key * 'b) -> 'a) -> 'a -> 'b t -> 'a
val pretty : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
val pretty_key : Format.formatter -> key -> unit
val pretty_in_key : Format.formatter -> in_key -> unit
val pretty_out_key : Format.formatter -> out_key -> unit