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 : 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 stripConstLocalType : Cil_types.typ -> Cil_types.typ
  val selfFormalsDecl : State.t
  val makeFormalsVarDecl :
    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 getGlobInit : ?main_name:string -> Cil_types.file -> Cil_types.fundec
  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
  module Sid : sig val next : unit -> int end
  module Eid : sig val next : unit -> int end
  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 ref ->
    variables:Cil_types.global list 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 mkCompInfo :
    bool ->
    string ->
    ?norig:string ->
    (Cil_types.compinfo ->
     (string * Cil_types.typ * int option * Cil_types.attributes *
      Cil_types.location)
     list) ->
    Cil_types.attributes -> Cil_types.compinfo
  val copyCompInfo :
    ?fresh:bool -> Cil_types.compinfo -> string -> Cil_types.compinfo
  val missingFieldName : string
  val compFullName : Cil_types.compinfo -> string
  val isCompleteType : ?allowZeroSizeArrays:bool -> 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 isCharType : Cil_types.typ -> bool
  val isShortType : Cil_types.typ -> bool
  val isCharPtrType : Cil_types.typ -> bool
  val isCharArrayType : Cil_types.typ -> bool
  val isIntegralType : Cil_types.typ -> bool
  val isIntegralOrPointerType : Cil_types.typ -> bool
  val isLogicIntegralType : 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 isPointerType : Cil_types.typ -> bool
  val isTypeTagType : Cil_types.logic_type -> bool
  val isFunctionType : Cil_types.typ -> 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 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 -> 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 ->
    bool -> bool -> string -> Cil_types.typ -> Cil_types.varinfo
  val makeFormalVar :
    Cil_types.fundec ->
    ?where:string -> string -> Cil_types.typ -> Cil_types.varinfo
  val makeLocalVar :
    Cil_types.fundec ->
    ?scope:Cil_types.block ->
    ?temp:bool ->
    ?insert:bool -> string -> Cil_types.typ -> Cil_types.varinfo
  val makeTempVar :
    Cil_types.fundec ->
    ?insert:bool ->
    ?name:string ->
    ?descr:string -> ?descrpure:bool -> Cil_types.typ -> Cil_types.varinfo
  val makeGlobalVar :
    ?source:bool ->
    ?temp:bool -> 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 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 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 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 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 -> 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 -> Cil_types.instr -> Cil_types.stmt
  val mkEmptyStmt :
    ?ghost:bool ->
    ?valid_sid:bool -> ?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 ->
    fundec:Cil_types.fundec ->
    ?loc:Cil_types.location -> Cil_types.exp -> Cil_types.stmt
  val mkWhile :
    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 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
  type attributeClass = AttrName of bool | AttrFunType of bool | AttrType
  val registerAttribute : string -> attributeClass -> unit
  val removeAttribute : string -> unit
  val attributeClass : string -> attributeClass
  val partitionAttributes :
    default: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 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 typeHasAttribute : string -> Cil_types.typ -> bool
  val typeHasQualifier : string -> Cil_types.typ -> bool
  val typeHasAttributeDeep : 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
  exception NotAnAttrParam of Cil_types.exp
  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.identified_term Cil_types.assigns ->
    ?allocation:Cil_types.identified_term 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
  type visitor_behavior
  val inplace_visit : unit -> visitor_behavior
  val copy_visit : Project.t -> visitor_behavior
  val refresh_visit : Project.t -> visitor_behavior
  val is_fresh_behavior : visitor_behavior -> bool
  val is_copy_behavior : visitor_behavior -> bool
  val reset_behavior_varinfo : visitor_behavior -> unit
  val reset_behavior_compinfo : visitor_behavior -> unit
  val reset_behavior_enuminfo : visitor_behavior -> unit
  val reset_behavior_enumitem : visitor_behavior -> unit
  val reset_behavior_typeinfo : visitor_behavior -> unit
  val reset_behavior_stmt : visitor_behavior -> unit
  val reset_behavior_logic_info : visitor_behavior -> unit
  val reset_behavior_logic_type_info : visitor_behavior -> unit
  val reset_behavior_fieldinfo : visitor_behavior -> unit
  val reset_behavior_model_info : visitor_behavior -> unit
  val reset_logic_var : visitor_behavior -> unit
  val reset_behavior_kernel_function : visitor_behavior -> unit
  val reset_behavior_fundec : visitor_behavior -> unit
  val get_varinfo :
    visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo
  val get_compinfo :
    visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo
  val get_enuminfo :
    visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo
  val get_enumitem :
    visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem
  val get_typeinfo :
    visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo
  val get_stmt : visitor_behavior -> Cil_types.stmt -> Cil_types.stmt
  val get_logic_info :
    visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info
  val get_logic_type_info :
    visitor_behavior ->
    Cil_types.logic_type_info -> Cil_types.logic_type_info
  val get_fieldinfo :
    visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo
  val get_model_info :
    visitor_behavior -> Cil_types.model_info -> Cil_types.model_info
  val get_logic_var :
    visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var
  val get_kernel_function :
    visitor_behavior ->
    Cil_types.kernel_function -> Cil_types.kernel_function
  val get_fundec : visitor_behavior -> Cil_types.fundec -> Cil_types.fundec
  val get_original_varinfo :
    visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo
  val get_original_compinfo :
    visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo
  val get_original_enuminfo :
    visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo
  val get_original_enumitem :
    visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem
  val get_original_typeinfo :
    visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo
  val get_original_stmt :
    visitor_behavior -> Cil_types.stmt -> Cil_types.stmt
  val get_original_logic_info :
    visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info
  val get_original_logic_type_info :
    visitor_behavior ->
    Cil_types.logic_type_info -> Cil_types.logic_type_info
  val get_original_fieldinfo :
    visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo
  val get_original_model_info :
    visitor_behavior -> Cil_types.model_info -> Cil_types.model_info
  val get_original_logic_var :
    visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var
  val get_original_kernel_function :
    visitor_behavior ->
    Cil_types.kernel_function -> Cil_types.kernel_function
  val get_original_fundec :
    visitor_behavior -> Cil_types.fundec -> Cil_types.fundec
  val set_varinfo :
    visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo -> unit
  val set_compinfo :
    visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo -> unit
  val set_enuminfo :
    visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo -> unit
  val set_enumitem :
    visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem -> unit
  val set_typeinfo :
    visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo -> unit
  val set_stmt : visitor_behavior -> Cil_types.stmt -> Cil_types.stmt -> unit
  val set_logic_info :
    visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info -> unit
  val set_logic_type_info :
    visitor_behavior ->
    Cil_types.logic_type_info -> Cil_types.logic_type_info -> unit
  val set_fieldinfo :
    visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo -> unit
  val set_model_info :
    visitor_behavior -> Cil_types.model_info -> Cil_types.model_info -> unit
  val set_logic_var :
    visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var -> unit
  val set_kernel_function :
    visitor_behavior ->
    Cil_types.kernel_function -> Cil_types.kernel_function -> unit
  val set_fundec :
    visitor_behavior -> Cil_types.fundec -> Cil_types.fundec -> unit
  val set_orig_varinfo :
    visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo -> unit
  val set_orig_compinfo :
    visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo -> unit
  val set_orig_enuminfo :
    visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo -> unit
  val set_orig_enumitem :
    visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem -> unit
  val set_orig_typeinfo :
    visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo -> unit
  val set_orig_stmt :
    visitor_behavior -> Cil_types.stmt -> Cil_types.stmt -> unit
  val set_orig_logic_info :
    visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info -> unit
  val set_orig_logic_type_info :
    visitor_behavior ->
    Cil_types.logic_type_info -> Cil_types.logic_type_info -> unit
  val set_orig_fieldinfo :
    visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo -> unit
  val set_orig_model_info :
    visitor_behavior -> Cil_types.model_info -> Cil_types.model_info -> unit
  val set_orig_logic_var :
    visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var -> unit
  val set_orig_kernel_function :
    visitor_behavior ->
    Cil_types.kernel_function -> Cil_types.kernel_function -> unit
  val set_orig_fundec :
    visitor_behavior -> Cil_types.fundec -> Cil_types.fundec -> unit
  val memo_varinfo :
    visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo
  val memo_compinfo :
    visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo
  val memo_enuminfo :
    visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo
  val memo_enumitem :
    visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem
  val memo_typeinfo :
    visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo
  val memo_stmt : visitor_behavior -> Cil_types.stmt -> Cil_types.stmt
  val memo_logic_info :
    visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info
  val memo_logic_type_info :
    visitor_behavior ->
    Cil_types.logic_type_info -> Cil_types.logic_type_info
  val memo_fieldinfo :
    visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo
  val memo_model_info :
    visitor_behavior -> Cil_types.model_info -> Cil_types.model_info
  val memo_logic_var :
    visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var
  val memo_kernel_function :
    visitor_behavior ->
    Cil_types.kernel_function -> Cil_types.kernel_function
  val memo_fundec : visitor_behavior -> Cil_types.fundec -> Cil_types.fundec
  val iter_visitor_varinfo :
    visitor_behavior ->
    (Cil_types.varinfo -> Cil_types.varinfo -> unit) -> unit
  val iter_visitor_compinfo :
    visitor_behavior ->
    (Cil_types.compinfo -> Cil_types.compinfo -> unit) -> unit
  val iter_visitor_enuminfo :
    visitor_behavior ->
    (Cil_types.enuminfo -> Cil_types.enuminfo -> unit) -> unit
  val iter_visitor_enumitem :
    visitor_behavior ->
    (Cil_types.enumitem -> Cil_types.enumitem -> unit) -> unit
  val iter_visitor_typeinfo :
    visitor_behavior ->
    (Cil_types.typeinfo -> Cil_types.typeinfo -> unit) -> unit
  val iter_visitor_stmt :
    visitor_behavior -> (Cil_types.stmt -> Cil_types.stmt -> unit) -> unit
  val iter_visitor_logic_info :
    visitor_behavior ->
    (Cil_types.logic_info -> Cil_types.logic_info -> unit) -> unit
  val iter_visitor_logic_type_info :
    visitor_behavior ->
    (Cil_types.logic_type_info -> Cil_types.logic_type_info -> unit) -> unit
  val iter_visitor_fieldinfo :
    visitor_behavior ->
    (Cil_types.fieldinfo -> Cil_types.fieldinfo -> unit) -> unit
  val iter_visitor_model_info :
    visitor_behavior ->
    (Cil_types.model_info -> Cil_types.model_info -> unit) -> unit
  val iter_visitor_logic_var :
    visitor_behavior ->
    (Cil_types.logic_var -> Cil_types.logic_var -> unit) -> unit
  val iter_visitor_kernel_function :
    visitor_behavior ->
    (Cil_types.kernel_function -> Cil_types.kernel_function -> unit) -> unit
  val iter_visitor_fundec :
    visitor_behavior ->
    (Cil_types.fundec -> Cil_types.fundec -> unit) -> unit
  val fold_visitor_varinfo :
    visitor_behavior ->
    (Cil_types.varinfo -> Cil_types.varinfo -> '-> 'a) -> '-> 'a
  val fold_visitor_compinfo :
    visitor_behavior ->
    (Cil_types.compinfo -> Cil_types.compinfo -> '-> 'a) -> '-> 'a
  val fold_visitor_enuminfo :
    visitor_behavior ->
    (Cil_types.enuminfo -> Cil_types.enuminfo -> '-> 'a) -> '-> 'a
  val fold_visitor_enumitem :
    visitor_behavior ->
    (Cil_types.enumitem -> Cil_types.enumitem -> '-> 'a) -> '-> 'a
  val fold_visitor_typeinfo :
    visitor_behavior ->
    (Cil_types.typeinfo -> Cil_types.typeinfo -> '-> 'a) -> '-> 'a
  val fold_visitor_stmt :
    visitor_behavior ->
    (Cil_types.stmt -> Cil_types.stmt -> '-> 'a) -> '-> 'a
  val fold_visitor_logic_info :
    visitor_behavior ->
    (Cil_types.logic_info -> Cil_types.logic_info -> '-> 'a) -> '-> 'a
  val fold_visitor_logic_type_info :
    visitor_behavior ->
    (Cil_types.logic_type_info -> Cil_types.logic_type_info -> '-> 'a) ->
    '-> 'a
  val fold_visitor_fieldinfo :
    visitor_behavior ->
    (Cil_types.fieldinfo -> Cil_types.fieldinfo -> '-> 'a) -> '-> 'a
  val fold_visitor_model_info :
    visitor_behavior ->
    (Cil_types.model_info -> Cil_types.model_info -> '-> 'a) -> '-> 'a
  val fold_visitor_logic_var :
    visitor_behavior ->
    (Cil_types.logic_var -> Cil_types.logic_var -> '-> 'a) -> '-> 'a
  val fold_visitor_kernel_function :
    visitor_behavior ->
    (Cil_types.kernel_function -> Cil_types.kernel_function -> '-> 'a) ->
    '-> 'a
  val fold_visitor_fundec :
    visitor_behavior ->
    (Cil_types.fundec -> Cil_types.fundec -> '-> 'a) -> '-> 'a
  class type cilVisitor =
    object
      method behavior : visitor_behavior
      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 : 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 visitAction
      method vallocation :
        Cil_types.identified_term Cil_types.allocation ->
        Cil_types.identified_term Cil_types.allocation visitAction
      method vannotation :
        Cil_types.global_annotation ->
        Cil_types.global_annotation visitAction
      method vassigns :
        Cil_types.identified_term Cil_types.assigns ->
        Cil_types.identified_term Cil_types.assigns visitAction
      method vattr :
        Cil_types.attribute -> Cil_types.attribute list visitAction
      method vattrparam :
        Cil_types.attrparam -> Cil_types.attrparam visitAction
      method vbehavior :
        Cil_types.funbehavior -> Cil_types.funbehavior visitAction
      method vblock : Cil_types.block -> Cil_types.block visitAction
      method vcode_annot :
        Cil_types.code_annotation -> Cil_types.code_annotation visitAction
      method vcompinfo : Cil_types.compinfo -> Cil_types.compinfo visitAction
      method vdeps :
        Cil_types.identified_term Cil_types.deps ->
        Cil_types.identified_term Cil_types.deps visitAction
      method venuminfo : Cil_types.enuminfo -> Cil_types.enuminfo visitAction
      method venumitem : Cil_types.enumitem -> Cil_types.enumitem visitAction
      method vexpr : Cil_types.exp -> Cil_types.exp visitAction
      method vfieldinfo :
        Cil_types.fieldinfo -> Cil_types.fieldinfo visitAction
      method vfile : Cil_types.file -> Cil_types.file visitAction
      method vfrees :
        Cil_types.identified_term list ->
        Cil_types.identified_term list visitAction
      method vfrom :
        Cil_types.identified_term Cil_types.from ->
        Cil_types.identified_term Cil_types.from visitAction
      method vfunc : Cil_types.fundec -> Cil_types.fundec visitAction
      method vglob : Cil_types.global -> Cil_types.global list visitAction
      method videntified_predicate :
        Cil_types.identified_predicate ->
        Cil_types.identified_predicate visitAction
      method videntified_term :
        Cil_types.identified_term -> Cil_types.identified_term visitAction
      method vimpact_pragma :
        Cil_types.term Cil_types.impact_pragma ->
        Cil_types.term Cil_types.impact_pragma visitAction
      method vinit :
        Cil_types.varinfo ->
        Cil_types.offset -> Cil_types.init -> Cil_types.init visitAction
      method vinitoffs : Cil_types.offset -> Cil_types.offset visitAction
      method vinst : Cil_types.instr -> Cil_types.instr list visitAction
      method vlocal_init :
        Cil_types.varinfo ->
        Cil_types.local_init -> Cil_types.local_init visitAction
      method vlogic_ctor_info_decl :
        Cil_types.logic_ctor_info -> Cil_types.logic_ctor_info visitAction
      method vlogic_ctor_info_use :
        Cil_types.logic_ctor_info -> Cil_types.logic_ctor_info visitAction
      method vlogic_info_decl :
        Cil_types.logic_info -> Cil_types.logic_info visitAction
      method vlogic_info_use :
        Cil_types.logic_info -> Cil_types.logic_info visitAction
      method vlogic_label :
        Cil_types.logic_label -> Cil_types.logic_label visitAction
      method vlogic_type :
        Cil_types.logic_type -> Cil_types.logic_type visitAction
      method vlogic_type_def :
        Cil_types.logic_type_def -> Cil_types.logic_type_def visitAction
      method vlogic_type_info_decl :
        Cil_types.logic_type_info -> Cil_types.logic_type_info visitAction
      method vlogic_type_info_use :
        Cil_types.logic_type_info -> Cil_types.logic_type_info visitAction
      method vlogic_var_decl :
        Cil_types.logic_var -> Cil_types.logic_var visitAction
      method vlogic_var_use :
        Cil_types.logic_var -> Cil_types.logic_var visitAction
      method vloop_pragma :
        Cil_types.term Cil_types.loop_pragma ->
        Cil_types.term Cil_types.loop_pragma visitAction
      method vlval : Cil_types.lval -> Cil_types.lval visitAction
      method vmodel_info :
        Cil_types.model_info -> Cil_types.model_info visitAction
      method voffs : Cil_types.offset -> Cil_types.offset visitAction
      method vpredicate :
        Cil_types.predicate -> Cil_types.predicate visitAction
      method vpredicate_node :
        Cil_types.predicate_node -> Cil_types.predicate_node visitAction
      method vquantifiers :
        Cil_types.quantifiers -> Cil_types.quantifiers visitAction
      method vslice_pragma :
        Cil_types.term Cil_types.slice_pragma ->
        Cil_types.term Cil_types.slice_pragma visitAction
      method vspec : Cil_types.funspec -> Cil_types.funspec visitAction
      method vstmt : Cil_types.stmt -> Cil_types.stmt visitAction
      method vterm : Cil_types.term -> Cil_types.term visitAction
      method vterm_lhost :
        Cil_types.term_lhost -> Cil_types.term_lhost visitAction
      method vterm_lval :
        Cil_types.term_lval -> Cil_types.term_lval visitAction
      method vterm_node :
        Cil_types.term_node -> Cil_types.term_node visitAction
      method vterm_offset :
        Cil_types.term_offset -> Cil_types.term_offset visitAction
      method vtype : Cil_types.typ -> Cil_types.typ visitAction
      method vvdec : Cil_types.varinfo -> Cil_types.varinfo visitAction
      method vvrbl : Cil_types.varinfo -> Cil_types.varinfo visitAction
    end
  val register_behavior_extension :
    string ->
    (cilVisitor ->
     Cil_types.acsl_extension_kind ->
     Cil_types.acsl_extension_kind visitAction) ->
    unit
  class internal_genericCilVisitor :
    Cil_types.fundec option ref ->
    visitor_behavior -> (unit -> unit) Queue.t -> cilVisitor
  class genericCilVisitor : visitor_behavior -> cilVisitor
  class nopCilVisitor : cilVisitor
  val doVisit :
    'visitor ->
    'visitor ->
    ('-> 'a) ->
    ('-> 'a visitAction) -> ('visitor -> '-> 'a) -> '-> 'a
  val doVisitList :
    'visitor ->
    'visitor ->
    ('-> 'a) ->
    ('-> 'a list visitAction) -> ('visitor -> '-> 'a) -> '-> 'a list
  val visitCilFileCopy : cilVisitor -> Cil_types.file -> Cil_types.file
  val visitCilFile : cilVisitor -> Cil_types.file -> unit
  val visitCilFileSameGlobals : cilVisitor -> Cil_types.file -> unit
  val visitCilGlobal :
    cilVisitor -> Cil_types.global -> Cil_types.global list
  val visitCilFunction : cilVisitor -> Cil_types.fundec -> Cil_types.fundec
  val visitCilExpr : cilVisitor -> Cil_types.exp -> Cil_types.exp
  val visitCilEnumInfo :
    cilVisitor -> Cil_types.enuminfo -> Cil_types.enuminfo
  val visitCilLval : cilVisitor -> Cil_types.lval -> Cil_types.lval
  val visitCilOffset : cilVisitor -> Cil_types.offset -> Cil_types.offset
  val visitCilInitOffset : cilVisitor -> Cil_types.offset -> Cil_types.offset
  val visitCilLocal_init :
    cilVisitor ->
    Cil_types.varinfo -> Cil_types.local_init -> Cil_types.local_init
  val visitCilInstr : cilVisitor -> Cil_types.instr -> Cil_types.instr list
  val visitCilStmt : cilVisitor -> Cil_types.stmt -> Cil_types.stmt
  val visitCilBlock : 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 : cilVisitor -> Cil_types.typ -> Cil_types.typ
  val visitCilVarDecl : cilVisitor -> Cil_types.varinfo -> Cil_types.varinfo
  val visitCilInit :
    cilVisitor ->
    Cil_types.varinfo -> Cil_types.offset -> Cil_types.init -> Cil_types.init
  val visitCilAttributes :
    cilVisitor -> Cil_types.attribute list -> Cil_types.attribute list
  val visitCilAnnotation :
    cilVisitor -> Cil_types.global_annotation -> Cil_types.global_annotation
  val visitCilCodeAnnotation :
    cilVisitor -> Cil_types.code_annotation -> Cil_types.code_annotation
  val visitCilDeps :
    cilVisitor ->
    Cil_types.identified_term Cil_types.deps ->
    Cil_types.identified_term Cil_types.deps
  val visitCilFrom :
    cilVisitor ->
    Cil_types.identified_term Cil_types.from ->
    Cil_types.identified_term Cil_types.from
  val visitCilAssigns :
    cilVisitor ->
    Cil_types.identified_term Cil_types.assigns ->
    Cil_types.identified_term Cil_types.assigns
  val visitCilFrees :
    cilVisitor ->
    Cil_types.identified_term list -> Cil_types.identified_term list
  val visitCilAllocates :
    cilVisitor ->
    Cil_types.identified_term list -> Cil_types.identified_term list
  val visitCilAllocation :
    cilVisitor ->
    Cil_types.identified_term Cil_types.allocation ->
    Cil_types.identified_term Cil_types.allocation
  val visitCilFunspec : cilVisitor -> Cil_types.funspec -> Cil_types.funspec
  val visitCilBehavior :
    cilVisitor -> Cil_types.funbehavior -> Cil_types.funbehavior
  val visitCilBehaviors :
    cilVisitor -> Cil_types.funbehavior list -> Cil_types.funbehavior list
  val visitCilExtended :
    cilVisitor -> Cil_types.acsl_extension -> Cil_types.acsl_extension
  val visitCilModelInfo :
    cilVisitor -> Cil_types.model_info -> Cil_types.model_info
  val visitCilLogicType :
    cilVisitor -> Cil_types.logic_type -> Cil_types.logic_type
  val visitCilIdPredicate :
    cilVisitor ->
    Cil_types.identified_predicate -> Cil_types.identified_predicate
  val visitCilPredicateNode :
    cilVisitor -> Cil_types.predicate_node -> Cil_types.predicate_node
  val visitCilPredicate :
    cilVisitor -> Cil_types.predicate -> Cil_types.predicate
  val visitCilPredicates :
    cilVisitor ->
    Cil_types.identified_predicate list ->
    Cil_types.identified_predicate list
  val visitCilTerm : cilVisitor -> Cil_types.term -> Cil_types.term
  val visitCilIdTerm :
    cilVisitor -> Cil_types.identified_term -> Cil_types.identified_term
  val visitCilTermLval :
    cilVisitor -> Cil_types.term_lval -> Cil_types.term_lval
  val visitCilTermLhost :
    cilVisitor -> Cil_types.term_lhost -> Cil_types.term_lhost
  val visitCilTermOffset :
    cilVisitor -> Cil_types.term_offset -> Cil_types.term_offset
  val visitCilLogicInfo :
    cilVisitor -> Cil_types.logic_info -> Cil_types.logic_info
  val visitCilLogicVarUse :
    cilVisitor -> Cil_types.logic_var -> Cil_types.logic_var
  val visitCilLogicVarDecl :
    cilVisitor -> Cil_types.logic_var -> Cil_types.logic_var
  val childrenBehavior :
    cilVisitor -> Cil_types.funbehavior -> Cil_types.funbehavior
  val is_skip : Cil_types.stmtkind -> bool
  val constFoldVisitor : bool -> 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 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
  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 -> 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 -> 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) ref
  val pp_global_ref : (Format.formatter -> Cil_types.global -> unit) ref
  val pp_exp_ref : (Format.formatter -> Cil_types.exp -> unit) ref
  val pp_lval_ref : (Format.formatter -> Cil_types.lval -> unit) ref
  val pp_ikind_ref : (Format.formatter -> Cil_types.ikind -> unit) ref
  val pp_attribute_ref :
    (Format.formatter -> Cil_types.attribute -> unit) ref
  val pp_attributes_ref :
    (Format.formatter -> Cil_types.attribute list -> unit) ref
  val ptrType : Cil_types.typ -> Cil_types.typ
  val constPtrType : Cil_types.typ -> Cil_types.typ
  val shortType : Cil_types.typ
  val ushortType : Cil_types.typ
  val shortPtrType : Cil_types.typ
  val ushortPtrType : Cil_types.typ
  val longPtrType : Cil_types.typ
  val ulongPtrType : Cil_types.typ
  val longlongPtrType : Cil_types.typ
  val ulonglongPtrType : Cil_types.typ
  val doublePtrType : Cil_types.typ
  val is_folded_zero : Cil_types.exp -> bool
  val signedIntegerTypes : Cil_types.typ list
  val unsignedIntegerTypes : Cil_types.typ list
  val signedIntegerPtrTypes : Cil_types.typ list
  val unsignedIntegerPtrTypes : Cil_types.typ list
  val is_signed_integer_type : Cil_types.typ -> bool
  val is_unsigned_integer_type : Cil_types.typ -> bool
  val is_integer_type : Cil_types.typ -> bool
  val is_integer_ptr_type : Cil_types.typ -> bool
  val is_function : Cil_types.varinfo -> bool
  val is_variadic_function : Cil_types.varinfo -> bool
  val static_string : Cil_types.exp -> string option
  val get_fundec_return_type : Cil_types.fundec -> Cil_types.typ
  val get_kf_attributes : Cil_types.kernel_function -> Cil_types.attributes
  val integer_ranking_comp : Cil_types.typ -> Cil_types.typ -> int
  val integer_promotion : Cil_types.typ -> Cil_types.typ -> bool
  val get_inst_loc : Cil_types.instr -> Cil_types.location
  val get_stmt_loc : Cil_types.stmt -> Cil_types.location
end