Module CfgWP.VC.L

module L: LogicSemantics.Make(M)

type loc = M.loc 
type value = loc Memory.value 
type logic = loc Memory.logic 
type region = loc Memory.sloc list 
type sigma = M.Sigma.t 
module L: Cvalues.Logic(M)
module C: LogicCompiler.Make(M)
type frame = C.frame 
val pp_frame : Format.formatter -> C.frame -> unit
val get_frame : unit -> C.frame
val in_frame : C.frame -> ('a -> 'b) -> 'a -> 'b
val mem_frame : Clabels.c_label -> C.sigma
val mem_at_frame : C.frame -> Clabels.c_label -> C.sigma
val mem_at : C.env -> Clabels.c_label -> C.sigma
val frame : Cil_types.kernel_function -> C.frame
val frame_copy : C.frame -> C.frame
val call_pre : Cil_types.kernel_function ->
C.value list ->
C.sigma -> C.frame
val call_post : Cil_types.kernel_function ->
C.value list ->
C.sigma Memory.sequence -> C.frame
val return : unit -> Cil_types.typ
val result : unit -> Lang.F.var
val status : unit -> Lang.F.var
val guards : 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 = C.env 
val new_env : Cil_datatype.Logic_var.t list -> C.env
val move : C.env ->
C.sigma -> C.env
val sigma : C.env -> C.sigma
val call : C.sigma -> C.env
val logic_of_value : 'a Memory.value -> 'a Memory.logic
val loc_of_term : C.env -> Cil_types.term -> M.loc
val val_of_term : C.env -> Cil_types.term -> Lang.F.term
val set_of_term : C.env -> Cil_types.term -> Vset.set
val collection_of_term : C.env -> Cil_types.term -> C.logic
val term : C.env -> Cil_types.term -> Lang.F.term
val access_offset : C.env ->
logic ->
Cil_types.term_offset -> logic
val update_offset : C.env ->
Lang.F.term -> Cil_types.term_offset -> Lang.F.term -> Lang.F.term
val shift_offset : C.env ->
Cil_types.typ ->
logic ->
Cil_types.term_offset -> Cil_types.typ * logic
type lv_value = 
| VAL of logic
| VAR of Cil_types.varinfo
val logic_var : C.env ->
Cil_types.logic_var -> lv_value
val load_loc : C.env ->
Cil_types.typ ->
loc ->
Cil_types.term_offset -> L.logic
val term_lval : C.env ->
Cil_types.term_lhost * Cil_types.term_offset -> logic
val addr_lval : C.env ->
Cil_types.term_lhost * Cil_types.term_offset -> logic
val term_unop : Cil_types.unop -> L.logic -> 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 -> eqsort
val eqsort_of_comparison : Cil_types.term -> Cil_types.term -> eqsort
val use_equal : bool -> bool
val term_equal : bool ->
C.env -> Cil_types.term -> Cil_types.term -> Lang.F.pred
val term_diff : bool ->
C.env -> Cil_types.term -> Cil_types.term -> Lang.F.pred
val compare_term : C.env ->
(Lang.F.term -> Lang.F.term -> 'a) ->
(M.loc -> M.loc -> 'a) -> Cil_types.term -> Cil_types.term -> 'a
val exp_equal : C.env ->
Cil_types.term -> Cil_types.term -> 'a Memory.logic
val exp_diff : C.env ->
Cil_types.term -> Cil_types.term -> 'a Memory.logic
val exp_compare : 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 -> L.logic -> L.logic
val arith : C.env ->
(C.logic -> C.logic -> 'a) ->
(L.logic -> L.logic -> 'a) ->
Cil_types.term -> Cil_types.term -> 'a
val term_binop : C.env ->
Cil_types.binop ->
Cil_types.term -> Cil_types.term -> 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 -> cvsort
val term_cast : C.env ->
Cil_types.typ -> Cil_types.term -> C.logic
val bind_quantifiers : env ->
Cil_types.logic_var list ->
Lang.F.var list * C.env * Lang.F.pred list
val term_node : env -> Cil_types.term -> logic
val separated_terms : C.env -> Cil_types.term list -> Lang.F.pred
val relation : bool ->
C.env ->
Cil_types.relation -> Cil_types.term -> Cil_types.term -> Lang.F.pred
val valid : M.Sigma.t ->
Memory.acs -> Ctypes.c_object -> L.region -> Lang.F.pred
val predicate : bool ->
C.env ->
Cil_types.predicate Cil_types.named -> Lang.F.pred
val assignable_lval : C.env ->
Cil_types.term_lhost * Cil_types.term_offset -> M.loc Memory.sloc list
val assignable : C.env -> Cil_types.term -> M.loc Memory.sloc list
val term_trigger : env -> Cil_types.term -> logic
val pred_trigger : bool ->
C.env ->
Cil_types.predicate Cil_types.named -> Lang.F.pred
val pred : positive:bool ->
C.env ->
Cil_types.predicate Cil_types.named -> Lang.F.pred
val logic : env -> Cil_types.term -> logic
val region : C.env -> Cil_types.term -> M.loc Memory.sloc list
val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
val assigns_from : C.env ->
(Cil_types.identified_term * 'a) list ->
(Ctypes.c_object * M.loc Memory.sloc list) list
val assigns : 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 -> L.region -> Lang.F.pred
val included : Ctypes.c_object ->
L.region ->
Ctypes.c_object -> L.region -> Lang.F.pred
val separated : (Ctypes.c_object * 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