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) -> ('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) -> 'a -> 'a
val fold_sorted :
?cmp:(key -> key -> int) -> (key -> data -> 'a -> 'a) -> '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
type lineDirectiveStyle =
LineComment
| LineCommentSparse
| LinePreprocessorInput
| LinePreprocessorOutput
type miscState = {
mutable lineDirectiveStyle : Cil.lineDirectiveStyle option;
mutable print_CIL_Input : bool;
mutable printCilAsIs : bool;
mutable lineLength : int;
mutable warnTruncate : bool;
}
val miscState : Cil.miscState
type featureDescr = {
fd_enabled : bool Pervasives.ref;
fd_name : string;
fd_description : string;
fd_extraopt : (string * Arg.spec * string) list;
fd_doit : Cil_types.file -> unit;
fd_post_check : 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 -> ('a -> Cil_types.global -> 'a) -> '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 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) -> ('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) -> 'a -> 'a
val fold_sorted :
?cmp:(key -> key -> int) -> (key -> data -> 'a -> 'a) -> '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 -> 'a) ->
ct:Cil_types.typ ->
initl:(Cil_types.offset * Cil_types.init) list -> acc:'a -> '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 : Cil_types.compinfo -> string -> Cil_types.compinfo
val missingFieldName : string
val compFullName : Cil_types.compinfo -> string
val isCompleteType : 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 -> 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 ->
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 lastTermOffset : Cil_types.term_offset -> Cil_types.term_offset
val addTermOffsetLval :
Cil_types.term_offset -> Cil_types.term_lval -> Cil_types.term_lval
val addTermOffset :
Cil_types.term_offset -> Cil_types.term_offset -> Cil_types.term_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 compareExp : Cil_types.exp -> Cil_types.exp -> bool
val compareLval : Cil_types.lval -> Cil_types.lval -> bool
val compareOffset : Cil_types.offset -> Cil_types.offset -> 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 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 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 Pervasives.ref list)
list -> Cil_types.block
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 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 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 -> 'a)
| JustCopy
| JustCopyPost of ('a -> 'a)
| ChangeTo of 'a
| ChangeToPost of 'a * ('a -> 'a)
| ChangeDoChildrenPost of 'a * ('a -> 'a)
val mk_behavior :
?name:string ->
?assumes:'a list ->
?requires:'a list ->
?post_cond:(Cil_types.termination_kind * 'a) list ->
?assigns:'b Cil_types.assigns ->
?allocation:'b Cil_types.allocation option ->
?extended:(string * int * 'a list) list ->
unit -> ('a, 'b) Cil_types.behavior
val default_behavior_name : string
val is_default_behavior : ('a, 'b) Cil_types.behavior -> bool
val find_default_behavior :
Cil_types.funspec -> Cil_types.funbehavior option
val find_default_requires : ('a, 'b) Cil_types.behavior list -> 'a list
type visitor_behavior
val inplace_visit : unit -> Cil.visitor_behavior
val copy_visit : Project.t -> Cil.visitor_behavior
val refresh_visit : Project.t -> Cil.visitor_behavior
val is_fresh_behavior : Cil.visitor_behavior -> bool
val is_copy_behavior : Cil.visitor_behavior -> bool
val reset_behavior_varinfo : Cil.visitor_behavior -> unit
val reset_behavior_compinfo : Cil.visitor_behavior -> unit
val reset_behavior_enuminfo : Cil.visitor_behavior -> unit
val reset_behavior_enumitem : Cil.visitor_behavior -> unit
val reset_behavior_typeinfo : Cil.visitor_behavior -> unit
val reset_behavior_stmt : Cil.visitor_behavior -> unit
val reset_behavior_logic_info : Cil.visitor_behavior -> unit
val reset_behavior_logic_type_info : Cil.visitor_behavior -> unit
val reset_behavior_fieldinfo : Cil.visitor_behavior -> unit
val reset_behavior_model_info : Cil.visitor_behavior -> unit
val reset_logic_var : Cil.visitor_behavior -> unit
val reset_behavior_kernel_function : Cil.visitor_behavior -> unit
val reset_behavior_fundec : Cil.visitor_behavior -> unit
val get_varinfo :
Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo
val get_compinfo :
Cil.visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo
val get_enuminfo :
Cil.visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo
val get_enumitem :
Cil.visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem
val get_typeinfo :
Cil.visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo
val get_stmt : Cil.visitor_behavior -> Cil_types.stmt -> Cil_types.stmt
val get_logic_info :
Cil.visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info
val get_logic_type_info :
Cil.visitor_behavior ->
Cil_types.logic_type_info -> Cil_types.logic_type_info
val get_fieldinfo :
Cil.visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo
val get_model_info :
Cil.visitor_behavior -> Cil_types.model_info -> Cil_types.model_info
val get_logic_var :
Cil.visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var
val get_kernel_function :
Cil.visitor_behavior ->
Cil_types.kernel_function -> Cil_types.kernel_function
val get_fundec :
Cil.visitor_behavior -> Cil_types.fundec -> Cil_types.fundec
val get_original_varinfo :
Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo
val get_original_compinfo :
Cil.visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo
val get_original_enuminfo :
Cil.visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo
val get_original_enumitem :
Cil.visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem
val get_original_typeinfo :
Cil.visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo
val get_original_stmt :
Cil.visitor_behavior -> Cil_types.stmt -> Cil_types.stmt
val get_original_logic_info :
Cil.visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info
val get_original_logic_type_info :
Cil.visitor_behavior ->
Cil_types.logic_type_info -> Cil_types.logic_type_info
val get_original_fieldinfo :
Cil.visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo
val get_original_model_info :
Cil.visitor_behavior -> Cil_types.model_info -> Cil_types.model_info
val get_original_logic_var :
Cil.visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var
val get_original_kernel_function :
Cil.visitor_behavior ->
Cil_types.kernel_function -> Cil_types.kernel_function
val get_original_fundec :
Cil.visitor_behavior -> Cil_types.fundec -> Cil_types.fundec
val set_varinfo :
Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo -> unit
val set_compinfo :
Cil.visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo -> unit
val set_enuminfo :
Cil.visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo -> unit
val set_enumitem :
Cil.visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem -> unit
val set_typeinfo :
Cil.visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo -> unit
val set_stmt :
Cil.visitor_behavior -> Cil_types.stmt -> Cil_types.stmt -> unit
val set_logic_info :
Cil.visitor_behavior ->
Cil_types.logic_info -> Cil_types.logic_info -> unit
val set_logic_type_info :
Cil.visitor_behavior ->
Cil_types.logic_type_info -> Cil_types.logic_type_info -> unit
val set_fieldinfo :
Cil.visitor_behavior ->
Cil_types.fieldinfo -> Cil_types.fieldinfo -> unit
val set_model_info :
Cil.visitor_behavior ->
Cil_types.model_info -> Cil_types.model_info -> unit
val set_logic_var :
Cil.visitor_behavior ->
Cil_types.logic_var -> Cil_types.logic_var -> unit
val set_kernel_function :
Cil.visitor_behavior ->
Cil_types.kernel_function -> Cil_types.kernel_function -> unit
val set_fundec :
Cil.visitor_behavior -> Cil_types.fundec -> Cil_types.fundec -> unit
val set_orig_varinfo :
Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo -> unit
val set_orig_compinfo :
Cil.visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo -> unit
val set_orig_enuminfo :
Cil.visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo -> unit
val set_orig_enumitem :
Cil.visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem -> unit
val set_orig_typeinfo :
Cil.visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo -> unit
val set_orig_stmt :
Cil.visitor_behavior -> Cil_types.stmt -> Cil_types.stmt -> unit
val set_orig_logic_info :
Cil.visitor_behavior ->
Cil_types.logic_info -> Cil_types.logic_info -> unit
val set_orig_logic_type_info :
Cil.visitor_behavior ->
Cil_types.logic_type_info -> Cil_types.logic_type_info -> unit
val set_orig_fieldinfo :
Cil.visitor_behavior ->
Cil_types.fieldinfo -> Cil_types.fieldinfo -> unit
val set_orig_model_info :
Cil.visitor_behavior ->
Cil_types.model_info -> Cil_types.model_info -> unit
val set_orig_logic_var :
Cil.visitor_behavior ->
Cil_types.logic_var -> Cil_types.logic_var -> unit
val set_orig_kernel_function :
Cil.visitor_behavior ->
Cil_types.kernel_function -> Cil_types.kernel_function -> unit
val set_orig_fundec :
Cil.visitor_behavior -> Cil_types.fundec -> Cil_types.fundec -> unit
val memo_varinfo :
Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo
val memo_compinfo :
Cil.visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo
val memo_enuminfo :
Cil.visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo
val memo_enumitem :
Cil.visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem
val memo_typeinfo :
Cil.visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo
val memo_stmt : Cil.visitor_behavior -> Cil_types.stmt -> Cil_types.stmt
val memo_logic_info :
Cil.visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info
val memo_logic_type_info :
Cil.visitor_behavior ->
Cil_types.logic_type_info -> Cil_types.logic_type_info
val memo_fieldinfo :
Cil.visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo
val memo_model_info :
Cil.visitor_behavior -> Cil_types.model_info -> Cil_types.model_info
val memo_logic_var :
Cil.visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var
val memo_kernel_function :
Cil.visitor_behavior ->
Cil_types.kernel_function -> Cil_types.kernel_function
val memo_fundec :
Cil.visitor_behavior -> Cil_types.fundec -> Cil_types.fundec
val iter_visitor_varinfo :
Cil.visitor_behavior ->
(Cil_types.varinfo -> Cil_types.varinfo -> unit) -> unit
val iter_visitor_compinfo :
Cil.visitor_behavior ->
(Cil_types.compinfo -> Cil_types.compinfo -> unit) -> unit
val iter_visitor_enuminfo :
Cil.visitor_behavior ->
(Cil_types.enuminfo -> Cil_types.enuminfo -> unit) -> unit
val iter_visitor_enumitem :
Cil.visitor_behavior ->
(Cil_types.enumitem -> Cil_types.enumitem -> unit) -> unit
val iter_visitor_typeinfo :
Cil.visitor_behavior ->
(Cil_types.typeinfo -> Cil_types.typeinfo -> unit) -> unit
val iter_visitor_stmt :
Cil.visitor_behavior ->
(Cil_types.stmt -> Cil_types.stmt -> unit) -> unit
val iter_visitor_logic_info :
Cil.visitor_behavior ->
(Cil_types.logic_info -> Cil_types.logic_info -> unit) -> unit
val iter_visitor_logic_type_info :
Cil.visitor_behavior ->
(Cil_types.logic_type_info -> Cil_types.logic_type_info -> unit) -> unit
val iter_visitor_fieldinfo :
Cil.visitor_behavior ->
(Cil_types.fieldinfo -> Cil_types.fieldinfo -> unit) -> unit
val iter_visitor_model_info :
Cil.visitor_behavior ->
(Cil_types.model_info -> Cil_types.model_info -> unit) -> unit
val iter_visitor_logic_var :
Cil.visitor_behavior ->
(Cil_types.logic_var -> Cil_types.logic_var -> unit) -> unit
val iter_visitor_kernel_function :
Cil.visitor_behavior ->
(Cil_types.kernel_function -> Cil_types.kernel_function -> unit) -> unit
val iter_visitor_fundec :
Cil.visitor_behavior ->
(Cil_types.fundec -> Cil_types.fundec -> unit) -> unit
val fold_visitor_varinfo :
Cil.visitor_behavior ->
(Cil_types.varinfo -> Cil_types.varinfo -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_compinfo :
Cil.visitor_behavior ->
(Cil_types.compinfo -> Cil_types.compinfo -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_enuminfo :
Cil.visitor_behavior ->
(Cil_types.enuminfo -> Cil_types.enuminfo -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_enumitem :
Cil.visitor_behavior ->
(Cil_types.enumitem -> Cil_types.enumitem -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_typeinfo :
Cil.visitor_behavior ->
(Cil_types.typeinfo -> Cil_types.typeinfo -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_stmt :
Cil.visitor_behavior ->
(Cil_types.stmt -> Cil_types.stmt -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_logic_info :
Cil.visitor_behavior ->
(Cil_types.logic_info -> Cil_types.logic_info -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_logic_type_info :
Cil.visitor_behavior ->
(Cil_types.logic_type_info -> Cil_types.logic_type_info -> 'a -> 'a) ->
'a -> 'a
val fold_visitor_fieldinfo :
Cil.visitor_behavior ->
(Cil_types.fieldinfo -> Cil_types.fieldinfo -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_model_info :
Cil.visitor_behavior ->
(Cil_types.model_info -> Cil_types.model_info -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_logic_var :
Cil.visitor_behavior ->
(Cil_types.logic_var -> Cil_types.logic_var -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_kernel_function :
Cil.visitor_behavior ->
(Cil_types.kernel_function -> Cil_types.kernel_function -> 'a -> 'a) ->
'a -> 'a
val fold_visitor_fundec :
Cil.visitor_behavior ->
(Cil_types.fundec -> Cil_types.fundec -> 'a -> 'a) -> 'a -> 'a
class type cilVisitor =
object
method behavior : Cil.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 : 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.identified_term Cil_types.allocation ->
Cil_types.identified_term Cil_types.allocation Cil.visitAction
method vannotation :
Cil_types.global_annotation ->
Cil_types.global_annotation Cil.visitAction
method vassigns :
Cil_types.identified_term Cil_types.assigns ->
Cil_types.identified_term 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.identified_term Cil_types.deps ->
Cil_types.identified_term 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.identified_term Cil_types.from ->
Cil_types.identified_term 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.term Cil_types.impact_pragma ->
Cil_types.term 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 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.term Cil_types.loop_pragma ->
Cil_types.term 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_named :
Cil_types.predicate Cil_types.named ->
Cil_types.predicate Cil_types.named Cil.visitAction
method vquantifiers :
Cil_types.quantifiers -> Cil_types.quantifiers Cil.visitAction
method vslice_pragma :
Cil_types.term Cil_types.slice_pragma ->
Cil_types.term 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 ->
int * Cil_types.identified_predicate list ->
(int * Cil_types.identified_predicate list) Cil.visitAction) ->
unit
class internal_genericCilVisitor :
Cil_types.fundec option Pervasives.ref ->
Cil.visitor_behavior -> (unit -> unit) Queue.t -> cilVisitor
class genericCilVisitor : Cil.visitor_behavior -> cilVisitor
class nopCilVisitor : cilVisitor
val doVisit :
'visitor ->
'visitor ->
('a -> 'a) ->
('a -> 'a Cil.visitAction) -> ('visitor -> 'a -> 'a) -> 'a -> 'a
val doVisitList :
'visitor ->
'visitor ->
('a -> 'a) ->
('a -> 'a list Cil.visitAction) ->
('visitor -> 'a -> 'a) -> '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 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 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.identified_term Cil_types.deps ->
Cil_types.identified_term Cil_types.deps
val visitCilFrom :
Cil.cilVisitor ->
Cil_types.identified_term Cil_types.from ->
Cil_types.identified_term Cil_types.from
val visitCilAssigns :
Cil.cilVisitor ->
Cil_types.identified_term Cil_types.assigns ->
Cil_types.identified_term 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.identified_term Cil_types.allocation ->
Cil_types.identified_term 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 ->
string * int * Cil_types.identified_predicate list ->
string * int * Cil_types.identified_predicate list
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 visitCilPredicate :
Cil.cilVisitor -> Cil_types.predicate -> Cil_types.predicate
val visitCilPredicateNamed :
Cil.cilVisitor ->
Cil_types.predicate Cil_types.named ->
Cil_types.predicate Cil_types.named
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
val forgcc : string -> string
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) -> ('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 currentGlobal : Cil_types.global Pervasives.ref
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 :
agressive: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 bitsOffset : Cil_types.typ -> Cil_types.offset -> int * int
val dExp : string -> Cil_types.exp
val dInstr : string -> Cil_types.location -> Cil_types.instr
val dGlobal : string -> Cil_types.location -> Cil_types.global
val mapNoCopy : ('a -> 'a) -> 'a list -> 'a list
val optMapNoCopy : ('a -> 'a) -> 'a option -> 'a option
val mapNoCopyList : ('a -> '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.named ->
Cil_types.predicate Cil_types.named
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_types.named -> 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_types.named -> 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
end