Functor Transfer_specification.Make

module Make: functor (Value : Abstract_value.External) -> functor (Location : Abstract_location.External) -> functor (Domain : Abstract_domain.External  with type value = Value.t
                                       and type location = Location.location) -> functor (States : Powerset.S  with type state = Domain.t) -> functor (Logic : Transfer_logic.S  with type state = Domain.t
                               and type states = States.t) -> sig .. end

Parameters:

`Value`	:	`Abstract_value.External`
`Location`	:	`Abstract_location.External`
`Domain`	:	`Abstract_domain.External with type value = Value.t and type location = Location.location`
`States`	:	`Powerset.S with type state = Domain.t`
`Logic`	:	`Transfer_logic.S with type state = Domain.t and type states = States.t`

val treat_statement_assigns : Cil_types.assigns -> Domain.t -> Domain.t

val compute_using_specification : Cil_types.kinstr ->
       Value.t Eval.call ->
       Cil_types.spec -> Domain.t -> Domain.t list Eval.or_bottom