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_callees_inputs : Locations.Zone.t Pervasives.ref
    val non_terminating_callees_outputs : Locations.Zone.t Pervasives.ref
    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 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.Computer.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 :
      Operational_inputs.compute_t array -> Operational_inputs.tt
  end