functor (M : Memory.Model) ->
sig
type loc = M.loc
type value = LogicSemantics.Make.loc Memory.value
type logic = LogicSemantics.Make.loc Memory.logic
type region = LogicSemantics.Make.loc Memory.sloc list
type sigma = M.Sigma.t
module L :
sig
type logic = M.loc Memory.logic
val value : logic -> Lang.F.term
val loc : logic -> M.loc
val vset : logic -> Vset.set
val sloc : logic -> M.loc Memory.sloc list
val rdescr :
M.loc Memory.sloc -> Lang.F.var list * M.loc * Lang.F.pred
val map : Lang.F.unop -> logic -> logic
val map_opp : logic -> logic
val map_loc : (M.loc -> M.loc) -> logic -> logic
val map_l2t : (M.loc -> Lang.F.term) -> logic -> logic
val map_t2l : (Lang.F.term -> M.loc) -> logic -> logic
val apply : Lang.F.binop -> logic -> logic -> logic
val apply_add : logic -> logic -> logic
val apply_sub : logic -> logic -> logic
val field : logic -> Cil_types.fieldinfo -> logic
val shift : logic -> Ctypes.c_object -> ?size:int -> logic -> logic
val load : M.Sigma.t -> Ctypes.c_object -> logic -> logic
val union : Cil_types.logic_type -> logic list -> logic
val inter : Cil_types.logic_type -> logic list -> logic
type region = M.loc Memory.sloc list
val separated : (Ctypes.c_object * region) list -> Lang.F.pred
val included :
Ctypes.c_object ->
region -> Ctypes.c_object -> region -> Lang.F.pred
val valid :
M.Sigma.t -> Memory.acs -> Ctypes.c_object -> region -> Lang.F.pred
end
module C :
sig
type value = M.loc Memory.value
type logic = M.loc Memory.logic
type sigma = M.Sigma.t
type chunk = M.Chunk.t
type frame = LogicCompiler.Make(M).frame
val pp_frame : Format.formatter -> frame -> unit
val frame : Cil_types.kernel_function -> frame
val frame_copy : frame -> frame
val call_pre :
Cil_types.kernel_function -> value list -> sigma -> frame
val call_post :
Cil_types.kernel_function ->
value list -> sigma Memory.sequence -> frame
val formal : Cil_types.varinfo -> value option
val return : unit -> Cil_types.typ
val result : unit -> Lang.F.var
val status : unit -> Lang.F.var
val trigger : Definitions.trigger -> unit
val guards : frame -> Lang.F.pred list
val mem_frame : Clabels.c_label -> sigma
val mem_at_frame : frame -> Clabels.c_label -> sigma
val in_frame : frame -> ('a -> 'b) -> 'a -> 'b
val get_frame : unit -> frame
type env = LogicCompiler.Make(M).env
val new_env : Cil_datatype.Logic_var.t list -> env
val move : env -> sigma -> env
val sigma : env -> sigma
val env_at : env -> Clabels.c_label -> env
val mem_at : env -> Clabels.c_label -> sigma
val env_let : env -> Cil_types.logic_var -> logic -> env
val env_letval : env -> Cil_types.logic_var -> value -> env
val term : env -> Cil_types.term -> Lang.F.term
val pred :
bool -> env -> Cil_types.predicate Cil_types.named -> Lang.F.pred
val logic : env -> Cil_types.term -> logic
val region : env -> Cil_types.term -> M.loc Memory.sloc list
val bootstrap_term : (env -> Cil_types.term -> Lang.F.term) -> unit
val bootstrap_pred :
(bool -> env -> Cil_types.predicate Cil_types.named -> Lang.F.pred) ->
unit
val bootstrap_logic : (env -> Cil_types.term -> logic) -> unit
val bootstrap_region :
(env -> Cil_types.term -> M.loc Memory.sloc list) -> unit
val call_fun :
env ->
Cil_types.logic_info ->
(Cil_types.logic_label * Cil_types.logic_label) list ->
Lang.F.term list -> Lang.F.term
val call_pred :
env ->
Cil_types.logic_info ->
(Cil_types.logic_label * Cil_types.logic_label) list ->
Lang.F.term list -> Lang.F.pred
val logic_var : env -> Cil_types.logic_var -> logic
val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
end
type frame = LogicSemantics.Make.C.frame
val pp_frame : Format.formatter -> LogicSemantics.Make.C.frame -> unit
val get_frame : unit -> LogicSemantics.Make.C.frame
val in_frame : LogicSemantics.Make.C.frame -> ('a -> 'b) -> 'a -> 'b
val mem_frame : Clabels.c_label -> LogicSemantics.Make.C.sigma
val mem_at_frame :
LogicSemantics.Make.C.frame ->
Clabels.c_label -> LogicSemantics.Make.C.sigma
val mem_at :
LogicSemantics.Make.C.env ->
Clabels.c_label -> LogicSemantics.Make.C.sigma
val frame : Cil_types.kernel_function -> LogicSemantics.Make.C.frame
val frame_copy :
LogicSemantics.Make.C.frame -> LogicSemantics.Make.C.frame
val call_pre :
Cil_types.kernel_function ->
LogicSemantics.Make.C.value list ->
LogicSemantics.Make.C.sigma -> LogicSemantics.Make.C.frame
val call_post :
Cil_types.kernel_function ->
LogicSemantics.Make.C.value list ->
LogicSemantics.Make.C.sigma Memory.sequence ->
LogicSemantics.Make.C.frame
val return : unit -> Cil_types.typ
val result : unit -> Lang.F.var
val status : unit -> Lang.F.var
val guards : LogicSemantics.Make.C.frame -> Lang.F.pred list
val pp_logic : Format.formatter -> M.loc Memory.logic -> unit
val pp_bound : Format.formatter -> Lang.F.term option -> unit
val pp_sloc : Format.formatter -> M.loc Memory.sloc -> unit
val pp_region : Format.formatter -> M.loc Memory.sloc list -> unit
type env = LogicSemantics.Make.C.env
val new_env : Cil_datatype.Logic_var.t list -> LogicSemantics.Make.C.env
val move :
LogicSemantics.Make.C.env ->
LogicSemantics.Make.C.sigma -> LogicSemantics.Make.C.env
val sigma : LogicSemantics.Make.C.env -> LogicSemantics.Make.C.sigma
val call : LogicSemantics.Make.C.sigma -> LogicSemantics.Make.C.env
val logic_of_value : 'a Memory.value -> 'a Memory.logic
val loc_of_term : LogicSemantics.Make.C.env -> Cil_types.term -> M.loc
val val_of_term :
LogicSemantics.Make.C.env -> Cil_types.term -> Lang.F.term
val set_of_term : LogicSemantics.Make.C.env -> Cil_types.term -> Vset.set
val collection_of_term :
LogicSemantics.Make.C.env ->
Cil_types.term -> LogicSemantics.Make.C.logic
val term : LogicSemantics.Make.C.env -> Cil_types.term -> Lang.F.term
val access_offset :
LogicSemantics.Make.C.env ->
LogicSemantics.Make.logic ->
Cil_types.term_offset -> LogicSemantics.Make.logic
val update_offset :
LogicSemantics.Make.C.env ->
Lang.F.term -> Cil_types.term_offset -> Lang.F.term -> Lang.F.term
val shift_offset :
LogicSemantics.Make.C.env ->
Cil_types.typ ->
LogicSemantics.Make.logic ->
Cil_types.term_offset -> Cil_types.typ * LogicSemantics.Make.logic
type lv_value =
VAL of LogicSemantics.Make.logic
| VAR of Cil_types.varinfo
val logic_var :
LogicSemantics.Make.C.env ->
Cil_types.logic_var -> LogicSemantics.Make.lv_value
val load_loc :
LogicSemantics.Make.C.env ->
Cil_types.typ ->
LogicSemantics.Make.loc ->
Cil_types.term_offset -> LogicSemantics.Make.L.logic
val term_lval :
LogicSemantics.Make.C.env ->
Cil_types.term_lhost * Cil_types.term_offset ->
LogicSemantics.Make.logic
val addr_lval :
LogicSemantics.Make.C.env ->
Cil_types.term_lhost * Cil_types.term_offset ->
LogicSemantics.Make.logic
val term_unop :
Cil_types.unop ->
LogicSemantics.Make.L.logic -> LogicSemantics.Make.L.logic
type eqsort =
EQ_set
| EQ_loc
| EQ_plain
| EQ_array of Matrix.matrix
| EQ_comp of Cil_types.compinfo
| EQ_incomparable
val eqsort_of_type : Cil_types.logic_type -> LogicSemantics.Make.eqsort
val eqsort_of_comparison :
Cil_types.term -> Cil_types.term -> LogicSemantics.Make.eqsort
val use_equal : bool -> bool
val term_equal :
bool ->
LogicSemantics.Make.C.env ->
Cil_types.term -> Cil_types.term -> Lang.F.pred
val term_diff :
bool ->
LogicSemantics.Make.C.env ->
Cil_types.term -> Cil_types.term -> Lang.F.pred
val compare_term :
LogicSemantics.Make.C.env ->
(Lang.F.term -> Lang.F.term -> 'a) ->
(M.loc -> M.loc -> 'a) -> Cil_types.term -> Cil_types.term -> 'a
val exp_equal :
LogicSemantics.Make.C.env ->
Cil_types.term -> Cil_types.term -> 'a Memory.logic
val exp_diff :
LogicSemantics.Make.C.env ->
Cil_types.term -> Cil_types.term -> 'a Memory.logic
val exp_compare :
LogicSemantics.Make.C.env ->
(Lang.F.term -> Lang.F.term -> Lang.F.pred) ->
(M.loc -> M.loc -> Lang.F.pred) ->
Cil_types.term -> Cil_types.term -> 'a Memory.logic
val toreal :
bool -> LogicSemantics.Make.L.logic -> LogicSemantics.Make.L.logic
val arith :
LogicSemantics.Make.C.env ->
(LogicSemantics.Make.C.logic -> LogicSemantics.Make.C.logic -> 'a) ->
(LogicSemantics.Make.L.logic -> LogicSemantics.Make.L.logic -> 'a) ->
Cil_types.term -> Cil_types.term -> 'a
val term_binop :
LogicSemantics.Make.C.env ->
Cil_types.binop ->
Cil_types.term -> Cil_types.term -> LogicSemantics.Make.L.logic
type cvsort =
L_real
| L_integer
| L_cint of Ctypes.c_int
| L_cfloat of Ctypes.c_float
| L_pointer of Cil_types.typ
val cvsort_of_type : Cil_types.logic_type -> LogicSemantics.Make.cvsort
val term_cast :
LogicSemantics.Make.C.env ->
Cil_types.typ -> Cil_types.term -> LogicSemantics.Make.C.logic
val bind_quantifiers :
LogicSemantics.Make.env ->
Cil_types.logic_var list ->
Lang.F.var list * LogicSemantics.Make.C.env * Lang.F.pred list
val term_node :
LogicSemantics.Make.env -> Cil_types.term -> LogicSemantics.Make.logic
val separated_terms :
LogicSemantics.Make.C.env -> Cil_types.term list -> Lang.F.pred
val relation :
bool ->
LogicSemantics.Make.C.env ->
Cil_types.relation -> Cil_types.term -> Cil_types.term -> Lang.F.pred
val valid :
C.env ->
Memory.acs -> Cil_types.logic_label -> Cil_types.term -> Lang.F.pred
val predicate :
bool ->
LogicSemantics.Make.C.env ->
Cil_types.predicate Cil_types.named -> Lang.F.pred
val assignable_lval :
LogicSemantics.Make.C.env ->
Cil_types.term_lhost * Cil_types.term_offset -> M.loc Memory.sloc list
val assignable :
LogicSemantics.Make.C.env -> Cil_types.term -> M.loc Memory.sloc list
val term_trigger :
LogicSemantics.Make.env -> Cil_types.term -> LogicSemantics.Make.logic
val pred_trigger :
bool ->
LogicSemantics.Make.C.env ->
Cil_types.predicate Cil_types.named -> Lang.F.pred
val pred :
positive:bool ->
LogicSemantics.Make.C.env ->
Cil_types.predicate Cil_types.named -> Lang.F.pred
val logic :
LogicSemantics.Make.env -> Cil_types.term -> LogicSemantics.Make.logic
val region :
LogicSemantics.Make.C.env -> Cil_types.term -> M.loc Memory.sloc list
val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
val assigns_from :
LogicSemantics.Make.C.env ->
(Cil_types.identified_term * 'a) list ->
(Ctypes.c_object * M.loc Memory.sloc list) list
val assigns :
LogicSemantics.Make.C.env ->
Cil_types.identified_term Cil_types.assigns ->
(Ctypes.c_object * M.loc Memory.sloc list) list option
val valid :
M.Sigma.t ->
Memory.acs ->
Ctypes.c_object -> LogicSemantics.Make.L.region -> Lang.F.pred
val included :
Ctypes.c_object ->
LogicSemantics.Make.L.region ->
Ctypes.c_object -> LogicSemantics.Make.L.region -> Lang.F.pred
val separated :
(Ctypes.c_object * LogicSemantics.Make.L.region) list -> Lang.F.pred
val occurs_opt : Lang.F.var -> Lang.F.term option -> bool
val occurs_sloc : Lang.F.var -> M.loc Memory.sloc -> bool
val occurs : Lang.F.var -> M.loc Memory.sloc list -> bool
val vars_opt : Lang.F.term option -> Lang.F.Vars.t
val vars_sloc : M.loc Memory.sloc -> Lang.F.Vars.t
val vars : M.loc Memory.sloc list -> Lang.F.Vars.t
end