module type Model =sig
..end
val configure : Model.tuning
val datatype : string
val separation : unit -> Separation.clause list
module Chunk:Memory.Chunk
module Heap:Qed.Collection.S
with type t = Chunk.t
module Sigma:Memory.Sigma
with type chunk = Chunk.t and type domain = Heap.set
type
loc
typechunk =
Memory.Chunk.t
typesigma =
Sigma.t
typesegment =
loc Memory.rloc
type
state
val state : sigma -> state
val lookup : state -> Lang.F.term -> Memory.mval
Mvalue
.
Recognized Cil
patterns:
Mvar x,[Mindex 0]
is rendered as *x
when x
has a pointer typeMmem p,[Mfield f;...]
is rendered as p->f...
like in CilMmem p,[Mindex k;...]
is rendered as p[k]...
to catch Cil Mem(AddPI(p,k)),...
val updates : state Memory.sequence -> Lang.F.Vars.t -> Memory.update Bag.t
The result shall be exhaustive with respect to values that are printed as Memory.mval
values at post
label via the lookup
function.
Otherwise, those values would not be pretty-printed to the user.
val apply : (Lang.F.term -> Lang.F.term) -> state -> state
val iter : (Memory.mval -> Lang.F.term -> unit) -> state -> unit
val pretty : Format.formatter -> loc -> unit
val vars : loc -> Lang.F.Vars.t
val occurs : Lang.F.var -> loc -> bool
val null : loc
val literal : eid:int -> Cstring.cst -> loc
val cvar : Cil_types.varinfo -> loc
val pointer_loc : Lang.F.term -> loc
val pointer_val : loc -> Lang.F.term
val field : loc -> Cil_types.fieldinfo -> loc
val shift : loc -> Ctypes.c_object -> Lang.F.term -> loc
term
. The element of the array are of
the given c_object
type.val base_addr : loc -> loc
val block_length : sigma -> Ctypes.c_object -> loc -> Lang.F.term
val cast : Ctypes.c_object Memory.sequence -> loc -> loc
cast ty loc
the cast is done from ty.pre
to ty.post
val loc_of_int : Ctypes.c_object -> Lang.F.term -> loc
val int_of_loc : Ctypes.c_int -> loc -> Lang.F.term
val domain : Ctypes.c_object -> loc -> Heap.set
val load : sigma ->
Ctypes.c_object -> loc -> loc Memory.value
val copied : sigma Memory.sequence ->
Ctypes.c_object -> loc -> loc -> Lang.F.pred list
copied sigma ty loc1 loc2
returns a set of formula that express that
the content for an object ty
is the same in sigma.pre
at loc1
and
in sigma.post
at loc2
val stored : sigma Memory.sequence ->
Ctypes.c_object -> loc -> Lang.F.term -> Lang.F.pred list
copied sigma ty loc t
returns a set of formula that express that
sigma.pre
and sigma.post
are identical except for an object ty
at
location loc
which is represented by t
in sigma.post
.val assigned : sigma Memory.sequence ->
Ctypes.c_object -> loc Memory.sloc -> Lang.F.pred list
true
as if the all set of memory location was given)val is_null : loc -> Lang.F.pred
val loc_eq : loc -> loc -> Lang.F.pred
val loc_lt : loc -> loc -> Lang.F.pred
val loc_neq : loc -> loc -> Lang.F.pred
val loc_leq : loc -> loc -> Lang.F.pred
val loc_diff : Ctypes.c_object -> loc -> loc -> Lang.F.term
val valid : sigma -> Memory.acs -> segment -> Lang.F.pred
Memory.acs
) in the given memory state at the given
segment.val scope : sigma ->
Mcfg.scope -> Cil_types.varinfo list -> sigma * Lang.F.pred list
val global : sigma -> Lang.F.term -> Lang.F.pred
p
, assumes this pointer p
(when valid)
is allocated outside the function frame under analysis. This means
separated from the formals and locals of the function.val included : segment -> segment -> Lang.F.pred
val separated : segment -> segment -> Lang.F.pred