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