sig
type key
module Key :
sig
val zero : Partition.key
val compare : Partition.key -> Partition.key -> int
val pretty : Stdlib.Format.formatter -> Partition.key -> unit
val exceed_rationing : Partition.key -> bool
end
type 'state partition
val empty : 'a Partition.partition
val is_empty : 'a Partition.partition -> bool
val size : 'a Partition.partition -> int
val to_list : 'a Partition.partition -> 'a list
val find : Partition.key -> 'a Partition.partition -> 'a
val replace :
Partition.key -> 'a -> 'a Partition.partition -> 'a Partition.partition
val merge :
(Partition.key -> 'a option -> 'b option -> 'c option) ->
'a Partition.partition ->
'b Partition.partition -> 'c Partition.partition
val iter : (Partition.key -> 'a -> unit) -> 'a Partition.partition -> unit
val filter :
(Partition.key -> 'a -> bool) ->
'a Partition.partition -> 'a Partition.partition
val map : ('a -> 'a) -> 'a Partition.partition -> 'a Partition.partition
type branch = int
type rationing
val new_rationing : limit:int -> merge:bool -> Partition.rationing
type unroll_limit =
ExpLimit of Cil_types.exp
| IntLimit of int
| AutoUnroll of Cil_types.stmt * int * int
type split_kind = Static | Dynamic
type split_monitor
val new_monitor : split_limit:int -> Partition.split_monitor
type action =
Enter_loop of Partition.unroll_limit
| Leave_loop
| Incr_loop
| Branch of Partition.branch * int
| Ration of Partition.rationing
| Restrict of Cil_types.exp * Integer.t list
| Split of Cil_types.exp * Partition.split_kind * Partition.split_monitor
| Merge of Cil_types.exp * Partition.split_kind
| Update_dynamic_splits
exception InvalidAction
module MakeFlow :
functor (Abstract : Abstractions.Eva) ->
sig
type state = Abstract.Dom.t
type t
val empty : Partition.MakeFlow.t
val initial : Partition.MakeFlow.state list -> Partition.MakeFlow.t
val to_list : Partition.MakeFlow.t -> Partition.MakeFlow.state list
val of_partition :
Partition.MakeFlow.state Partition.partition ->
Partition.MakeFlow.t
val to_partition :
Partition.MakeFlow.t ->
Partition.MakeFlow.state Partition.partition
val is_empty : Partition.MakeFlow.t -> bool
val size : Partition.MakeFlow.t -> int
val union :
Partition.MakeFlow.t ->
Partition.MakeFlow.t -> Partition.MakeFlow.t
val transfer_keys :
Partition.MakeFlow.t -> Partition.action -> Partition.MakeFlow.t
val transfer_states :
(Partition.MakeFlow.state -> Partition.MakeFlow.state list) ->
Partition.MakeFlow.t -> Partition.MakeFlow.t
val iter :
(Partition.MakeFlow.state -> unit) -> Partition.MakeFlow.t -> unit
val filter_map :
(Partition.key ->
Partition.MakeFlow.state -> Partition.MakeFlow.state option) ->
Partition.MakeFlow.t -> Partition.MakeFlow.t
val join_duplicate_keys :
Partition.MakeFlow.t -> Partition.MakeFlow.t
end
end