sig
  val compute_call_ref :
    (Cil_types.kernel_function ->
     recursive:bool ->
     call_kinstr:Cil_types.kinstr ->
     Cvalue.Model.t ->
     (Cil_types.exp * Cvalue.V_Offsetmap.t) list -> Value_types.call_result)
    Pervasives.ref
  val do_assign :
    with_alarms:CilE.warn_mode ->
    Cil_types.kernel_function ->
    Locals_scoping.clobbered_set ->
    Cvalue.Model.t -> Cil_types.lval -> Cil_types.exp -> Cvalue.Model.t
  val interp_call :
    with_alarms:CilE.warn_mode ->
    Locals_scoping.clobbered_set ->
    Cil_types.stmt ->
    Cil_types.lval option ->
    Cil_types.exp ->
    Cil_types.exp list ->
    Cvalue.Model.t -> Cvalue.Model.t list * Value_types.cacheable
  exception AlwaysOverlap
  val check_non_overlapping :
    Cvalue.Model.t -> Cil_types.lval list -> Cil_types.lval list -> unit
  val check_unspecified_sequence :
    Cvalue.Model.t ->
    (Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
     Cil_types.lval list * Cil_types.stmt Pervasives.ref list)
    list -> unit
  val externalize :
    with_alarms:CilE.warn_mode ->
    Cil_types.kernel_function ->
    return_lv:Cil_types.lval option ->
    Locals_scoping.clobbered_set ->
    Cvalue.Model.t -> Cvalue.V_Offsetmap.t option * Cvalue.Model.t
end