sig
  val equation : Sigs.equation -> Lang.F.pred
  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 -> 'Sigs.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 volatile : ?warn:string -> unit -> bool
  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) -> 'Sigs.sloc -> 'Sigs.sloc
  val map_value : ('-> 'b) -> 'Sigs.value -> 'Sigs.value
  val map_logic : ('-> 'b) -> 'Sigs.logic -> 'Sigs.logic
  val plain : Cil_types.logic_type -> Lang.F.term -> 'Sigs.logic
  type polarity = [ `Negative | `NoPolarity | `Positive ]
  val negate : Cvalues.polarity -> Cvalues.polarity
  module Logic :
    functor (M : Sigs.Model->
      sig
        type logic = M.loc Sigs.logic
        type segment = Ctypes.c_object * M.loc Sigs.sloc
        type region = M.loc Sigs.region
        val value : Cvalues.Logic.logic -> Lang.F.term
        val loc : Cvalues.Logic.logic -> M.loc
        val vset : Cvalues.Logic.logic -> Vset.set
        val region :
          Ctypes.c_object -> Cvalues.Logic.logic -> Cvalues.Logic.region
        val rdescr : M.loc Sigs.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
        val separated : Cvalues.Logic.region list -> Lang.F.pred
        val included :
          Cvalues.Logic.segment -> Cvalues.Logic.segment -> Lang.F.pred
        val valid :
          M.Sigma.t -> Sigs.acs -> Cvalues.Logic.segment -> Lang.F.pred
        val invalid : M.Sigma.t -> Cvalues.Logic.segment -> Lang.F.pred
      end
end