PdgIndex.Signature
What we call a Signature
a mapping between keys that represent either a * function input or output, and some information.
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
| InCtrl | (* input control point *) |
| InNum of int | (* parameters numbered from 1 *) |
| 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
| OutRet | (* key for the output corresponding to the |
| OutLoc of Frama_c_kernel.Locations.Zone.t | (* key for output locations. used in call signatures only *) |
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 find_input : 'a t -> int -> 'a
val find_in_ctrl : 'info t -> 'info
val find_in_top : 'info t -> 'info
val find_out_ret : 'a 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 pretty :
( Stdlib.Format.formatter -> 'a -> unit ) ->
Stdlib.Format.formatter ->
'a t ->
unit
val pretty_key : Stdlib.Format.formatter -> key -> unit
val pretty_in_key : Stdlib.Format.formatter -> in_key -> unit
val pretty_out_key : Stdlib.Format.formatter -> out_key -> unit