sig   val bool_val : Lang.F.unop   val bool_eq : Lang.F.binop   val bool_lt : Lang.F.binop   val bool_neq : Lang.F.binop   val bool_leq : Lang.F.binop   val bool_and : Lang.F.binop   val bool_or : Lang.F.binop   val is_true : Lang.F.pred -> Lang.F.term   val is_false : Lang.F.pred -> Lang.F.term   val null : (Lang.F.term -> Lang.F.pred) Context.value   val is_null : Ctypes.c_object -> Lang.F.term -> Lang.F.pred   val is_object : Ctypes.c_object -> 'Memory.value -> Lang.F.pred   val has_ctype : Cil_types.typ -> Lang.F.term -> Lang.F.pred   val has_ltype : Cil_types.logic_type -> Lang.F.term -> Lang.F.pred   val cdomain : Cil_types.typ -> (Lang.F.term -> Lang.F.pred) option   val ldomain : Cil_types.logic_type -> (Lang.F.term -> Lang.F.pred) option   val equal_object :     Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred   val equal_comp :     Cil_types.compinfo -> Lang.F.term -> Lang.F.term -> Lang.F.pred   val equal_array :     Matrix.matrix -> Lang.F.term -> Lang.F.term -> Lang.F.pred   val ainf : Lang.F.term option   val asup : int -> Lang.F.term option   val constant : Cil_types.constant -> Lang.F.term   val logic_constant : Cil_types.logic_constant -> Lang.F.term   val constant_exp : Cil_types.exp -> Lang.F.term   val constant_term : Cil_types.term -> Lang.F.term   val map_sloc : ('-> 'b) -> 'Memory.sloc -> 'Memory.sloc   val map_value : ('-> 'b) -> 'Memory.value -> 'Memory.value   val map_logic : ('-> 'b) -> 'Memory.logic -> 'Memory.logic   val plain : Cil_types.logic_type -> Lang.F.term -> 'Memory.logic   type polarity = [ `Negative | `NoPolarity | `Positive ]   val negate : Cvalues.polarity -> Cvalues.polarity   module Logic :     functor (M : Memory.Model->       sig         type logic = M.loc Memory.logic         val value : Cvalues.Logic.logic -> Lang.F.term         val loc : Cvalues.Logic.logic -> M.loc         val vset : Cvalues.Logic.logic -> Vset.set         val sloc : Cvalues.Logic.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 -> Cvalues.Logic.logic -> Cvalues.Logic.logic         val map_opp : Cvalues.Logic.logic -> Cvalues.Logic.logic         val map_loc :           (M.loc -> M.loc) -> Cvalues.Logic.logic -> Cvalues.Logic.logic         val map_l2t :           (M.loc -> Lang.F.term) ->           Cvalues.Logic.logic -> Cvalues.Logic.logic         val map_t2l :           (Lang.F.term -> M.loc) ->           Cvalues.Logic.logic -> Cvalues.Logic.logic         val apply :           Lang.F.binop ->           Cvalues.Logic.logic -> Cvalues.Logic.logic -> Cvalues.Logic.logic         val apply_add :           Cvalues.Logic.logic -> Cvalues.Logic.logic -> Cvalues.Logic.logic         val apply_sub :           Cvalues.Logic.logic -> Cvalues.Logic.logic -> Cvalues.Logic.logic         val field :           Cvalues.Logic.logic -> Cil_types.fieldinfo -> Cvalues.Logic.logic         val shift :           Cvalues.Logic.logic ->           Ctypes.c_object ->           ?size:int -> Cvalues.Logic.logic -> Cvalues.Logic.logic         val load :           M.Sigma.t ->           Ctypes.c_object -> Cvalues.Logic.logic -> Cvalues.Logic.logic         val union :           Cil_types.logic_type ->           Cvalues.Logic.logic list -> Cvalues.Logic.logic         val inter :           Cil_types.logic_type ->           Cvalues.Logic.logic list -> Cvalues.Logic.logic         val subset :           Cil_types.logic_type ->           Cvalues.Logic.logic ->           Cil_types.logic_type -> Cvalues.Logic.logic -> Lang.F.pred         type region = M.loc Memory.sloc list         val separated :           (Ctypes.c_object * Cvalues.Logic.region) list -> Lang.F.pred         val included :           Ctypes.c_object ->           Cvalues.Logic.region ->           Ctypes.c_object -> Cvalues.Logic.region -> Lang.F.pred         val valid :           M.Sigma.t ->           Memory.acs ->           Ctypes.c_object -> Cvalues.Logic.region -> Lang.F.pred       end end