sig   type value = Main_values.CVal.t   type location = Main_locations.PLoc.location   val find_right_value :     Cil_types.typ ->     Cvalue.V_Offsetmap.t -> Cvalue_transfer.value Eval.flagged_value   module Transfer :     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 end