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