module M:Wp.Sigs.Model
val configure : Wp.WpContext.tuning
Context
values.val configure_ia : Interpreted_automata.automaton -> Interpreted_automata.vertex Wp.Sigs.binder
StmtSemantics
.val datatype : string
val hypotheses : unit -> Wp.MemoryContext.clause list
module Chunk:Wp.Sigs.Chunk
module Heap:Qed.Collection.S
with type t = Chunk.t
module Sigma:Wp.Sigs.Sigma
with type chunk = Chunk.t and module Chunk = Heap
type
loc
typechunk =
Wp.Sigs.Chunk.t
typesigma =
Sigma.t
typedomain =
Sigma.domain
typesegment =
loc Wp.Sigs.rloc
type
state
val state : sigma -> state
val lookup : state -> Wp.Lang.F.term -> Wp.Sigs.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 Wp.Sigs.sequence ->
Wp.Lang.F.Vars.t -> Wp.Sigs.update Bag.t
The result shall be exhaustive with respect to values that are printed as Sigs.mval
values at post
label via the lookup
function.
Otherwise, those values would not be pretty-printed to the user.
val apply : (Wp.Lang.F.term -> Wp.Lang.F.term) ->
state -> state
val iter : (Wp.Sigs.mval -> Wp.Lang.F.term -> unit) -> state -> unit
val pretty : Format.formatter -> loc -> unit
val vars : loc -> Wp.Lang.F.Vars.t
val occurs : Wp.Lang.F.var -> loc -> bool
val null : loc
val literal : eid:int -> Wp.Cstring.cst -> loc
val cvar : Cil_types.varinfo -> loc
val pointer_loc : Wp.Lang.F.term -> loc
val pointer_val : loc -> Wp.Lang.F.term
val field : loc -> Cil_types.fieldinfo -> loc
val shift : loc ->
Wp.Ctypes.c_object -> Wp.Lang.F.term -> loc
term
. The element of the array are of
the given c_object
type.val base_addr : loc -> loc
val base_offset : loc -> Wp.Lang.F.term
val block_length : sigma ->
Wp.Ctypes.c_object -> loc -> Wp.Lang.F.term
val cast : Wp.Ctypes.c_object Wp.Sigs.sequence -> loc -> loc
cast ty loc
the cast is done from ty.pre
to ty.post
.
Might fail on memory models not supporting pointer casts.val loc_of_int : Wp.Ctypes.c_object -> Wp.Lang.F.term -> loc
val int_of_loc : Wp.Ctypes.c_int -> loc -> Wp.Lang.F.term
val domain : Wp.Ctypes.c_object -> loc -> domain
val load : sigma ->
Wp.Ctypes.c_object -> loc -> loc Wp.Sigs.value
val copied : sigma Wp.Sigs.sequence ->
Wp.Ctypes.c_object ->
loc -> loc -> Wp.Sigs.equation list
copied sigma ty loc1 loc2
returns a set of formula expressing that the
content for an object ty
is the same in sigma.pre
at loc1
and in
sigma.post
at loc2
.
val stored : sigma Wp.Sigs.sequence ->
Wp.Ctypes.c_object ->
loc -> Wp.Lang.F.term -> Wp.Sigs.equation list
copied sigma ty loc t
returns a set of formula expressing 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 Wp.Sigs.sequence ->
Wp.Ctypes.c_object -> loc Wp.Sigs.sloc -> Wp.Sigs.equation list
This function can over-approximate the set of given memory location (e.g
it can return true
as if the all set of memory location was given).
val is_null : loc -> Wp.Lang.F.pred
val loc_eq : loc -> loc -> Wp.Lang.F.pred
val loc_lt : loc -> loc -> Wp.Lang.F.pred
val loc_neq : loc -> loc -> Wp.Lang.F.pred
val loc_leq : loc -> loc -> Wp.Lang.F.pred
val loc_diff : Wp.Ctypes.c_object ->
loc -> loc -> Wp.Lang.F.term
val valid : sigma -> Wp.Sigs.acs -> segment -> Wp.Lang.F.pred
Wp.Sigs.acs
) in the given memory state at the given
segment.val frame : sigma -> Wp.Lang.F.pred list
val alloc : sigma -> Cil_types.varinfo list -> sigma
val invalid : sigma -> segment -> Wp.Lang.F.pred
val scope : sigma Wp.Sigs.sequence ->
Wp.Sigs.scope -> Cil_types.varinfo list -> Wp.Lang.F.pred list
val global : sigma -> Wp.Lang.F.term -> Wp.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 -> Wp.Lang.F.pred
val separated : segment -> segment -> Wp.Lang.F.pred