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 : theMachine
val selfMachine : State.t
val selfMachine_is_computed : ?project:Project.project -> unit -> bool
val msvcMode : unit -> bool
val gccMode : unit -> bool
val emptyFunctionFromVI : Cil_types.varinfo -> Cil_types.fundec
val emptyFunction : string -> Cil_types.fundec
val setFormals : Cil_types.fundec -> Cil_types.varinfo list -> unit
val getReturnType : Cil_types.typ -> Cil_types.typ
val setReturnTypeVI : Cil_types.varinfo -> Cil_types.typ -> unit
val setReturnType : Cil_types.fundec -> Cil_types.typ -> unit
val setFunctionType : Cil_types.fundec -> Cil_types.typ -> unit
val setFunctionTypeMakeFormals : Cil_types.fundec -> Cil_types.typ -> unit
val setMaxId : Cil_types.fundec -> unit
val selfFormalsDecl : State.t
val makeFormalsVarDecl :
?ghost:bool ->
string * Cil_types.typ * Cil_types.attributes -> Cil_types.varinfo
val setFormalsDecl : Cil_types.varinfo -> Cil_types.typ -> unit
val removeFormalsDecl : Cil_types.varinfo -> unit
val unsafeSetFormalsDecl :
Cil_types.varinfo -> Cil_types.varinfo list -> unit
val iterFormalsDecl :
(Cil_types.varinfo -> Cil_types.varinfo list -> unit) -> unit
val getFormalsDecl : Cil_types.varinfo -> Cil_types.varinfo list
val dummyFile : Cil_types.file
val iterGlobals : Cil_types.file -> (Cil_types.global -> unit) -> unit
val foldGlobals :
Cil_types.file -> ('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
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) -> ('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 missingFieldName : string
val compFullName : Cil_types.compinfo -> string
val isCompleteType : ?allowZeroSizeArrays:bool -> Cil_types.typ -> bool
val has_flexible_array_member : Cil_types.typ -> bool
val unrollType : Cil_types.typ -> Cil_types.typ
val unrollTypeDeep : Cil_types.typ -> Cil_types.typ
val separateStorageModifiers :
Cil_types.attribute list ->
Cil_types.attribute list * Cil_types.attribute list
val arithmeticConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ
val integralPromotion : Cil_types.typ -> Cil_types.typ
val isAnyCharType : Cil_types.typ -> bool
val isCharType : Cil_types.typ -> bool
val isShortType : Cil_types.typ -> bool
val isAnyCharPtrType : Cil_types.typ -> bool
val isCharPtrType : Cil_types.typ -> bool
val isCharConstPtrType : Cil_types.typ -> bool
val isAnyCharArrayType : Cil_types.typ -> bool
val isCharArrayType : Cil_types.typ -> bool
val isIntegralType : Cil_types.typ -> bool
val isBoolType : Cil_types.typ -> bool
val isLogicPureBooleanType : Cil_types.logic_type -> bool
val isIntegralOrPointerType : Cil_types.typ -> bool
val isLogicIntegralType : Cil_types.logic_type -> bool
val isLogicBooleanType : Cil_types.logic_type -> bool
val isFloatingType : Cil_types.typ -> bool
val isLogicFloatType : Cil_types.logic_type -> bool
val isLogicRealOrFloatType : Cil_types.logic_type -> bool
val isLogicRealType : Cil_types.logic_type -> bool
val isArithmeticType : Cil_types.typ -> bool
val isScalarType : Cil_types.typ -> bool
val isArithmeticOrPointerType : Cil_types.typ -> bool
val isLogicArithmeticType : Cil_types.logic_type -> bool
val isFunctionType : Cil_types.typ -> bool
val isLogicFunctionType : Cil_types.logic_type -> bool
val isPointerType : Cil_types.typ -> bool
val isFunPtrType : Cil_types.typ -> bool
val isLogicFunPtrType : Cil_types.logic_type -> bool
val isTypeTagType : Cil_types.logic_type -> bool
val isVariadicListType : Cil_types.typ -> bool
val argsToList :
(string * Cil_types.typ * Cil_types.attributes) list option ->
(string * Cil_types.typ * Cil_types.attributes) list
val argsToPairOfLists :
(string * Cil_types.typ * Cil_types.attributes) list option ->
(string * Cil_types.typ * Cil_types.attributes) list *
(string * Cil_types.typ * Cil_types.attributes) list
val isArrayType : Cil_types.typ -> bool
val isStructOrUnionType : Cil_types.typ -> bool
exception LenOfArray
val lenOfArray : Cil_types.exp option -> int
val lenOfArray64 : Cil_types.exp option -> Integer.t
val getCompField : Cil_types.compinfo -> string -> Cil_types.fieldinfo
type existsAction = ExistsTrue | ExistsFalse | ExistsMaybe
val existsType : (Cil_types.typ -> existsAction) -> Cil_types.typ -> bool
val splitFunctionType :
Cil_types.typ ->
Cil_types.typ *
(string * Cil_types.typ * Cil_types.attributes) list option * bool *
Cil_types.attributes
val splitFunctionTypeVI :
Cil_types.varinfo ->
Cil_types.typ *
(string * Cil_types.typ * Cil_types.attributes) list option * bool *
Cil_types.attributes
val makeVarinfo :
?source:bool ->
?temp:bool ->
?referenced:bool ->
?ghost:bool ->
?loc:Cil_datatype.Location.t ->
bool -> bool -> string -> Cil_types.typ -> Cil_types.varinfo
val makeFormalVar :
Cil_types.fundec ->
?ghost:bool ->
?where:string ->
?loc:Cil_datatype.Location.t ->
string -> Cil_types.typ -> Cil_types.varinfo
val makeLocalVar :
Cil_types.fundec ->
?scope:Cil_types.block ->
?temp:bool ->
?referenced:bool ->
?insert:bool ->
?ghost:bool ->
?loc:Cil_datatype.Location.t ->
string -> Cil_types.typ -> Cil_types.varinfo
val refresh_local_name : Cil_types.fundec -> Cil_types.varinfo -> unit
val makeTempVar :
Cil_types.fundec ->
?insert:bool ->
?ghost:bool ->
?name:string ->
?descr:string ->
?descrpure:bool ->
?loc:Cil_datatype.Location.t -> Cil_types.typ -> Cil_types.varinfo
val makeGlobalVar :
?source:bool ->
?temp:bool ->
?referenced:bool ->
?ghost:bool ->
?loc:Cil_datatype.Location.t ->
string -> Cil_types.typ -> Cil_types.varinfo
val copyVarinfo : Cil_types.varinfo -> string -> Cil_types.varinfo
val update_var_type : Cil_types.varinfo -> Cil_types.typ -> unit
val isBitfield : Cil_types.lval -> bool
val lastOffset : Cil_types.offset -> Cil_types.offset
val addOffsetLval : Cil_types.offset -> Cil_types.lval -> Cil_types.lval
val addOffset : Cil_types.offset -> Cil_types.offset -> Cil_types.offset
val removeOffsetLval : Cil_types.lval -> Cil_types.lval * Cil_types.offset
val removeOffset : Cil_types.offset -> Cil_types.offset * Cil_types.offset
val typeOfLval : Cil_types.lval -> Cil_types.typ
val typeOfLhost : Cil_types.lhost -> Cil_types.typ
val typeOfTermLval : Cil_types.term_lval -> Cil_types.logic_type
val typeOffset : Cil_types.typ -> Cil_types.offset -> Cil_types.typ
val typeTermOffset :
Cil_types.logic_type -> Cil_types.term_offset -> Cil_types.logic_type
val typeOfInit : Cil_types.init -> Cil_types.typ
val is_modifiable_lval : Cil_types.lval -> bool
val zero : loc:Cil_datatype.Location.t -> Cil_types.exp
val one : loc:Cil_datatype.Location.t -> Cil_types.exp
val mone : loc:Cil_datatype.Location.t -> Cil_types.exp
val kinteger64 :
loc:Cil_types.location ->
?repr:string -> ?kind:Cil_types.ikind -> Integer.t -> Cil_types.exp
val kinteger :
loc:Cil_types.location -> Cil_types.ikind -> int -> Cil_types.exp
val integer : loc:Cil_types.location -> int -> Cil_types.exp
val kfloat :
loc:Cil_types.location -> Cil_types.fkind -> float -> Cil_types.exp
val isInteger : Cil_types.exp -> Integer.t option
val isConstant : Cil_types.exp -> bool
val isIntegerConstant : Cil_types.exp -> bool
val isConstantOffset : Cil_types.offset -> bool
val isZero : Cil_types.exp -> bool
val isLogicZero : Cil_types.term -> bool
val isLogicNull : Cil_types.term -> bool
val no_op_coerce : Cil_types.logic_type -> Cil_types.term -> bool
val reduce_multichar : Cil_types.typ -> int64 list -> int64
val interpret_character_constant :
int64 list -> Cil_types.constant * Cil_types.typ
val charConstToInt : char -> Integer.t
val charConstToIntConstant : char -> Cil_types.constant
val constFold : bool -> Cil_types.exp -> Cil_types.exp
val constFoldToInt : ?machdep:bool -> Cil_types.exp -> Integer.t option
val constFoldTermNodeAtTop : Cil_types.term_node -> Cil_types.term_node
val constFoldTerm : bool -> Cil_types.term -> Cil_types.term
val constFoldOffset : bool -> Cil_types.offset -> Cil_types.offset
val constFoldBinOp :
loc:Cil_types.location ->
bool ->
Cil_types.binop ->
Cil_types.exp -> Cil_types.exp -> Cil_types.typ -> Cil_types.exp
val compareConstant : Cil_types.constant -> Cil_types.constant -> bool
val increm : Cil_types.exp -> int -> Cil_types.exp
val increm64 : Cil_types.exp -> Integer.t -> Cil_types.exp
val var : Cil_types.varinfo -> Cil_types.lval
val evar : ?loc:Cil_types.location -> Cil_types.varinfo -> Cil_types.exp
val mkAddrOf : loc:Cil_types.location -> Cil_types.lval -> Cil_types.exp
val mkAddrOfVi : Cil_types.varinfo -> Cil_types.exp
val mkAddrOrStartOf :
loc:Cil_types.location -> Cil_types.lval -> Cil_types.exp
val mkMem : addr:Cil_types.exp -> off:Cil_types.offset -> Cil_types.lval
val mkBinOp :
loc:Cil_types.location ->
Cil_types.binop -> Cil_types.exp -> Cil_types.exp -> Cil_types.exp
val mkBinOp_safe_ptr_cmp :
loc:Cil_types.location ->
Cil_types.binop -> Cil_types.exp -> Cil_types.exp -> Cil_types.exp
val mkTermMem :
addr:Cil_types.term -> off:Cil_types.term_offset -> Cil_types.term_lval
val mkString : loc:Cil_types.location -> string -> Cil_types.exp
val need_cast : ?force:bool -> Cil_types.typ -> Cil_types.typ -> bool
val mkCastT :
?force:bool ->
e:Cil_types.exp ->
oldt:Cil_types.typ -> newt:Cil_types.typ -> Cil_types.exp
val mkCast :
?force:bool -> e:Cil_types.exp -> newt:Cil_types.typ -> Cil_types.exp
val stripTermCasts : Cil_types.term -> Cil_types.term
val stripCasts : Cil_types.exp -> Cil_types.exp
val stripInfo : Cil_types.exp -> Cil_types.exp
val stripCastsAndInfo : Cil_types.exp -> Cil_types.exp
val stripCastsButLastInfo : Cil_types.exp -> Cil_types.exp
val exp_info_of_term : Cil_types.term -> Cil_types.exp_info
val term_of_exp_info :
Cil_types.location ->
Cil_types.term_node -> Cil_types.exp_info -> Cil_types.term
val map_under_info :
(Cil_types.exp -> Cil_types.exp) -> Cil_types.exp -> Cil_types.exp
val app_under_info : (Cil_types.exp -> unit) -> Cil_types.exp -> unit
val typeOf : Cil_types.exp -> Cil_types.typ
val typeOf_pointed : Cil_types.typ -> Cil_types.typ
val typeOf_array_elem : Cil_types.typ -> Cil_types.typ
val is_fully_arithmetic : Cil_types.typ -> bool
val parseInt : string -> Integer.t
val parseIntExp : loc:Cil_types.location -> string -> Cil_types.exp
val parseIntLogic : loc:Cil_types.location -> string -> Cil_types.term
val appears_in_expr : Cil_types.varinfo -> Cil_types.exp -> bool
val mkStmt :
?ghost:bool ->
?valid_sid:bool ->
?sattr:Cil_types.attributes -> Cil_types.stmtkind -> Cil_types.stmt
val mkStmtCfg :
before:bool ->
new_stmtkind:Cil_types.stmtkind ->
ref_stmt:Cil_types.stmt -> Cil_types.stmt
val mkBlock : Cil_types.stmt list -> Cil_types.block
val mkBlockNonScoping : Cil_types.stmt list -> Cil_types.block
val mkStmtCfgBlock : Cil_types.stmt list -> Cil_types.stmt
val mkStmtOneInstr :
?ghost:bool ->
?valid_sid:bool ->
?sattr:Cil_types.attributes -> Cil_types.instr -> Cil_types.stmt
val mkEmptyStmt :
?ghost:bool ->
?valid_sid:bool ->
?sattr:Cil_types.attributes ->
?loc:Cil_types.location -> unit -> Cil_types.stmt
val dummyInstr : Cil_types.instr
val dummyStmt : Cil_types.stmt
val mkPureExprInstr :
fundec:Cil_types.fundec ->
scope:Cil_types.block ->
?loc:Cil_types.location -> Cil_types.exp -> Cil_types.instr
val mkPureExpr :
?ghost:bool ->
?valid_sid:bool ->
fundec:Cil_types.fundec ->
?loc:Cil_types.location -> Cil_types.exp -> Cil_types.stmt
val mkLoop :
?sattr:Cil_types.attributes ->
guard:Cil_types.exp -> body:Cil_types.stmt list -> Cil_types.stmt list
val mkForIncr :
iter:Cil_types.varinfo ->
first:Cil_types.exp ->
stopat:Cil_types.exp ->
incr:Cil_types.exp -> body:Cil_types.stmt list -> Cil_types.stmt list
val mkFor :
start:Cil_types.stmt list ->
guard:Cil_types.exp ->
next:Cil_types.stmt list ->
body:Cil_types.stmt list -> Cil_types.stmt list
val block_from_unspecified_sequence :
(Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
Cil_types.lval list * Cil_types.stmt ref list)
list -> Cil_types.block
val treat_constructor_as_func :
(Cil_types.lval option ->
Cil_types.exp -> Cil_types.exp list -> Cil_types.location -> 'a) ->
Cil_types.varinfo ->
Cil_types.varinfo ->
Cil_types.exp list ->
Cil_types.constructor_kind -> Cil_types.location -> 'a
val find_def_stmt : Cil_types.block -> Cil_types.varinfo -> Cil_types.stmt
val has_extern_local_init : Cil_types.block -> bool
val is_ghost_else : Cil_types.block -> bool
type attributeClass = AttrName of bool | AttrFunType of bool | AttrType
val registerAttribute : string -> 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 frama_c_ghost_else : string
val frama_c_ghost_formal : string
val frama_c_init_obj : string
val frama_c_mutable : string
val frama_c_inlined : string
val is_mutable_or_initialized : Cil_types.lval -> bool
val isGhostFormalVarinfo : Cil_types.varinfo -> bool
val isGhostFormalVarDecl :
string * Cil_types.typ * Cil_types.attributes -> bool
val typeDeepDropAttributes : string list -> Cil_types.typ -> Cil_types.typ
val typeDeepDropAllAttributes : Cil_types.typ -> Cil_types.typ
val filterAttributes :
string -> Cil_types.attributes -> Cil_types.attributes
val hasAttribute : string -> Cil_types.attributes -> bool
val mkAttrAnnot : string -> string
val attributeName : Cil_types.attribute -> string
val findAttribute :
string -> Cil_types.attribute list -> Cil_types.attrparam list
val typeAttrs : Cil_types.typ -> Cil_types.attribute list
val typeAttr : Cil_types.typ -> Cil_types.attribute list
val setTypeAttrs : Cil_types.typ -> Cil_types.attributes -> Cil_types.typ
val typeAddAttributes :
Cil_types.attribute list -> Cil_types.typ -> Cil_types.typ
val typeRemoveAttributes : string list -> Cil_types.typ -> Cil_types.typ
val typeRemoveAllAttributes : Cil_types.typ -> Cil_types.typ
val typeRemoveAttributesDeep :
string list -> Cil_types.typ -> Cil_types.typ
val typeHasAttribute : string -> Cil_types.typ -> bool
val typeHasQualifier : string -> Cil_types.typ -> bool
val typeHasAttributeDeep : string -> Cil_types.typ -> bool
val typeHasAttributeMemoryBlock : string -> Cil_types.typ -> bool
val type_remove_qualifier_attributes : Cil_types.typ -> Cil_types.typ
val type_remove_qualifier_attributes_deep : Cil_types.typ -> Cil_types.typ
val type_remove_attributes_for_c_cast : Cil_types.typ -> Cil_types.typ
val type_remove_attributes_for_logic_type : Cil_types.typ -> Cil_types.typ
val filter_qualifier_attributes :
Cil_types.attributes -> Cil_types.attributes
val splitArrayAttributes :
Cil_types.attributes -> Cil_types.attributes * Cil_types.attributes
val bitfield_attribute_name : string
val expToAttrParam : Cil_types.exp -> Cil_types.attrparam
val global_annotation_attributes :
Cil_types.global_annotation -> Cil_types.attributes
val global_attributes : Cil_types.global -> Cil_types.attributes
exception NotAnAttrParam of Cil_types.exp
val isConstType : Cil_types.typ -> bool
val isVolatileType : Cil_types.typ -> bool
val isVolatileLogicType : Cil_types.logic_type -> bool
val isVolatileLval : Cil_types.lval -> bool
val isVolatileTermLval : Cil_types.term_lval -> bool
val isGhostType : Cil_types.typ -> bool
val isWFGhostType : Cil_types.typ -> bool
type 'a visitAction =
SkipChildren
| DoChildren
| DoChildrenPost of ('a -> '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:Cil_types.identified_predicate list ->
?requires:Cil_types.identified_predicate list ->
?post_cond:(Cil_types.termination_kind * Cil_types.identified_predicate)
list ->
?assigns:Cil_types.assigns ->
?allocation:Cil_types.allocation ->
?extended:Cil_types.acsl_extension list -> unit -> Cil_types.behavior
val default_behavior_name : string
val is_default_behavior : Cil_types.behavior -> bool
val find_default_behavior :
Cil_types.funspec -> Cil_types.funbehavior option
val find_default_requires :
Cil_types.behavior list -> Cil_types.identified_predicate list
class type cilVisitor =
object
method behavior : Visitor_behavior.t
method current_func : Cil_types.fundec option
method current_kinstr : Cil_types.kinstr
method current_stmt : Cil_types.stmt option
method fill_global_tables : unit
method get_filling_actions : (unit -> unit) Queue.t
method plain_copy_visitor : 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.allocation -> Cil_types.allocation visitAction
method vannotation :
Cil_types.global_annotation ->
Cil_types.global_annotation visitAction
method vassigns : Cil_types.assigns -> 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.deps -> 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.from -> 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.impact_pragma -> 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.loop_pragma -> 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.slice_pragma -> 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.t -> (unit -> unit) Queue.t -> cilVisitor
class genericCilVisitor : Visitor_behavior.t -> cilVisitor
class nopCilVisitor : cilVisitor
val doVisit :
'visitor ->
'visitor ->
('a -> 'a) ->
('a -> 'a visitAction) -> ('visitor -> 'a -> 'a) -> 'a -> 'a
val doVisitList :
'visitor ->
'visitor ->
('a -> 'a) ->
('a -> 'a list visitAction) -> ('visitor -> 'a -> 'a) -> '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.deps -> Cil_types.deps
val visitCilFrom : cilVisitor -> Cil_types.from -> Cil_types.from
val visitCilAssigns : cilVisitor -> Cil_types.assigns -> 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.allocation -> 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) -> ('a -> Datatype.t) -> unit
type data = Cil_types.location
val set : data -> unit
val get : unit -> data
val clear : unit -> unit
end
val pp_thisloc : Format.formatter -> unit
val empty_funspec : unit -> Cil_types.funspec
val is_empty_funspec : Cil_types.funspec -> bool
val is_empty_behavior : Cil_types.funbehavior -> bool
val uniqueVarNames : Cil_types.file -> unit
val peepHole2 :
aggressive:bool ->
(Cil_types.stmt * Cil_types.stmt -> Cil_types.stmt list option) ->
Cil_types.stmt list -> Cil_types.stmt list
val peepHole1 :
(Cil_types.instr -> Cil_types.instr list option) ->
Cil_types.stmt list -> unit
exception SizeOfError of string * Cil_types.typ
val empty_size_cache : unit -> Cil_types.bitsSizeofTypCache
val unsignedVersionOf : Cil_types.ikind -> Cil_types.ikind
val intKindForSize : int -> bool -> Cil_types.ikind
val floatKindForSize : int -> Cil_types.fkind
val bitsSizeOf : Cil_types.typ -> int
val bytesSizeOf : Cil_types.typ -> int
val bytesSizeOfInt : Cil_types.ikind -> int
val bitsSizeOfInt : Cil_types.ikind -> int
val isSigned : Cil_types.ikind -> bool
val bitsSizeOfBitfield : Cil_types.typ -> int
val rank : Cil_types.ikind -> int
val intTypeIncluded : Cil_types.ikind -> Cil_types.ikind -> bool
val frank : Cil_types.fkind -> int
val truncateInteger64 : Cil_types.ikind -> Integer.t -> Integer.t * bool
val max_signed_number : int -> Integer.t
val min_signed_number : int -> Integer.t
val max_unsigned_number : int -> Integer.t
val fitsInInt : Cil_types.ikind -> Integer.t -> bool
val isFiniteFloat : Cil_types.fkind -> float -> bool
val isExactFloat : Cil_types.fkind -> Cil_types.logic_real -> bool
exception Not_representable
val intKindForValue : Integer.t -> bool -> Cil_types.ikind
val sizeOf : loc:Cil_types.location -> Cil_types.typ -> Cil_types.exp
val bytesAlignOf : Cil_types.typ -> int
val intOfAttrparam : Cil_types.attrparam -> int option
val bitsOffset : Cil_types.typ -> Cil_types.offset -> int * int
val mapNoCopy : ('a -> 'a) -> '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 -> 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 set_extension_handler :
visit:(string ->
cilVisitor ->
Cil_types.acsl_extension_kind ->
Cil_types.acsl_extension_kind visitAction) ->
unit
val set_deprecated_extension_handler :
handler:(string ->
Cil_types.ext_category ->
(cilVisitor ->
Cil_types.acsl_extension_kind ->
Cil_types.acsl_extension_kind visitAction) ->
unit) ->
unit
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 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