sig
  module Frama_c_builtins :
    sig
      val self : State.t
      val name : string
      val mark_as_computed : ?project:Project.t -> unit -> unit
      val is_computed : ?project:Project.t -> unit -> bool
      module Datatype : Datatype.S
      val add_hook_on_update : (Datatype.t -> unit) -> unit
      val howto_marshal : (Datatype.t -> 'a) -> ('-> Datatype.t) -> unit
      type key = string
      type data = Cil_types.varinfo
      val replace : key -> data -> unit
      val add : key -> data -> unit
      val clear : unit -> unit
      val length : unit -> int
      val iter : (key -> data -> unit) -> unit
      val iter_sorted :
        ?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
      val fold : (key -> data -> '-> 'a) -> '-> 'a
      val fold_sorted :
        ?cmp:(key -> key -> int) -> (key -> data -> '-> 'a) -> '-> 'a
      val memo : ?change:(data -> data) -> (key -> data) -> key -> data
      val find : key -> data
      val find_all : key -> data list
      val mem : key -> bool
      val remove : key -> unit
    end
  val is_builtin : Cil_types.varinfo -> bool
  val is_unused_builtin : Cil_types.varinfo -> bool
  val is_special_builtin : string -> bool
  val add_special_builtin : string -> unit
  val add_special_builtin_family : (string -> bool) -> unit
  val init_builtins : unit -> unit
  val initCIL : initLogicBuiltins:(unit -> unit) -> Cil_types.mach -> unit
  type theMachine = private {
    mutable useLogicalOperators : bool;
    mutable theMachine : Cil_types.mach;
    mutable lowerConstants : bool;
    mutable insertImplicitCasts : bool;
    mutable underscore_name : bool;
    mutable stringLiteralType : Cil_types.typ;
    mutable upointKind : Cil_types.ikind;
    mutable upointType : Cil_types.typ;
    mutable wcharKind : Cil_types.ikind;
    mutable wcharType : Cil_types.typ;
    mutable ptrdiffKind : Cil_types.ikind;
    mutable ptrdiffType : Cil_types.typ;
    mutable typeOfSizeOf : Cil_types.typ;
    mutable kindOfSizeOf : Cil_types.ikind;
  }
  val theMachine : Cil.theMachine
  val selfMachine : State.t
  val selfMachine_is_computed : ?project:Project.project -> unit -> bool
  val msvcMode : unit -> bool
  val gccMode : unit -> bool
  val emptyFunctionFromVI : Cil_types.varinfo -> Cil_types.fundec
  val emptyFunction : string -> Cil_types.fundec
  val setFormals : Cil_types.fundec -> Cil_types.varinfo list -> unit
  val getReturnType : Cil_types.typ -> Cil_types.typ
  val setReturnTypeVI : Cil_types.varinfo -> Cil_types.typ -> unit
  val setReturnType : Cil_types.fundec -> Cil_types.typ -> unit
  val setFunctionType : Cil_types.fundec -> Cil_types.typ -> unit
  val setFunctionTypeMakeFormals : Cil_types.fundec -> Cil_types.typ -> unit
  val setMaxId : Cil_types.fundec -> unit
  val selfFormalsDecl : State.t
  val makeFormalsVarDecl :
    ?ghost:bool ->
    string * Cil_types.typ * Cil_types.attributes -> Cil_types.varinfo
  val setFormalsDecl : Cil_types.varinfo -> Cil_types.typ -> unit
  val removeFormalsDecl : Cil_types.varinfo -> unit
  val unsafeSetFormalsDecl :
    Cil_types.varinfo -> Cil_types.varinfo list -> unit
  val iterFormalsDecl :
    (Cil_types.varinfo -> Cil_types.varinfo list -> unit) -> unit
  val getFormalsDecl : Cil_types.varinfo -> Cil_types.varinfo list
  val dummyFile : Cil_types.file
  val iterGlobals : Cil_types.file -> (Cil_types.global -> unit) -> unit
  val foldGlobals :
    Cil_types.file -> ('-> Cil_types.global -> 'a) -> '-> 'a
  val mapGlobals :
    Cil_types.file -> (Cil_types.global -> Cil_types.global) -> unit
  val findOrCreateFunc :
    Cil_types.file -> string -> Cil_types.typ -> Cil_types.varinfo
  val new_exp : loc:Cil_types.location -> Cil_types.exp_node -> Cil_types.exp
  val copy_exp : Cil_types.exp -> Cil_types.exp
  val dummy_exp : Cil_types.exp_node -> Cil_types.exp
  val is_case_label : Cil_types.label -> bool
  val pushGlobal :
    Cil_types.global ->
    types:Cil_types.global list Pervasives.ref ->
    variables:Cil_types.global list Pervasives.ref -> unit
  val invalidStmt : Cil_types.stmt
  module Builtin_functions :
    sig
      val self : State.t
      val name : string
      val mark_as_computed : ?project:Project.t -> unit -> unit
      val is_computed : ?project:Project.t -> unit -> bool
      module Datatype : Datatype.S
      val add_hook_on_update : (Datatype.t -> unit) -> unit
      val howto_marshal : (Datatype.t -> 'a) -> ('-> Datatype.t) -> unit
      type key = string
      type data = Cil_types.typ * Cil_types.typ list * bool
      val replace : key -> data -> unit
      val add : key -> data -> unit
      val clear : unit -> unit
      val length : unit -> int
      val iter : (key -> data -> unit) -> unit
      val iter_sorted :
        ?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
      val fold : (key -> data -> '-> 'a) -> '-> 'a
      val fold_sorted :
        ?cmp:(key -> key -> int) -> (key -> data -> '-> 'a) -> '-> 'a
      val memo : ?change:(data -> data) -> (key -> data) -> key -> data
      val find : key -> data
      val find_all : key -> data list
      val mem : key -> bool
      val remove : key -> unit
    end
  val builtinLoc : Cil_types.location
  val range_loc :
    Cil_types.location -> Cil_types.location -> Cil_types.location
  val makeZeroInit :
    loc:Cil_types.location -> Cil_types.typ -> Cil_types.init
  val foldLeftCompound :
    implicit:bool ->
    doinit:(Cil_types.offset -> Cil_types.init -> Cil_types.typ -> '-> 'a) ->
    ct:Cil_types.typ ->
    initl:(Cil_types.offset * Cil_types.init) list -> acc:'-> 'a
  val voidType : Cil_types.typ
  val isVoidType : Cil_types.typ -> bool
  val isVoidPtrType : Cil_types.typ -> bool
  val intType : Cil_types.typ
  val uintType : Cil_types.typ
  val longType : Cil_types.typ
  val longLongType : Cil_types.typ
  val ulongType : Cil_types.typ
  val ulongLongType : Cil_types.typ
  val uint16_t : unit -> Cil_types.typ
  val uint32_t : unit -> Cil_types.typ
  val uint64_t : unit -> Cil_types.typ
  val charType : Cil_types.typ
  val scharType : Cil_types.typ
  val ucharType : Cil_types.typ
  val charPtrType : Cil_types.typ
  val scharPtrType : Cil_types.typ
  val ucharPtrType : Cil_types.typ
  val charConstPtrType : Cil_types.typ
  val voidPtrType : Cil_types.typ
  val voidConstPtrType : Cil_types.typ
  val intPtrType : Cil_types.typ
  val uintPtrType : Cil_types.typ
  val floatType : Cil_types.typ
  val doubleType : Cil_types.typ
  val longDoubleType : Cil_types.typ
  val isSignedInteger : Cil_types.typ -> bool
  val isUnsignedInteger : Cil_types.typ -> bool
  val missingFieldName : string
  val compFullName : Cil_types.compinfo -> string
  val isCompleteType : ?allowZeroSizeArrays:bool -> Cil_types.typ -> bool
  val has_flexible_array_member : Cil_types.typ -> bool
  val unrollType : Cil_types.typ -> Cil_types.typ
  val unrollTypeDeep : Cil_types.typ -> Cil_types.typ
  val separateStorageModifiers :
    Cil_types.attribute list ->
    Cil_types.attribute list * Cil_types.attribute list
  val arithmeticConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ
  val integralPromotion : Cil_types.typ -> Cil_types.typ
  val isAnyCharType : Cil_types.typ -> bool
  val isCharType : Cil_types.typ -> bool
  val isShortType : Cil_types.typ -> bool
  val isAnyCharPtrType : Cil_types.typ -> bool
  val isCharPtrType : Cil_types.typ -> bool
  val isCharConstPtrType : Cil_types.typ -> bool
  val isAnyCharArrayType : Cil_types.typ -> bool
  val isCharArrayType : Cil_types.typ -> bool
  val isIntegralType : Cil_types.typ -> bool
  val isBoolType : Cil_types.typ -> bool
  val isLogicPureBooleanType : Cil_types.logic_type -> bool
  val isIntegralOrPointerType : Cil_types.typ -> bool
  val isLogicIntegralType : Cil_types.logic_type -> bool
  val isLogicBooleanType : Cil_types.logic_type -> bool
  val isFloatingType : Cil_types.typ -> bool
  val isLogicFloatType : Cil_types.logic_type -> bool
  val isLogicRealOrFloatType : Cil_types.logic_type -> bool
  val isLogicRealType : Cil_types.logic_type -> bool
  val isArithmeticType : Cil_types.typ -> bool
  val isArithmeticOrPointerType : Cil_types.typ -> bool
  val isLogicArithmeticType : Cil_types.logic_type -> bool
  val isFunctionType : Cil_types.typ -> bool
  val isLogicFunctionType : Cil_types.logic_type -> bool
  val isPointerType : Cil_types.typ -> bool
  val isFunPtrType : Cil_types.typ -> bool
  val isLogicFunPtrType : Cil_types.logic_type -> bool
  val isTypeTagType : Cil_types.logic_type -> bool
  val isVariadicListType : Cil_types.typ -> bool
  val argsToList :
    (string * Cil_types.typ * Cil_types.attributes) list option ->
    (string * Cil_types.typ * Cil_types.attributes) list
  val argsToPairOfLists :
    (string * Cil_types.typ * Cil_types.attributes) list option ->
    (string * Cil_types.typ * Cil_types.attributes) list *
    (string * Cil_types.typ * Cil_types.attributes) list
  val isArrayType : Cil_types.typ -> bool
  val isStructOrUnionType : Cil_types.typ -> bool
  exception LenOfArray
  val lenOfArray : Cil_types.exp option -> int
  val lenOfArray64 : Cil_types.exp option -> Integer.t
  val getCompField : Cil_types.compinfo -> string -> Cil_types.fieldinfo
  type existsAction = ExistsTrue | ExistsFalse | ExistsMaybe
  val existsType :
    (Cil_types.typ -> Cil.existsAction) -> Cil_types.typ -> bool
  val splitFunctionType :
    Cil_types.typ ->
    Cil_types.typ *
    (string * Cil_types.typ * Cil_types.attributes) list option * bool *
    Cil_types.attributes
  val splitFunctionTypeVI :
    Cil_types.varinfo ->
    Cil_types.typ *
    (string * Cil_types.typ * Cil_types.attributes) list option * bool *
    Cil_types.attributes
  val makeVarinfo :
    ?source:bool ->
    ?temp:bool ->
    ?referenced:bool ->
    ?ghost:bool ->
    ?loc:Cil_datatype.Location.t ->
    bool -> bool -> string -> Cil_types.typ -> Cil_types.varinfo
  val makeFormalVar :
    Cil_types.fundec ->
    ?ghost:bool ->
    ?where:string ->
    ?loc:Cil_datatype.Location.t ->
    string -> Cil_types.typ -> Cil_types.varinfo
  val makeLocalVar :
    Cil_types.fundec ->
    ?scope:Cil_types.block ->
    ?temp:bool ->
    ?referenced:bool ->
    ?insert:bool ->
    ?ghost:bool ->
    ?loc:Cil_datatype.Location.t ->
    string -> Cil_types.typ -> Cil_types.varinfo
  val refresh_local_name : Cil_types.fundec -> Cil_types.varinfo -> unit
  val makeTempVar :
    Cil_types.fundec ->
    ?insert:bool ->
    ?ghost:bool ->
    ?name:string ->
    ?descr:string ->
    ?descrpure:bool ->
    ?loc:Cil_datatype.Location.t -> Cil_types.typ -> Cil_types.varinfo
  val makeGlobalVar :
    ?source:bool ->
    ?temp:bool ->
    ?referenced:bool ->
    ?ghost:bool ->
    ?loc:Cil_datatype.Location.t ->
    string -> Cil_types.typ -> Cil_types.varinfo
  val copyVarinfo : Cil_types.varinfo -> string -> Cil_types.varinfo
  val update_var_type : Cil_types.varinfo -> Cil_types.typ -> unit
  val isBitfield : Cil_types.lval -> bool
  val lastOffset : Cil_types.offset -> Cil_types.offset
  val addOffsetLval : Cil_types.offset -> Cil_types.lval -> Cil_types.lval
  val addOffset : Cil_types.offset -> Cil_types.offset -> Cil_types.offset
  val removeOffsetLval : Cil_types.lval -> Cil_types.lval * Cil_types.offset
  val removeOffset : Cil_types.offset -> Cil_types.offset * Cil_types.offset
  val typeOfLval : Cil_types.lval -> Cil_types.typ
  val typeOfLhost : Cil_types.lhost -> Cil_types.typ
  val typeOfTermLval : Cil_types.term_lval -> Cil_types.logic_type
  val typeOffset : Cil_types.typ -> Cil_types.offset -> Cil_types.typ
  val typeTermOffset :
    Cil_types.logic_type -> Cil_types.term_offset -> Cil_types.logic_type
  val typeOfInit : Cil_types.init -> Cil_types.typ
  val is_modifiable_lval : Cil_types.lval -> bool
  val zero : loc:Cil_datatype.Location.t -> Cil_types.exp
  val one : loc:Cil_datatype.Location.t -> Cil_types.exp
  val mone : loc:Cil_datatype.Location.t -> Cil_types.exp
  val kinteger64 :
    loc:Cil_types.location ->
    ?repr:string -> ?kind:Cil_types.ikind -> Integer.t -> Cil_types.exp
  val kinteger :
    loc:Cil_types.location -> Cil_types.ikind -> int -> Cil_types.exp
  val integer : loc:Cil_types.location -> int -> Cil_types.exp
  val kfloat :
    loc:Cil_types.location -> Cil_types.fkind -> float -> Cil_types.exp
  val isInteger : Cil_types.exp -> Integer.t option
  val isConstant : Cil_types.exp -> bool
  val isIntegerConstant : Cil_types.exp -> bool
  val isConstantOffset : Cil_types.offset -> bool
  val isZero : Cil_types.exp -> bool
  val isLogicZero : Cil_types.term -> bool
  val isLogicNull : Cil_types.term -> bool
  val no_op_coerce : Cil_types.logic_type -> Cil_types.term -> bool
  val reduce_multichar : Cil_types.typ -> int64 list -> int64
  val interpret_character_constant :
    int64 list -> Cil_types.constant * Cil_types.typ
  val charConstToInt : char -> Integer.t
  val charConstToIntConstant : char -> Cil_types.constant
  val constFold : bool -> Cil_types.exp -> Cil_types.exp
  val constFoldToInt : ?machdep:bool -> Cil_types.exp -> Integer.t option
  val constFoldTermNodeAtTop : Cil_types.term_node -> Cil_types.term_node
  val constFoldTerm : bool -> Cil_types.term -> Cil_types.term
  val constFoldOffset : bool -> Cil_types.offset -> Cil_types.offset
  val constFoldBinOp :
    loc:Cil_types.location ->
    bool ->
    Cil_types.binop ->
    Cil_types.exp -> Cil_types.exp -> Cil_types.typ -> Cil_types.exp
  val compareConstant : Cil_types.constant -> Cil_types.constant -> bool
  val increm : Cil_types.exp -> int -> Cil_types.exp
  val increm64 : Cil_types.exp -> Integer.t -> Cil_types.exp
  val var : Cil_types.varinfo -> Cil_types.lval
  val evar : ?loc:Cil_types.location -> Cil_types.varinfo -> Cil_types.exp
  val mkAddrOf : loc:Cil_types.location -> Cil_types.lval -> Cil_types.exp
  val mkAddrOfVi : Cil_types.varinfo -> Cil_types.exp
  val mkAddrOrStartOf :
    loc:Cil_types.location -> Cil_types.lval -> Cil_types.exp
  val mkMem : addr:Cil_types.exp -> off:Cil_types.offset -> Cil_types.lval
  val mkBinOp :
    loc:Cil_types.location ->
    Cil_types.binop -> Cil_types.exp -> Cil_types.exp -> Cil_types.exp
  val mkBinOp_safe_ptr_cmp :
    loc:Cil_types.location ->
    Cil_types.binop -> Cil_types.exp -> Cil_types.exp -> Cil_types.exp
  val mkTermMem :
    addr:Cil_types.term -> off:Cil_types.term_offset -> Cil_types.term_lval
  val mkString : loc:Cil_types.location -> string -> Cil_types.exp
  val need_cast : ?force:bool -> Cil_types.typ -> Cil_types.typ -> bool
  val mkCastT :
    ?force:bool ->
    e:Cil_types.exp ->
    oldt:Cil_types.typ -> newt:Cil_types.typ -> Cil_types.exp
  val mkCast :
    ?force:bool -> e:Cil_types.exp -> newt:Cil_types.typ -> Cil_types.exp
  val stripTermCasts : Cil_types.term -> Cil_types.term
  val stripCasts : Cil_types.exp -> Cil_types.exp
  val stripInfo : Cil_types.exp -> Cil_types.exp
  val stripCastsAndInfo : Cil_types.exp -> Cil_types.exp
  val stripCastsButLastInfo : Cil_types.exp -> Cil_types.exp
  val exp_info_of_term : Cil_types.term -> Cil_types.exp_info
  val term_of_exp_info :
    Cil_types.location ->
    Cil_types.term_node -> Cil_types.exp_info -> Cil_types.term
  val map_under_info :
    (Cil_types.exp -> Cil_types.exp) -> Cil_types.exp -> Cil_types.exp
  val app_under_info : (Cil_types.exp -> unit) -> Cil_types.exp -> unit
  val typeOf : Cil_types.exp -> Cil_types.typ
  val typeOf_pointed : Cil_types.typ -> Cil_types.typ
  val typeOf_array_elem : Cil_types.typ -> Cil_types.typ
  val is_fully_arithmetic : Cil_types.typ -> bool
  val parseInt : string -> Integer.t
  val parseIntExp : loc:Cil_types.location -> string -> Cil_types.exp
  val parseIntLogic : loc:Cil_types.location -> string -> Cil_types.term
  val appears_in_expr : Cil_types.varinfo -> Cil_types.exp -> bool
  val mkStmt :
    ?ghost:bool ->
    ?valid_sid:bool ->
    ?sattr:Cil_types.attributes -> Cil_types.stmtkind -> Cil_types.stmt
  val mkStmtCfg :
    before:bool ->
    new_stmtkind:Cil_types.stmtkind ->
    ref_stmt:Cil_types.stmt -> Cil_types.stmt
  val mkBlock : Cil_types.stmt list -> Cil_types.block
  val mkBlockNonScoping : Cil_types.stmt list -> Cil_types.block
  val mkStmtCfgBlock : Cil_types.stmt list -> Cil_types.stmt
  val mkStmtOneInstr :
    ?ghost:bool ->
    ?valid_sid:bool ->
    ?sattr:Cil_types.attributes -> Cil_types.instr -> Cil_types.stmt
  val mkEmptyStmt :
    ?ghost:bool ->
    ?valid_sid:bool ->
    ?sattr:Cil_types.attributes ->
    ?loc:Cil_types.location -> unit -> Cil_types.stmt
  val dummyInstr : Cil_types.instr
  val dummyStmt : Cil_types.stmt
  val mkPureExprInstr :
    fundec:Cil_types.fundec ->
    scope:Cil_types.block ->
    ?loc:Cil_types.location -> Cil_types.exp -> Cil_types.instr
  val mkPureExpr :
    ?ghost:bool ->
    ?valid_sid:bool ->
    fundec:Cil_types.fundec ->
    ?loc:Cil_types.location -> Cil_types.exp -> Cil_types.stmt
  val mkLoop :
    ?sattr:Cil_types.attributes ->
    guard:Cil_types.exp -> body:Cil_types.stmt list -> Cil_types.stmt list
  val mkForIncr :
    iter:Cil_types.varinfo ->
    first:Cil_types.exp ->
    stopat:Cil_types.exp ->
    incr:Cil_types.exp -> body:Cil_types.stmt list -> Cil_types.stmt list
  val mkFor :
    start:Cil_types.stmt list ->
    guard:Cil_types.exp ->
    next:Cil_types.stmt list ->
    body:Cil_types.stmt list -> Cil_types.stmt list
  val block_from_unspecified_sequence :
    (Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
     Cil_types.lval list * Cil_types.stmt Pervasives.ref list)
    list -> Cil_types.block
  val treat_constructor_as_func :
    (Cil_types.lval option ->
     Cil_types.exp -> Cil_types.exp list -> Cil_types.location -> 'a) ->
    Cil_types.varinfo ->
    Cil_types.varinfo ->
    Cil_types.exp list ->
    Cil_types.constructor_kind -> Cil_types.location -> 'a
  val find_def_stmt : Cil_types.block -> Cil_types.varinfo -> Cil_types.stmt
  val has_extern_local_init : Cil_types.block -> bool
  val is_ghost_else : Cil_types.block -> bool
  type attributeClass = AttrName of bool | AttrFunType of bool | AttrType
  val registerAttribute : string -> Cil.attributeClass -> unit
  val removeAttribute : string -> unit
  val attributeClass : string -> Cil.attributeClass
  val partitionAttributes :
    default:Cil.attributeClass ->
    Cil_types.attributes ->
    Cil_types.attribute list * Cil_types.attribute list *
    Cil_types.attribute list
  val addAttribute :
    Cil_types.attribute -> Cil_types.attributes -> Cil_types.attributes
  val addAttributes :
    Cil_types.attribute list -> Cil_types.attributes -> Cil_types.attributes
  val dropAttribute : string -> Cil_types.attributes -> Cil_types.attributes
  val dropAttributes :
    string list -> Cil_types.attributes -> Cil_types.attributes
  val frama_c_ghost_else : string
  val frama_c_ghost_formal : string
  val frama_c_init_obj : string
  val frama_c_mutable : string
  val is_mutable_or_initialized : Cil_types.lval -> bool
  val isGhostFormalVarinfo : Cil_types.varinfo -> bool
  val isGhostFormalVarDecl :
    string * Cil_types.typ * Cil_types.attributes -> bool
  val typeDeepDropAttributes : string list -> Cil_types.typ -> Cil_types.typ
  val typeDeepDropAllAttributes : Cil_types.typ -> Cil_types.typ
  val filterAttributes :
    string -> Cil_types.attributes -> Cil_types.attributes
  val hasAttribute : string -> Cil_types.attributes -> bool
  val mkAttrAnnot : string -> string
  val attributeName : Cil_types.attribute -> string
  val findAttribute :
    string -> Cil_types.attribute list -> Cil_types.attrparam list
  val typeAttrs : Cil_types.typ -> Cil_types.attribute list
  val typeAttr : Cil_types.typ -> Cil_types.attribute list
  val setTypeAttrs : Cil_types.typ -> Cil_types.attributes -> Cil_types.typ
  val typeAddAttributes :
    Cil_types.attribute list -> Cil_types.typ -> Cil_types.typ
  val typeRemoveAttributes : string list -> Cil_types.typ -> Cil_types.typ
  val typeRemoveAllAttributes : Cil_types.typ -> Cil_types.typ
  val typeRemoveAttributesDeep :
    string list -> Cil_types.typ -> Cil_types.typ
  val typeHasAttribute : string -> Cil_types.typ -> bool
  val typeHasQualifier : string -> Cil_types.typ -> bool
  val typeHasAttributeDeep : string -> Cil_types.typ -> bool
  val typeHasAttributeMemoryBlock : string -> Cil_types.typ -> bool
  val type_remove_qualifier_attributes : Cil_types.typ -> Cil_types.typ
  val type_remove_qualifier_attributes_deep : Cil_types.typ -> Cil_types.typ
  val type_remove_attributes_for_c_cast : Cil_types.typ -> Cil_types.typ
  val type_remove_attributes_for_logic_type : Cil_types.typ -> Cil_types.typ
  val filter_qualifier_attributes :
    Cil_types.attributes -> Cil_types.attributes
  val splitArrayAttributes :
    Cil_types.attributes -> Cil_types.attributes * Cil_types.attributes
  val bitfield_attribute_name : string
  val expToAttrParam : Cil_types.exp -> Cil_types.attrparam
  val global_annotation_attributes :
    Cil_types.global_annotation -> Cil_types.attributes
  val global_attributes : Cil_types.global -> Cil_types.attributes
  exception NotAnAttrParam of Cil_types.exp
  val isConstType : Cil_types.typ -> bool
  val isVolatileType : Cil_types.typ -> bool
  val isVolatileLogicType : Cil_types.logic_type -> bool
  val isVolatileLval : Cil_types.lval -> bool
  val isVolatileTermLval : Cil_types.term_lval -> bool
  val isGhostType : Cil_types.typ -> bool
  val isWFGhostType : Cil_types.typ -> bool
  type 'a visitAction =
      SkipChildren
    | DoChildren
    | DoChildrenPost of ('-> 'a)
    | JustCopy
    | JustCopyPost of ('-> 'a)
    | ChangeTo of 'a
    | ChangeToPost of 'a * ('-> 'a)
    | ChangeDoChildrenPost of 'a * ('-> 'a)
  val mk_behavior :
    ?name:string ->
    ?assumes:Cil_types.identified_predicate list ->
    ?requires:Cil_types.identified_predicate list ->
    ?post_cond:(Cil_types.termination_kind * Cil_types.identified_predicate)
               list ->
    ?assigns:Cil_types.assigns ->
    ?allocation:Cil_types.allocation ->
    ?extended:Cil_types.acsl_extension list -> unit -> Cil_types.behavior
  val default_behavior_name : string
  val is_default_behavior : Cil_types.behavior -> bool
  val find_default_behavior :
    Cil_types.funspec -> Cil_types.funbehavior option
  val find_default_requires :
    Cil_types.behavior list -> Cil_types.identified_predicate list
  class type cilVisitor =
    object
      method behavior : Visitor_behavior.t
      method current_func : Cil_types.fundec option
      method current_kinstr : Cil_types.kinstr
      method current_stmt : Cil_types.stmt option
      method fill_global_tables : unit
      method get_filling_actions : (unit -> unit) Queue.t
      method plain_copy_visitor : Cil.cilVisitor
      method pop_stmt : Cil_types.stmt -> unit
      method project : Project.t option
      method push_stmt : Cil_types.stmt -> unit
      method queueInstr : Cil_types.instr list -> unit
      method reset_current_func : unit -> unit
      method set_current_func : Cil_types.fundec -> unit
      method unqueueInstr : unit -> Cil_types.instr list
      method vallocates :
        Cil_types.identified_term list ->
        Cil_types.identified_term list Cil.visitAction
      method vallocation :
        Cil_types.allocation -> Cil_types.allocation Cil.visitAction
      method vannotation :
        Cil_types.global_annotation ->
        Cil_types.global_annotation Cil.visitAction
      method vassigns :
        Cil_types.assigns -> Cil_types.assigns Cil.visitAction
      method vattr :
        Cil_types.attribute -> Cil_types.attribute list Cil.visitAction
      method vattrparam :
        Cil_types.attrparam -> Cil_types.attrparam Cil.visitAction
      method vbehavior :
        Cil_types.funbehavior -> Cil_types.funbehavior Cil.visitAction
      method vblock : Cil_types.block -> Cil_types.block Cil.visitAction
      method vcode_annot :
        Cil_types.code_annotation ->
        Cil_types.code_annotation Cil.visitAction
      method vcompinfo :
        Cil_types.compinfo -> Cil_types.compinfo Cil.visitAction
      method vdeps : Cil_types.deps -> Cil_types.deps Cil.visitAction
      method venuminfo :
        Cil_types.enuminfo -> Cil_types.enuminfo Cil.visitAction
      method venumitem :
        Cil_types.enumitem -> Cil_types.enumitem Cil.visitAction
      method vexpr : Cil_types.exp -> Cil_types.exp Cil.visitAction
      method vfieldinfo :
        Cil_types.fieldinfo -> Cil_types.fieldinfo Cil.visitAction
      method vfile : Cil_types.file -> Cil_types.file Cil.visitAction
      method vfrees :
        Cil_types.identified_term list ->
        Cil_types.identified_term list Cil.visitAction
      method vfrom : Cil_types.from -> Cil_types.from Cil.visitAction
      method vfunc : Cil_types.fundec -> Cil_types.fundec Cil.visitAction
      method vglob :
        Cil_types.global -> Cil_types.global list Cil.visitAction
      method videntified_predicate :
        Cil_types.identified_predicate ->
        Cil_types.identified_predicate Cil.visitAction
      method videntified_term :
        Cil_types.identified_term ->
        Cil_types.identified_term Cil.visitAction
      method vimpact_pragma :
        Cil_types.impact_pragma -> Cil_types.impact_pragma Cil.visitAction
      method vinit :
        Cil_types.varinfo ->
        Cil_types.offset -> Cil_types.init -> Cil_types.init Cil.visitAction
      method vinitoffs : Cil_types.offset -> Cil_types.offset Cil.visitAction
      method vinst : Cil_types.instr -> Cil_types.instr list Cil.visitAction
      method vlocal_init :
        Cil_types.varinfo ->
        Cil_types.local_init -> Cil_types.local_init Cil.visitAction
      method vlogic_ctor_info_decl :
        Cil_types.logic_ctor_info ->
        Cil_types.logic_ctor_info Cil.visitAction
      method vlogic_ctor_info_use :
        Cil_types.logic_ctor_info ->
        Cil_types.logic_ctor_info Cil.visitAction
      method vlogic_info_decl :
        Cil_types.logic_info -> Cil_types.logic_info Cil.visitAction
      method vlogic_info_use :
        Cil_types.logic_info -> Cil_types.logic_info Cil.visitAction
      method vlogic_label :
        Cil_types.logic_label -> Cil_types.logic_label Cil.visitAction
      method vlogic_type :
        Cil_types.logic_type -> Cil_types.logic_type Cil.visitAction
      method vlogic_type_def :
        Cil_types.logic_type_def -> Cil_types.logic_type_def Cil.visitAction
      method vlogic_type_info_decl :
        Cil_types.logic_type_info ->
        Cil_types.logic_type_info Cil.visitAction
      method vlogic_type_info_use :
        Cil_types.logic_type_info ->
        Cil_types.logic_type_info Cil.visitAction
      method vlogic_var_decl :
        Cil_types.logic_var -> Cil_types.logic_var Cil.visitAction
      method vlogic_var_use :
        Cil_types.logic_var -> Cil_types.logic_var Cil.visitAction
      method vloop_pragma :
        Cil_types.loop_pragma -> Cil_types.loop_pragma Cil.visitAction
      method vlval : Cil_types.lval -> Cil_types.lval Cil.visitAction
      method vmodel_info :
        Cil_types.model_info -> Cil_types.model_info Cil.visitAction
      method voffs : Cil_types.offset -> Cil_types.offset Cil.visitAction
      method vpredicate :
        Cil_types.predicate -> Cil_types.predicate Cil.visitAction
      method vpredicate_node :
        Cil_types.predicate_node -> Cil_types.predicate_node Cil.visitAction
      method vquantifiers :
        Cil_types.quantifiers -> Cil_types.quantifiers Cil.visitAction
      method vslice_pragma :
        Cil_types.slice_pragma -> Cil_types.slice_pragma Cil.visitAction
      method vspec : Cil_types.funspec -> Cil_types.funspec Cil.visitAction
      method vstmt : Cil_types.stmt -> Cil_types.stmt Cil.visitAction
      method vterm : Cil_types.term -> Cil_types.term Cil.visitAction
      method vterm_lhost :
        Cil_types.term_lhost -> Cil_types.term_lhost Cil.visitAction
      method vterm_lval :
        Cil_types.term_lval -> Cil_types.term_lval Cil.visitAction
      method vterm_node :
        Cil_types.term_node -> Cil_types.term_node Cil.visitAction
      method vterm_offset :
        Cil_types.term_offset -> Cil_types.term_offset Cil.visitAction
      method vtype : Cil_types.typ -> Cil_types.typ Cil.visitAction
      method vvdec : Cil_types.varinfo -> Cil_types.varinfo Cil.visitAction
      method vvrbl : Cil_types.varinfo -> Cil_types.varinfo Cil.visitAction
    end
  val register_behavior_extension :
    string ->
    (Cil.cilVisitor ->
     Cil_types.acsl_extension_kind ->
     Cil_types.acsl_extension_kind Cil.visitAction) ->
    unit
  class internal_genericCilVisitor :
    Cil_types.fundec option Pervasives.ref ->
    Visitor_behavior.t -> (unit -> unit) Queue.t -> cilVisitor
  class genericCilVisitor : Visitor_behavior.t -> cilVisitor
  class nopCilVisitor : cilVisitor
  val doVisit :
    'visitor ->
    'visitor ->
    ('-> 'a) ->
    ('-> 'Cil.visitAction) -> ('visitor -> '-> 'a) -> '-> 'a
  val doVisitList :
    'visitor ->
    'visitor ->
    ('-> 'a) ->
    ('-> 'a list Cil.visitAction) ->
    ('visitor -> '-> 'a) -> '-> 'a list
  val visitCilFileCopy : Cil.cilVisitor -> Cil_types.file -> Cil_types.file
  val visitCilFile : Cil.cilVisitor -> Cil_types.file -> unit
  val visitCilFileSameGlobals : Cil.cilVisitor -> Cil_types.file -> unit
  val visitCilGlobal :
    Cil.cilVisitor -> Cil_types.global -> Cil_types.global list
  val visitCilFunction :
    Cil.cilVisitor -> Cil_types.fundec -> Cil_types.fundec
  val visitCilExpr : Cil.cilVisitor -> Cil_types.exp -> Cil_types.exp
  val visitCilEnumInfo :
    Cil.cilVisitor -> Cil_types.enuminfo -> Cil_types.enuminfo
  val visitCilLval : Cil.cilVisitor -> Cil_types.lval -> Cil_types.lval
  val visitCilOffset : Cil.cilVisitor -> Cil_types.offset -> Cil_types.offset
  val visitCilInitOffset :
    Cil.cilVisitor -> Cil_types.offset -> Cil_types.offset
  val visitCilLocal_init :
    Cil.cilVisitor ->
    Cil_types.varinfo -> Cil_types.local_init -> Cil_types.local_init
  val visitCilInstr :
    Cil.cilVisitor -> Cil_types.instr -> Cil_types.instr list
  val visitCilStmt : Cil.cilVisitor -> Cil_types.stmt -> Cil_types.stmt
  val visitCilBlock : Cil.cilVisitor -> Cil_types.block -> Cil_types.block
  val transient_block : Cil_types.block -> Cil_types.block
  val is_transient_block : Cil_types.block -> bool
  val flatten_transient_sub_blocks : Cil_types.block -> Cil_types.block
  val block_of_transient : Cil_types.block -> Cil_types.block
  val visitCilType : Cil.cilVisitor -> Cil_types.typ -> Cil_types.typ
  val visitCilVarDecl :
    Cil.cilVisitor -> Cil_types.varinfo -> Cil_types.varinfo
  val visitCilInit :
    Cil.cilVisitor ->
    Cil_types.varinfo -> Cil_types.offset -> Cil_types.init -> Cil_types.init
  val visitCilAttributes :
    Cil.cilVisitor -> Cil_types.attribute list -> Cil_types.attribute list
  val visitCilAnnotation :
    Cil.cilVisitor ->
    Cil_types.global_annotation -> Cil_types.global_annotation
  val visitCilCodeAnnotation :
    Cil.cilVisitor -> Cil_types.code_annotation -> Cil_types.code_annotation
  val visitCilDeps : Cil.cilVisitor -> Cil_types.deps -> Cil_types.deps
  val visitCilFrom : Cil.cilVisitor -> Cil_types.from -> Cil_types.from
  val visitCilAssigns :
    Cil.cilVisitor -> Cil_types.assigns -> Cil_types.assigns
  val visitCilFrees :
    Cil.cilVisitor ->
    Cil_types.identified_term list -> Cil_types.identified_term list
  val visitCilAllocates :
    Cil.cilVisitor ->
    Cil_types.identified_term list -> Cil_types.identified_term list
  val visitCilAllocation :
    Cil.cilVisitor -> Cil_types.allocation -> Cil_types.allocation
  val visitCilFunspec :
    Cil.cilVisitor -> Cil_types.funspec -> Cil_types.funspec
  val visitCilBehavior :
    Cil.cilVisitor -> Cil_types.funbehavior -> Cil_types.funbehavior
  val visitCilBehaviors :
    Cil.cilVisitor ->
    Cil_types.funbehavior list -> Cil_types.funbehavior list
  val visitCilExtended :
    Cil.cilVisitor -> Cil_types.acsl_extension -> Cil_types.acsl_extension
  val visitCilModelInfo :
    Cil.cilVisitor -> Cil_types.model_info -> Cil_types.model_info
  val visitCilLogicType :
    Cil.cilVisitor -> Cil_types.logic_type -> Cil_types.logic_type
  val visitCilIdPredicate :
    Cil.cilVisitor ->
    Cil_types.identified_predicate -> Cil_types.identified_predicate
  val visitCilPredicateNode :
    Cil.cilVisitor -> Cil_types.predicate_node -> Cil_types.predicate_node
  val visitCilPredicate :
    Cil.cilVisitor -> Cil_types.predicate -> Cil_types.predicate
  val visitCilPredicates :
    Cil.cilVisitor ->
    Cil_types.identified_predicate list ->
    Cil_types.identified_predicate list
  val visitCilTerm : Cil.cilVisitor -> Cil_types.term -> Cil_types.term
  val visitCilIdTerm :
    Cil.cilVisitor -> Cil_types.identified_term -> Cil_types.identified_term
  val visitCilTermLval :
    Cil.cilVisitor -> Cil_types.term_lval -> Cil_types.term_lval
  val visitCilTermLhost :
    Cil.cilVisitor -> Cil_types.term_lhost -> Cil_types.term_lhost
  val visitCilTermOffset :
    Cil.cilVisitor -> Cil_types.term_offset -> Cil_types.term_offset
  val visitCilLogicInfo :
    Cil.cilVisitor -> Cil_types.logic_info -> Cil_types.logic_info
  val visitCilLogicVarUse :
    Cil.cilVisitor -> Cil_types.logic_var -> Cil_types.logic_var
  val visitCilLogicVarDecl :
    Cil.cilVisitor -> Cil_types.logic_var -> Cil_types.logic_var
  val childrenBehavior :
    Cil.cilVisitor -> Cil_types.funbehavior -> Cil_types.funbehavior
  val is_skip : Cil_types.stmtkind -> bool
  val constFoldVisitor : bool -> Cil.cilVisitor
  module CurrentLoc :
    sig
      val self : State.t
      val name : string
      val mark_as_computed : ?project:Project.t -> unit -> unit
      val is_computed : ?project:Project.t -> unit -> bool
      module Datatype : Datatype.S
      val add_hook_on_update : (Datatype.t -> unit) -> unit
      val howto_marshal : (Datatype.t -> 'a) -> ('-> Datatype.t) -> unit
      type data = Cil_types.location
      val set : data -> unit
      val get : unit -> data
      val clear : unit -> unit
    end
  val pp_thisloc : Format.formatter -> unit
  val empty_funspec : unit -> Cil_types.funspec
  val is_empty_funspec : Cil_types.funspec -> bool
  val is_empty_behavior : Cil_types.funbehavior -> bool
  val uniqueVarNames : Cil_types.file -> unit
  val peepHole2 :
    aggressive:bool ->
    (Cil_types.stmt * Cil_types.stmt -> Cil_types.stmt list option) ->
    Cil_types.stmt list -> Cil_types.stmt list
  val peepHole1 :
    (Cil_types.instr -> Cil_types.instr list option) ->
    Cil_types.stmt list -> unit
  exception SizeOfError of string * Cil_types.typ
  val empty_size_cache : unit -> Cil_types.bitsSizeofTypCache
  val unsignedVersionOf : Cil_types.ikind -> Cil_types.ikind
  val intKindForSize : int -> bool -> Cil_types.ikind
  val floatKindForSize : int -> Cil_types.fkind
  val bitsSizeOf : Cil_types.typ -> int
  val bytesSizeOf : Cil_types.typ -> int
  val bytesSizeOfInt : Cil_types.ikind -> int
  val bitsSizeOfInt : Cil_types.ikind -> int
  val isSigned : Cil_types.ikind -> bool
  val bitsSizeOfBitfield : Cil_types.typ -> int
  val rank : Cil_types.ikind -> int
  val intTypeIncluded : Cil_types.ikind -> Cil_types.ikind -> bool
  val frank : Cil_types.fkind -> int
  val truncateInteger64 : Cil_types.ikind -> Integer.t -> Integer.t * bool
  val max_signed_number : int -> Integer.t
  val min_signed_number : int -> Integer.t
  val max_unsigned_number : int -> Integer.t
  val fitsInInt : Cil_types.ikind -> Integer.t -> bool
  val isFiniteFloat : Cil_types.fkind -> float -> bool
  val isExactFloat : Cil_types.fkind -> Cil_types.logic_real -> bool
  exception Not_representable
  val intKindForValue : Integer.t -> bool -> Cil_types.ikind
  val sizeOf : loc:Cil_types.location -> Cil_types.typ -> Cil_types.exp
  val bytesAlignOf : Cil_types.typ -> int
  val intOfAttrparam : Cil_types.attrparam -> int option
  val bitsOffset : Cil_types.typ -> Cil_types.offset -> int * int
  val mapNoCopy : ('-> 'a) -> 'a list -> 'a list
  val optMapNoCopy : ('-> 'a) -> 'a option -> 'a option
  val mapNoCopyList : ('-> 'a list) -> 'a list -> 'a list
  val startsWith : string -> string -> bool
  type formatArg =
      Fe of Cil_types.exp
    | Feo of Cil_types.exp option
    | Fu of Cil_types.unop
    | Fb of Cil_types.binop
    | Fk of Cil_types.ikind
    | FE of Cil_types.exp list
    | Ff of (string * Cil_types.typ * Cil_types.attributes)
    | FF of (string * Cil_types.typ * Cil_types.attributes) list
    | Fva of bool
    | Fv of Cil_types.varinfo
    | Fl of Cil_types.lval
    | Flo of Cil_types.lval option
    | Fo of Cil_types.offset
    | Fc of Cil_types.compinfo
    | Fi of Cil_types.instr
    | FI of Cil_types.instr list
    | Ft of Cil_types.typ
    | Fd of int
    | Fg of string
    | Fs of Cil_types.stmt
    | FS of Cil_types.stmt list
    | FA of Cil_types.attributes
    | Fp of Cil_types.attrparam
    | FP of Cil_types.attrparam list
    | FX of string
  val d_formatarg : Format.formatter -> Cil.formatArg -> unit
  val stmt_of_instr_list :
    ?loc:Cil_types.location -> Cil_types.instr list -> Cil_types.stmtkind
  val cvar_to_lvar : Cil_types.varinfo -> Cil_types.logic_var
  val make_temp_logic_var : Cil_types.logic_type -> Cil_types.logic_var
  val lzero : ?loc:Cil_types.location -> unit -> Cil_types.term
  val lone : ?loc:Cil_types.location -> unit -> Cil_types.term
  val lmone : ?loc:Cil_types.location -> unit -> Cil_types.term
  val lconstant : ?loc:Cil_types.location -> Integer.t -> Cil_types.term
  val close_predicate : Cil_types.predicate -> Cil_types.predicate
  val extract_varinfos_from_exp : Cil_types.exp -> Cil_datatype.Varinfo.Set.t
  val extract_varinfos_from_lval :
    Cil_types.lval -> Cil_datatype.Varinfo.Set.t
  val extract_free_logicvars_from_term :
    Cil_types.term -> Cil_datatype.Logic_var.Set.t
  val extract_free_logicvars_from_predicate :
    Cil_types.predicate -> Cil_datatype.Logic_var.Set.t
  val extract_labels_from_annot :
    Cil_types.code_annotation -> Cil_datatype.Logic_label.Set.t
  val extract_labels_from_term :
    Cil_types.term -> Cil_datatype.Logic_label.Set.t
  val extract_labels_from_pred :
    Cil_types.predicate -> Cil_datatype.Logic_label.Set.t
  val extract_stmts_from_labels :
    Cil_datatype.Logic_label.Set.t -> Cil_datatype.Stmt.Set.t
  val create_alpha_renaming :
    Cil_types.varinfo list -> Cil_types.varinfo list -> Cil.cilVisitor
  val separate_switch_succs :
    Cil_types.stmt -> Cil_types.stmt list * Cil_types.stmt
  val separate_if_succs : Cil_types.stmt -> Cil_types.stmt * Cil_types.stmt
  val dependency_on_ast : State.t -> unit
  val set_dependencies_of_ast : State.t -> unit
  val pp_typ_ref : (Format.formatter -> Cil_types.typ -> unit) Pervasives.ref
  val pp_global_ref :
    (Format.formatter -> Cil_types.global -> unit) Pervasives.ref
  val pp_exp_ref : (Format.formatter -> Cil_types.exp -> unit) Pervasives.ref
  val pp_lval_ref :
    (Format.formatter -> Cil_types.lval -> unit) Pervasives.ref
  val pp_ikind_ref :
    (Format.formatter -> Cil_types.ikind -> unit) Pervasives.ref
  val pp_attribute_ref :
    (Format.formatter -> Cil_types.attribute -> unit) Pervasives.ref
  val pp_attributes_ref :
    (Format.formatter -> Cil_types.attribute list -> unit) Pervasives.ref
  val set_extension_handler :
    visit:(string ->
           Cil.cilVisitor ->
           Cil_types.acsl_extension_kind ->
           Cil_types.acsl_extension_kind Cil.visitAction) ->
    unit
  val set_deprecated_extension_handler :
    handler:(string ->
             Cil_types.ext_category ->
             (Cil.cilVisitor ->
              Cil_types.acsl_extension_kind ->
              Cil_types.acsl_extension_kind Cil.visitAction) ->
             unit) ->
    unit
end