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 const' ]
  type var = [ `var of var' ]
  type lval = [ `lval of lval' | `var of var' ]
  type exp =
      [ `const of const' | `exp of exp' | `lval of lval' | `var of var' ]
  type init =
      [ `const of const'
      | `exp of exp'
      | `init of init'
      | `lval of lval'
      | `var of var' ]
  val pretty :
    Format.formatter ->
    [ `const of const'
    | `exp of exp'
    | `init of init'
    | `lval of lval'
    | `none
    | `var of var' ] -> unit
  val none : [> `none ]
  val here : label
  val old : label
  val pre : label
  val post : label
  val loop_entry : label
  val loop_current : label
  val program_init : label
  val of_constant : Cil_types.constant -> [> const ]
  val of_int : int -> [> const ]
  val of_integer : Integer.t -> [> const ]
  val zero : [> const ]
  val one : [> const ]
  val var : Cil_types.varinfo -> [> var ]
  val of_lval : Cil_types.lval -> [> lval ]
  exception EmptyList
  val of_exp : Cil_types.exp -> [> exp ]
  val of_exp_copy : Cil_types.exp -> [> exp ]
  val unop : Cil_types.unop -> [< exp ] -> [> exp ]
  val neg : [< exp ] -> [> exp ]
  val lognot : [< exp ] -> [> exp ]
  val bwnot : [< exp ] -> [> exp ]
  val succ : [< exp ] -> [> exp ]
  val add_int : [< exp ] -> int -> [> exp ]
  val binop : Cil_types.binop -> [< exp ] -> [< exp ] -> [> exp ]
  val add : [< exp ] -> [< exp ] -> [> exp ]
  val sub : [< exp ] -> [< exp ] -> [> exp ]
  val mul : [< exp ] -> [< exp ] -> [> exp ]
  val div : [< exp ] -> [< exp ] -> [> exp ]
  val modulo : [< exp ] -> [< exp ] -> [> exp ]
  val shiftl : [< exp ] -> [< exp ] -> [> exp ]
  val shiftr : [< exp ] -> [< exp ] -> [> exp ]
  val lt : [< exp ] -> [< exp ] -> [> exp ]
  val gt : [< exp ] -> [< exp ] -> [> exp ]
  val le : [< exp ] -> [< exp ] -> [> exp ]
  val ge : [< exp ] -> [< exp ] -> [> exp ]
  val eq : [< exp ] -> [< exp ] -> [> exp ]
  val ne : [< exp ] -> [< exp ] -> [> exp ]
  val logor : [< exp ] -> [< exp ] -> [> exp ]
  val logand : [< exp ] -> [< exp ] -> [> exp ]
  val logor_list : [< exp ] list -> exp
  val logand_list : [< exp ] list -> exp
  val bwand : [< exp ] -> [< exp ] -> [> exp ]
  val bwor : [< exp ] -> [< exp ] -> [> exp ]
  val bwxor : [< exp ] -> [< exp ] -> [> exp ]
  val cast : ('v, 's) typ -> [< exp ] -> [> exp ]
  val cast' : Cil_types.typ -> [< exp ] -> [> exp ]
  val addr : [< lval ] -> [> exp ]
  val mem : [< exp ] -> [> lval ]
  val index : [< lval ] -> [< exp ] -> [> lval ]
  val field : [< lval ] -> Cil_types.fieldinfo -> [> lval ]
  val fieldnamed : [< lval ] -> string -> [> lval ]
  val result : [> lval ]
  val term : Cil_types.term -> [> exp ]
  val range :
    [< `const of const'
     | `exp of exp'
     | `lval of lval'
     | `none
     | `var of var' ] ->
    [< `const of const'
     | `exp of exp'
     | `lval of lval'
     | `none
     | `var of var' ] ->
    [> exp ]
  val whole : [> exp ]
  val whole_right : [> exp ]
  val app : Cil_types.logic_info -> label list -> [< exp ] list -> [> exp ]
  val object_pointer : ?at:label -> [< exp ] -> [> exp ]
  val valid : ?at:label -> [< exp ] -> [> exp ]
  val valid_read : ?at:label -> [< exp ] -> [> exp ]
  val initialized : ?at:label -> [< exp ] -> [> exp ]
  val dangling : ?at:label -> [< exp ] -> [> exp ]
  val allocable : ?at:label -> [< exp ] -> [> exp ]
  val freeable : ?at:label -> [< exp ] -> [> exp ]
  val fresh : label -> label -> [< exp ] -> [< exp ] -> [> exp ]
  val of_init : Cil_types.init -> [> init ]
  val compound : Cil_types.typ -> init list -> [> init ]
  val values : (init, 'values) typ -> 'values -> init
  val ( + ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( - ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( * ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( / ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( % ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( << ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( >> ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( < ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( > ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( <= ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( >= ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( == ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( != ) : [< exp ] -> [< exp ] -> [> exp ]
  val ( -- ) : [< exp ] -> [< exp ] -> [> exp ]
  exception LogicInC of exp
  exception CInLogic of exp
  exception NotATerm of exp
  exception NotAPredicate of exp
  exception NotAFunction of Cil_types.logic_info
  exception Typing_error of string
  val cil_logic_label : label -> Cil_types.logic_label
  val cil_constant : [< const ] -> Cil_types.constant
  val cil_varinfo : [< var ] -> Cil_types.varinfo
  val cil_lval : loc:Cil_types.location -> [< lval ] -> Cil_types.lval
  val cil_exp : loc:Cil_types.location -> [< exp ] -> Cil_types.exp
  val cil_term_lval :
    loc:Cil_types.location ->
    ?restyp:Cil_types.typ -> [< lval ] -> Cil_types.term_lval
  val cil_term :
    loc:Cil_types.location ->
    ?restyp:Cil_types.typ -> [< exp ] -> Cil_types.term
  val cil_iterm :
    loc:Cil_types.location ->
    ?restyp:Cil_types.typ -> [< exp ] -> Cil_types.identified_term
  val cil_pred :
    loc:Cil_types.location ->
    ?restyp:Cil_types.typ -> [< exp ] -> Cil_types.predicate
  val cil_ipred :
    loc:Cil_types.location ->
    ?restyp:Cil_types.typ -> [< exp ] -> Cil_types.identified_predicate
  val cil_init : loc:Cil_types.location -> [< init ] -> Cil_types.init
  val cil_typeof : [< var ] -> Cil_types.typ
  type instr'
  type stmt'
  type instr = [ `instr of Cil_builder.Pure.instr' ]
  type stmt =
      [ `instr of Cil_builder.Pure.instr' | `stmt of Cil_builder.Pure.stmt' ]
  val of_instr : Cil_types.instr -> [> Cil_builder.Pure.instr ]
  val skip : [> Cil_builder.Pure.instr ]
  val assign : [< lval ] -> [< exp ] -> [> Cil_builder.Pure.instr ]
  val incr : [< lval ] -> [> Cil_builder.Pure.instr ]
  val call :
    [< `lval of lval' | `none | `var of var' ] ->
    [< exp ] -> [< exp ] list -> [> Cil_builder.Pure.instr ]
  val of_stmtkind : Cil_types.stmtkind -> [> Cil_builder.Pure.stmt ]
  val of_stmt : Cil_types.stmt -> [> Cil_builder.Pure.stmt ]
  val of_stmts : Cil_types.stmt list -> [> Cil_builder.Pure.stmt ]
  val block : [< Cil_builder.Pure.stmt ] list -> [> Cil_builder.Pure.stmt ]
  val ghost : [< Cil_builder.Pure.stmt ] -> [> Cil_builder.Pure.stmt ]
  val cil_instr :
    loc:Cil_types.location -> Cil_builder.Pure.instr -> Cil_types.instr
  val cil_stmtkind :
    loc:Cil_types.location -> Cil_builder.Pure.stmt -> Cil_types.stmtkind
  val cil_stmt :
    loc:Cil_types.location -> Cil_builder.Pure.stmt -> Cil_types.stmt
  val ( := ) : [< lval ] -> [< exp ] -> [> Cil_builder.Pure.instr ]
  val ( += ) : [< lval ] -> [< exp ] -> [> Cil_builder.Pure.instr ]
  val ( -= ) : [< lval ] -> [< exp ] -> [> Cil_builder.Pure.instr ]
end