sig
type polarity = [ `Negative | `NoPolarity | `Positive ]
module Make :
functor (M : Memory.Model) ->
sig
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
val pp_logic : Format.formatter -> LogicSemantics.Make.logic -> unit
val pp_sloc :
Format.formatter -> LogicSemantics.Make.loc Memory.sloc -> unit
val pp_region :
Format.formatter -> LogicSemantics.Make.region -> unit
type call
type frame
val pp_frame : Format.formatter -> LogicSemantics.Make.frame -> unit
val get_frame : unit -> LogicSemantics.Make.frame
val in_frame : LogicSemantics.Make.frame -> ('a -> 'b) -> 'a -> 'b
val mem_frame : Clabels.c_label -> LogicSemantics.Make.sigma
val mem_at_frame :
LogicSemantics.Make.frame ->
Clabels.c_label -> LogicSemantics.Make.sigma
val call :
Cil_types.kernel_function ->
LogicSemantics.Make.value list -> LogicSemantics.Make.call
val frame : Cil_types.kernel_function -> LogicSemantics.Make.frame
val call_pre :
LogicSemantics.Make.sigma ->
LogicSemantics.Make.call ->
LogicSemantics.Make.sigma -> LogicSemantics.Make.frame
val call_post :
LogicSemantics.Make.sigma ->
LogicSemantics.Make.call ->
LogicSemantics.Make.sigma Memory.sequence ->
LogicSemantics.Make.frame
val return : unit -> Cil_types.typ
val result : unit -> Lang.F.var
val status : unit -> Lang.F.var
val guards : LogicSemantics.Make.frame -> Lang.F.pred list
type env
val new_env : Cil_types.logic_var list -> LogicSemantics.Make.env
val move :
LogicSemantics.Make.env ->
LogicSemantics.Make.sigma -> LogicSemantics.Make.env
val sigma : LogicSemantics.Make.env -> LogicSemantics.Make.sigma
val mem_at :
LogicSemantics.Make.env ->
Clabels.c_label -> LogicSemantics.Make.sigma
val call_env : LogicSemantics.Make.sigma -> LogicSemantics.Make.env
val term : LogicSemantics.Make.env -> Cil_types.term -> Lang.F.term
val pred :
LogicSemantics.polarity ->
LogicSemantics.Make.env -> Cil_types.predicate -> Lang.F.pred
val region :
LogicSemantics.Make.env ->
Cil_types.term -> LogicSemantics.Make.region
val assigns :
LogicSemantics.Make.env ->
Cil_types.assigns ->
(Ctypes.c_object * LogicSemantics.Make.region) list option
val assigns_from :
LogicSemantics.Make.env ->
Cil_types.from list ->
(Ctypes.c_object * LogicSemantics.Make.region) list
val val_of_term :
LogicSemantics.Make.env -> Cil_types.term -> Lang.F.term
val loc_of_term :
LogicSemantics.Make.env ->
Cil_types.term -> LogicSemantics.Make.loc
val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
val vars : LogicSemantics.Make.region -> Lang.F.Vars.t
val occurs : Lang.F.var -> LogicSemantics.Make.region -> bool
val valid :
LogicSemantics.Make.sigma ->
Memory.acs ->
Ctypes.c_object -> LogicSemantics.Make.region -> Lang.F.pred
val included :
Ctypes.c_object ->
LogicSemantics.Make.region ->
Ctypes.c_object -> LogicSemantics.Make.region -> Lang.F.pred
val separated :
(Ctypes.c_object * LogicSemantics.Make.region) list -> Lang.F.pred
end
end