functor
  (Fenv : Dataflows.FUNCTION_ENV) (X : sig
                                         val _version : string
                                         val _kf : Cil_types.kernel_function
                                         val stmt_state :
                                           Cil_types.stmt -> Db.Value.state
                                         val at_call :
                                           Cil_types.stmt ->
                                           Cil_types.kernel_function ->
                                           Inout_type.t
                                       end->
  sig
    val non_terminating_inputs : Locations.Zone.t Pervasives.ref
    val non_terminating_outputs : Locations.Zone.t Pervasives.ref
    val store_non_terminating_inputs : Locations.Zone.t -> unit
    val store_non_terminating_outputs : Locations.Zone.t -> unit
    val store_non_terminating_subcall :
      Locations.Zone.t -> Operational_inputs.t -> unit
    val catenate :
      Operational_inputs.compute_t ->
      Operational_inputs.compute_t -> Operational_inputs.compute_t
    type t = Operational_inputs.compute_t
    val pretty : Format.formatter -> Operational_inputs.compute_t -> unit
    val bottom : Operational_inputs.compute_t
    val join_and_is_included :
      Operational_inputs.compute_t ->
      Operational_inputs.compute_t -> Operational_inputs.compute_t * bool
    val join :
      Operational_inputs.compute_t ->
      Operational_inputs.compute_t -> Operational_inputs.compute_t
    val is_included :
      Operational_inputs.compute_t -> Operational_inputs.compute_t -> bool
    val transfer_exp :
      Cil_types.stmt ->
      Cil_types.exp ->
      Operational_inputs.compute_t -> Operational_inputs.compute_t
    val add_out :
      Db.Value.state ->
      Cil_types.lval ->
      Locations.Zone.t ->
      Operational_inputs.compute_t -> Operational_inputs.compute_t
    val transfer_call :
      Cil_types.stmt ->
      Cil_types.lval option ->
      Cil_types.exp ->
      Cil_types.exp list ->
      '-> Operational_inputs.compute_t -> Operational_inputs.compute_t
    val transfer_instr :
      Cil_types.stmt ->
      Cil_types.instr ->
      Operational_inputs.Computer.t -> Operational_inputs.Computer.t
    val transfer_guard :
      Cil_types.stmt ->
      Cil_types.exp ->
      Operational_inputs.compute_t ->
      Operational_inputs.compute_t * Operational_inputs.compute_t
    val return_data : Operational_inputs.compute_t Pervasives.ref
    val transfer_stmt :
      Cil_types.stmt ->
      Operational_inputs.Computer.t ->
      (Cil_types.stmt * Operational_inputs.Computer.t) list
    val init : (Cil_types.stmt * Operational_inputs.compute_t) list
    val end_dataflow : unit -> Operational_inputs.Computer.t
  end