sig
  exception NotACType
  type ('value, 'shape) typ
  val of_ltyp : Cil_types.logic_type -> (unit, unit) typ
  val integer : (unit, unit) typ
  val real : (unit, unit) typ
  val of_ctyp : Cil_types.typ -> ('v, 'v) typ
  val void : ('v, 'v) typ
  val bool : ('v, 'v) typ
  val char : ('v, 'v) typ
  val schar : ('v, 'v) typ
  val uchar : ('v, 'v) typ
  val int : ('v, 'v) typ
  val unit : ('v, 'v) typ
  val short : ('v, 'v) typ
  val ushort : ('v, 'v) typ
  val long : ('v, 'v) typ
  val ulong : ('v, 'v) typ
  val longlong : ('v, 'v) typ
  val ulonglong : ('v, 'v) typ
  val float : ('v, 'v) typ
  val double : ('v, 'v) typ
  val longdouble : ('v, 'v) typ
  val ptr : ('v, 's) typ -> ('v, 'v) typ
  val array : ?size:int -> ('v, 's) typ -> ('v, 's list) typ
  val attribute :
    ('v, 's) typ -> string -> Cil_types.attrparam list -> ('v, 's) typ
  val const : ('v, 's) typ -> ('v, 's) typ
  val stdlib_generated : ('v, 's) typ -> ('v, 's) typ
  val cil_typ : ('v, 's) typ -> Cil_types.typ
  val cil_logic_type : ('v, 's) typ -> Cil_types.logic_type
  type const'
  type var'
  type lval'
  type exp'
  type init'
  type label
  type const = [ `const of Cil_builder.Exp.const' ]
  type var = [ `var of Cil_builder.Exp.var' ]
  type lval =
      [ `lval of Cil_builder.Exp.lval' | `var of Cil_builder.Exp.var' ]
  type exp =
      [ `const of Cil_builder.Exp.const'
      | `exp of Cil_builder.Exp.exp'
      | `lval of Cil_builder.Exp.lval'
      | `var of Cil_builder.Exp.var' ]
  type init =
      [ `const of Cil_builder.Exp.const'
      | `exp of Cil_builder.Exp.exp'
      | `init of Cil_builder.Exp.init'
      | `lval of Cil_builder.Exp.lval'
      | `var of Cil_builder.Exp.var' ]
  val pretty :
    Stdlib.Format.formatter ->
    [ `const of Cil_builder.Exp.const'
    | `exp of Cil_builder.Exp.exp'
    | `init of Cil_builder.Exp.init'
    | `lval of Cil_builder.Exp.lval'
    | `none
    | `var of Cil_builder.Exp.var' ] -> unit
  val none : [> `none ]
  val here : Cil_builder.Exp.label
  val old : Cil_builder.Exp.label
  val pre : Cil_builder.Exp.label
  val post : Cil_builder.Exp.label
  val loop_entry : Cil_builder.Exp.label
  val loop_current : Cil_builder.Exp.label
  val program_init : Cil_builder.Exp.label
  val of_constant : Cil_types.constant -> [> Cil_builder.Exp.const ]
  val of_int : int -> [> Cil_builder.Exp.const ]
  val of_integer : Integer.t -> [> Cil_builder.Exp.const ]
  val zero : [> Cil_builder.Exp.const ]
  val one : [> Cil_builder.Exp.const ]
  val var : Cil_types.varinfo -> [> Cil_builder.Exp.var ]
  val of_lval : Cil_types.lval -> [> Cil_builder.Exp.lval ]
  exception EmptyList
  val of_exp : Cil_types.exp -> [> Cil_builder.Exp.exp ]
  val of_exp_copy : Cil_types.exp -> [> Cil_builder.Exp.exp ]
  val unop :
    Cil_types.unop -> [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val neg : [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val lognot : [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val bwnot : [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val succ : [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val add_int : [< Cil_builder.Exp.exp ] -> int -> [> Cil_builder.Exp.exp ]
  val binop :
    Cil_types.binop ->
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val add :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val sub :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val mul :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val div :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val modulo :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val shiftl :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val shiftr :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val lt :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val gt :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val le :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ge :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val eq :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ne :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val logor :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val logand :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val logor_list : [< Cil_builder.Exp.exp ] list -> Cil_builder.Exp.exp
  val logand_list : [< Cil_builder.Exp.exp ] list -> Cil_builder.Exp.exp
  val bwand :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val bwor :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val bwxor :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val cast :
    ('v, 's) typ -> [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val cast' :
    Cil_types.typ -> [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val addr : [< Cil_builder.Exp.lval ] -> [> Cil_builder.Exp.exp ]
  val mem : [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.lval ]
  val index :
    [< Cil_builder.Exp.lval ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.lval ]
  val field :
    [< Cil_builder.Exp.lval ] ->
    Cil_types.fieldinfo -> [> Cil_builder.Exp.lval ]
  val fieldnamed :
    [< Cil_builder.Exp.lval ] -> string -> [> Cil_builder.Exp.lval ]
  val result : [> Cil_builder.Exp.lval ]
  val term : Cil_types.term -> [> Cil_builder.Exp.exp ]
  val range :
    [< `const of Cil_builder.Exp.const'
     | `exp of Cil_builder.Exp.exp'
     | `lval of Cil_builder.Exp.lval'
     | `none
     | `var of Cil_builder.Exp.var' ] ->
    [< `const of Cil_builder.Exp.const'
     | `exp of Cil_builder.Exp.exp'
     | `lval of Cil_builder.Exp.lval'
     | `none
     | `var of Cil_builder.Exp.var' ] ->
    [> Cil_builder.Exp.exp ]
  val whole : [> Cil_builder.Exp.exp ]
  val whole_right : [> Cil_builder.Exp.exp ]
  val app :
    Cil_types.logic_info ->
    Cil_builder.Exp.label list ->
    [< Cil_builder.Exp.exp ] list -> [> Cil_builder.Exp.exp ]
  val object_pointer :
    ?at:Cil_builder.Exp.label ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val valid :
    ?at:Cil_builder.Exp.label ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val valid_read :
    ?at:Cil_builder.Exp.label ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val initialized :
    ?at:Cil_builder.Exp.label ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val dangling :
    ?at:Cil_builder.Exp.label ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val allocable :
    ?at:Cil_builder.Exp.label ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val freeable :
    ?at:Cil_builder.Exp.label ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val fresh :
    Cil_builder.Exp.label ->
    Cil_builder.Exp.label ->
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val of_init : Cil_types.init -> [> Cil_builder.Exp.init ]
  val compound :
    Cil_types.typ -> Cil_builder.Exp.init list -> [> Cil_builder.Exp.init ]
  val values :
    (Cil_builder.Exp.init, 'values) typ -> 'values -> Cil_builder.Exp.init
  val ( + ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( - ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( * ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( / ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( % ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( << ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( >> ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( < ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( > ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( <= ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( >= ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( == ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( != ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  val ( -- ) :
    [< Cil_builder.Exp.exp ] ->
    [< Cil_builder.Exp.exp ] -> [> Cil_builder.Exp.exp ]
  exception LogicInC of Cil_builder.Exp.exp
  exception CInLogic of Cil_builder.Exp.exp
  exception NotATerm of Cil_builder.Exp.exp
  exception NotAPredicate of Cil_builder.Exp.exp
  exception NotAFunction of Cil_types.logic_info
  exception Typing_error of string
  val cil_logic_label : Cil_builder.Exp.label -> Cil_types.logic_label
  val cil_constant : [< Cil_builder.Exp.const ] -> Cil_types.constant
  val cil_varinfo : [< Cil_builder.Exp.var ] -> Cil_types.varinfo
  val cil_lval :
    loc:Cil_types.location -> [< Cil_builder.Exp.lval ] -> Cil_types.lval
  val cil_exp :
    loc:Cil_types.location -> [< Cil_builder.Exp.exp ] -> Cil_types.exp
  val cil_term_lval :
    loc:Cil_types.location ->
    ?restyp:Cil_types.typ -> [< Cil_builder.Exp.lval ] -> Cil_types.term_lval
  val cil_term :
    loc:Cil_types.location ->
    ?restyp:Cil_types.typ -> [< Cil_builder.Exp.exp ] -> Cil_types.term
  val cil_iterm :
    loc:Cil_types.location ->
    ?restyp:Cil_types.typ ->
    [< Cil_builder.Exp.exp ] -> Cil_types.identified_term
  val cil_pred :
    loc:Cil_types.location ->
    ?restyp:Cil_types.typ -> [< Cil_builder.Exp.exp ] -> Cil_types.predicate
  val cil_ipred :
    loc:Cil_types.location ->
    ?restyp:Cil_types.typ ->
    [< Cil_builder.Exp.exp ] -> Cil_types.identified_predicate
  val cil_init :
    loc:Cil_types.location -> [< Cil_builder.Exp.init ] -> Cil_types.init
  val cil_typeof : [< Cil_builder.Exp.var ] -> Cil_types.typ
end