module Make:
Definitions
type
value = M.loc Wp.Sigs.value
type
logic = M.loc Wp.Sigs.logic
type
result = M.loc Wp.Sigs.result
type
sigma = M.Sigma.t
type
chunk = M.Chunk.t
Frames
type
call
type
frame
val pp_frame : Stdlib.Format.formatter -> frame -> unit
val local : descr:string -> frame
val frame : Cil_types.kernel_function -> frame
val call : ?result:M.loc ->
Cil_types.kernel_function ->
value list -> call
val call_pre : sigma ->
call ->
sigma -> frame
val call_post : sigma ->
call ->
sigma Wp.Sigs.sequence -> frame
val mk_frame : ?kf:Cil_types.kernel_function ->
?result:result ->
?status:Wp.Lang.F.var ->
?formals:value Cil_datatype.Varinfo.Map.t ->
?labels:sigma Wp.Clabels.LabelMap.t ->
?descr:string -> unit -> frame
val formal : Cil_types.varinfo -> value option
val return : unit -> Cil_types.typ
val result : unit -> result
val status : unit -> Wp.Lang.F.var
val trigger : Wp.Definitions.trigger -> unit
val guards : frame -> Wp.Lang.F.pred list
val mem_frame : Wp.Clabels.c_label -> sigma
val has_at_frame : frame -> Wp.Clabels.c_label -> bool
val mem_at_frame : frame ->
Wp.Clabels.c_label -> sigma
val set_at_frame : frame ->
Wp.Clabels.c_label -> sigma -> unit
val in_frame : frame -> ('a -> 'b) -> 'a -> 'b
val get_frame : unit -> frame
Environment
type
env
val mk_env : ?here:sigma ->
?lvars:Cil_datatype.Logic_var.t list -> unit -> env
val current : env -> sigma
val move_at : env ->
sigma -> env
val env_at : env -> Wp.Clabels.c_label -> env
val mem_at : env ->
Wp.Clabels.c_label -> sigma
val env_let : env ->
Cil_types.logic_var ->
logic -> env
val env_letp : env ->
Cil_types.logic_var -> Wp.Lang.F.pred -> env
val env_letval : env ->
Cil_types.logic_var ->
value -> env
Compiler
val term : env -> Cil_types.term -> Wp.Lang.F.term
val pred : Wp.LogicCompiler.polarity ->
env -> Cil_types.predicate -> Wp.Lang.F.pred
val logic : env -> Cil_types.term -> logic
val region : env ->
unfold:bool -> Cil_types.term -> M.loc Wp.Sigs.region
When ~unfold:true
, decompose compound regions field by field
val bootstrap_term : (env -> Cil_types.term -> Wp.Lang.F.term) -> unit
val bootstrap_pred : (Wp.LogicCompiler.polarity ->
env -> Cil_types.predicate -> Wp.Lang.F.pred) ->
unit
val bootstrap_logic : (env -> Cil_types.term -> logic) ->
unit
val bootstrap_region : (env ->
unfold:bool -> Cil_types.term -> M.loc Wp.Sigs.region) ->
unit
Application
val call_fun : env ->
Wp.Lang.F.tau ->
Cil_types.logic_info ->
Cil_types.logic_label list -> Wp.Lang.F.term list -> Wp.Lang.F.term
val call_pred : env ->
Cil_types.logic_info ->
Cil_types.logic_label list -> Wp.Lang.F.term list -> Wp.Lang.F.pred
Logic Variable and ACSL Constants
val logic_var : env ->
Cil_types.logic_var -> logic
val logic_info : env -> Cil_types.logic_info -> Wp.Lang.F.pred option
val has_ltype : Cil_types.logic_type -> Wp.Lang.F.term -> Wp.Lang.F.pred
Logic Lemmas
val lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma