module Make: functor (
M
:
Memory.Model
) ->
functor (
C
:
Code
with type loc = M.loc
) ->
functor (
L
:
Logic
with type loc = M.loc
) ->
sig
.. end
Parameters: |
M |
: |
Memory.Model
|
C |
: |
Code with type loc = M.loc
|
L |
: |
Logic with type loc = M.loc
|
|
module Hmap: M.Heap.Map
module Dom: M.Heap.Set
type
region = (Ctypes.c_object * M.loc Memory.sloc list) list
val vars : region -> Lang.F.Vars.t
val dsloc : Ctypes.c_object -> M.loc Memory.sloc -> M.Heap.set
val domain : region -> Dom.t
val assigned_seq : Lang.F.pred Bag.t ->
M.sigma Memory.sequence ->
(Ctypes.c_object * M.loc Memory.sloc) list -> Lang.F.pred Bag.t
val assigned : M.sigma Memory.sequence -> region -> Lang.F.pred list