sig
module type Code =
sig
type loc
val equal_obj :
Ctypes.c_object ->
LogicAssigns.Code.loc Memory.value ->
LogicAssigns.Code.loc Memory.value -> Lang.F.pred
end
module type Logic =
sig
type loc
val vars : LogicAssigns.Logic.loc Memory.sloc list -> Lang.F.Vars.t
val pp_logic :
Format.formatter -> LogicAssigns.Logic.loc Memory.logic -> unit
val pp_sloc :
Format.formatter -> LogicAssigns.Logic.loc Memory.sloc -> unit
val pp_region :
Format.formatter -> LogicAssigns.Logic.loc Memory.sloc list -> unit
end
module Make :
functor
(M : Memory.Model) (C : sig
type loc = M.loc
val equal_obj :
Ctypes.c_object ->
loc Memory.value ->
loc Memory.value -> Lang.F.pred
end) (L : sig
type loc = M.loc
val vars :
loc Memory.sloc list ->
Lang.F.Vars.t
val pp_logic :
Format.formatter ->
loc Memory.logic -> unit
val pp_sloc :
Format.formatter ->
loc Memory.sloc -> unit
val pp_region :
Format.formatter ->
loc Memory.sloc list -> unit
end) ->
sig
type region = (Ctypes.c_object * M.loc Memory.sloc list) list
val vars : LogicAssigns.Make.region -> Lang.F.Vars.t
val domain : LogicAssigns.Make.region -> M.Heap.set
val assigned :
M.sigma Memory.sequence ->
LogicAssigns.Make.region -> Lang.F.pred list
end
end