sig
  module Type :
    sig
      exception NotACType
      type ('value, 'shape) typ
      val of_ltyp : Cil_types.logic_type -> (unit, unit) Cil_builder.Type.typ
      val integer : (unit, unit) Cil_builder.Type.typ
      val real : (unit, unit) Cil_builder.Type.typ
      val of_ctyp : Cil_types.typ -> ('v, 'v) Cil_builder.Type.typ
      val void : ('v, 'v) Cil_builder.Type.typ
      val bool : ('v, 'v) Cil_builder.Type.typ
      val char : ('v, 'v) Cil_builder.Type.typ
      val schar : ('v, 'v) Cil_builder.Type.typ
      val uchar : ('v, 'v) Cil_builder.Type.typ
      val int : ('v, 'v) Cil_builder.Type.typ
      val unit : ('v, 'v) Cil_builder.Type.typ
      val short : ('v, 'v) Cil_builder.Type.typ
      val ushort : ('v, 'v) Cil_builder.Type.typ
      val long : ('v, 'v) Cil_builder.Type.typ
      val ulong : ('v, 'v) Cil_builder.Type.typ
      val longlong : ('v, 'v) Cil_builder.Type.typ
      val ulonglong : ('v, 'v) Cil_builder.Type.typ
      val float : ('v, 'v) Cil_builder.Type.typ
      val double : ('v, 'v) Cil_builder.Type.typ
      val longdouble : ('v, 'v) Cil_builder.Type.typ
      val ptr :
        ('v, 's) Cil_builder.Type.typ -> ('v, 'v) Cil_builder.Type.typ
      val array :
        ?size:int ->
        ('v, 's) Cil_builder.Type.typ -> ('v, 's list) Cil_builder.Type.typ
      val attribute :
        ('v, 's) Cil_builder.Type.typ ->
        string -> Cil_types.attrparam list -> ('v, 's) Cil_builder.Type.typ
      val const :
        ('v, 's) Cil_builder.Type.typ -> ('v, 's) Cil_builder.Type.typ
      val stdlib_generated :
        ('v, 's) Cil_builder.Type.typ -> ('v, 's) Cil_builder.Type.typ
      val cil_typ : ('v, 's) Cil_builder.Type.typ -> Cil_types.typ
      val cil_logic_type :
        ('v, 's) Cil_builder.Type.typ -> Cil_types.logic_type
    end
  module Exp :
    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
  module Pure :
    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
  exception WrongContext of string
  module type T = sig val loc : Cil_types.location end
  module Stateful :
    functor (Location : T->
      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
        val open_function :
          ?ghost:bool -> ?vorig_name:string -> string -> [> var ]
        val set_return_type : ('s, 'v) typ -> unit
        val set_return_type' : Cil_types.typ -> unit
        val add_attribute : Cil_types.attribute -> unit
        val add_new_attribute : string -> Cil_types.attrparam list -> unit
        val add_stdlib_generated : unit -> unit
        val finish_function : ?register:bool -> unit -> Cil_types.global
        val finish_declaration : ?register:bool -> unit -> Cil_types.global
        type source =
            [ `const of const'
            | `exp of exp'
            | `indirect of exp
            | `lval of lval'
            | `var of var' ]
        val indirect :
          [< Cil_builder.Stateful.source ] ->
          [> Cil_builder.Stateful.source ]
        val assigns :
          [< exp ] list ->
          [< `const of const'
           | `exp of exp'
           | `indirect of [< exp ]
           | `lval of lval'
           | `var of var' ]
          list -> unit
        val requires : [< exp ] -> unit
        val ensures : [< exp ] -> unit
        val of_stmtkind : Cil_types.stmtkind -> unit
        val of_stmt : Cil_types.stmt -> unit
        val of_stmts : Cil_types.stmt list -> unit
        val open_block :
          ?into:Cil_types.fundec -> ?ghost:bool -> unit -> unit
        val open_ghost : ?into:Cil_types.fundec -> unit -> unit
        val open_switch : ?into:Cil_types.fundec -> [< exp ] -> unit
        val open_if : ?into:Cil_types.fundec -> [< exp ] -> unit
        val open_else : unit -> unit
        val close : unit -> unit
        val finish_block : unit -> Cil_types.block
        val finish_instr_list :
          ?scope:Cil_types.block -> unit -> Cil_types.instr list
        val finish_stmt : unit -> Cil_types.stmt
        val case : [< exp ] -> unit
        val break : unit -> unit
        val return :
          [< `const of const'
           | `exp of exp'
           | `lval of lval'
           | `none
           | `var of var' ] ->
          unit
        val local :
          ?ghost:bool -> ?init:'-> (init, 'v) typ -> string -> [> var ]
        val local' :
          ?ghost:bool -> ?init:init -> Cil_types.typ -> string -> [> var ]
        val local_copy :
          ?ghost:bool -> ?suffix:string -> [< var ] -> [> var ]
        val parameter :
          ?ghost:bool ->
          ?attributes:Cil_types.attributes ->
          Cil_types.typ -> string -> [> var ]
        val of_instr : Cil_types.instr -> unit
        val skip : unit -> unit
        val assign : [< lval ] -> [< exp ] -> unit
        val incr : [< lval ] -> unit
        val call :
          [< `lval of lval' | `none | `var of var' ] ->
          [< exp ] -> [< exp ] list -> unit
        val pure : [< exp ] -> unit
        val ( := ) : [< lval ] -> [< exp ] -> unit
        val ( += ) : [< lval ] -> [< exp ] -> unit
        val ( -= ) : [< lval ] -> [< exp ] -> unit
      end
end