Functor LogicSemantics.Make

module Make: 
functor (M : Memory.Model) -> sig .. end
Parameters:
M : Memory.Model

type loc = M.loc 
type sigma = M.Sigma.t 
type value = M.loc Memory.value 
type logic = M.loc Memory.logic 
type region = M.loc Memory.sloc list 

Debug


val pp_logic : Format.formatter -> logic -> unit
val pp_sloc : Format.formatter -> loc Memory.sloc -> unit
val pp_region : Format.formatter -> region -> unit

Frames


type call 
type frame 
val pp_frame : Format.formatter -> frame -> unit
val get_frame : unit -> frame
val in_frame : frame -> ('a -> 'b) -> 'a -> 'b
val mem_frame : Clabels.c_label -> sigma
val mem_at_frame : frame -> Clabels.c_label -> sigma
val call : Cil_types.kernel_function ->
value list -> call
val frame : Cil_types.kernel_function -> frame
val call_pre : sigma ->
call ->
sigma -> frame
val call_post : sigma ->
call ->
sigma Memory.sequence -> frame
val return : unit -> Cil_types.typ
val result : unit -> Lang.F.var
val status : unit -> Lang.F.var
val guards : frame -> Lang.F.pred list

Traductions


type env 
val new_env : Cil_types.logic_var list -> env
val move : env ->
sigma -> env
val sigma : env -> sigma
val mem_at : env -> Clabels.c_label -> sigma
val call_env : sigma -> env
val term : env -> Cil_types.term -> Lang.F.term
val pred : positive:bool ->
env -> Cil_types.predicate Cil_types.named -> Lang.F.pred
val region : env -> Cil_types.term -> region
val assigns : env ->
Cil_types.identified_term Cil_types.assigns ->
(Ctypes.c_object * region) list option
val assigns_from : env ->
Cil_types.identified_term Cil_types.from list ->
(Ctypes.c_object * region) list
val val_of_term : env -> Cil_types.term -> Lang.F.term
val loc_of_term : env -> Cil_types.term -> loc
val lemma : LogicUsage.logic_lemma -> Definitions.dlemma

Regions


val vars : region -> Lang.F.Vars.t
val occurs : Lang.F.var -> region -> bool
val valid : sigma ->
Memory.acs -> Ctypes.c_object -> region -> Lang.F.pred
val included : Ctypes.c_object ->
region ->
Ctypes.c_object -> region -> Lang.F.pred
val separated : (Ctypes.c_object * region) list -> Lang.F.pred