sig
  val add_retres_to_state :
    Cil_types.kernel_function ->
    Cvalue.V_Offsetmap.t ->
    Cvalue.Model.t -> Cil_types.varinfo * Cvalue.Model.t
  val returned_value :
    Cil_types.kernel_function ->
    Cvalue.Model.t -> Cvalue.V.t * Cvalue.Model.t
end