functor   (Valuation : sig                  type t                  type value = value                  type origin = bool                  type loc = location                  val find :                    t ->                    Cil_types.exp ->                    (value, origin) Eval.record_val Eval.or_top                  val fold :                    (Cil_types.exp ->                     (value, origin) Eval.record_val -> '-> 'a) ->                    t -> '-> 'a                  val find_loc :                    t -> Cil_types.lval -> loc Eval.record_loc Eval.or_top                end->   sig     type state = Cvalue.Model.t     type return = Cvalue.V_Offsetmap.t option     val update : Valuation.t -> state -> state     val assign :       Cil_types.kinstr ->       location Eval.left_value ->       Cil_types.exp ->       value Eval.assigned -> Valuation.t -> state -> state Eval.or_bottom     val assume :       Cil_types.stmt ->       Cil_types.exp -> bool -> Valuation.t -> state -> state Eval.or_bottom     val finalize_call :       Cil_types.stmt ->       value Eval.call -> pre:state -> post:state -> state Eval.or_bottom     val make_return :       Cil_types.kernel_function ->       Cil_types.stmt -> value Eval.assigned -> Valuation.t -> state -> return     val assign_return :       Cil_types.stmt ->       location Eval.left_value ->       Cil_types.kernel_function ->       return ->       value Eval.assigned -> Valuation.t -> state -> state Eval.or_bottom     val default_call :       Cil_types.stmt ->       value Eval.call -> state -> (state, return, value) Eval.call_result     val enter_loop : Cil_types.stmt -> state -> state     val incr_loop_counter : Cil_types.stmt -> state -> state     val leave_loop : Cil_types.stmt -> state -> state     val start_call :       Cil_types.stmt ->       Cvalue_transfer.value Eval.call ->       Valuation.t ->       state ->       (state, return, Cvalue_transfer.value) Eval.call_action *       Base.SetLattice.t   end