sig
type file = {
mutable fileName : string;
mutable globals : Cil_types.global list;
mutable globinit : Cil_types.fundec option;
mutable globinitcalled : bool;
}
and global =
GType of Cil_types.typeinfo * Cil_types.location
| GCompTag of Cil_types.compinfo * Cil_types.location
| GCompTagDecl of Cil_types.compinfo * Cil_types.location
| GEnumTag of Cil_types.enuminfo * Cil_types.location
| GEnumTagDecl of Cil_types.enuminfo * Cil_types.location
| GVarDecl of Cil_types.funspec * Cil_types.varinfo * Cil_types.location
| GVar of Cil_types.varinfo * Cil_types.initinfo * Cil_types.location
| GFun of Cil_types.fundec * Cil_types.location
| GAsm of string * Cil_types.location
| GPragma of Cil_types.attribute * Cil_types.location
| GText of string
| GAnnot of Cil_types.global_annotation * Cil_types.location
and typ =
TVoid of Cil_types.attributes
| TInt of Cil_types.ikind * Cil_types.attributes
| TFloat of Cil_types.fkind * Cil_types.attributes
| TPtr of Cil_types.typ * Cil_types.attributes
| TArray of Cil_types.typ * Cil_types.exp option *
Cil_types.bitsSizeofTypCache * Cil_types.attributes
| TFun of Cil_types.typ *
(string * Cil_types.typ * Cil_types.attributes) list option *
bool * Cil_types.attributes
| TNamed of Cil_types.typeinfo * Cil_types.attributes
| TComp of Cil_types.compinfo * Cil_types.bitsSizeofTypCache *
Cil_types.attributes
| TEnum of Cil_types.enuminfo * Cil_types.attributes
| TBuiltin_va_list of Cil_types.attributes
and ikind =
IBool
| IChar
| ISChar
| IUChar
| IInt
| IUInt
| IShort
| IUShort
| ILong
| IULong
| ILongLong
| IULongLong
and fkind = FFloat | FDouble | FLongDouble
and bitsSizeofTyp =
Not_Computed
| Computed of int
| Not_Computable of (string * Cil_types.typ)
and bitsSizeofTypCache = { mutable scache : Cil_types.bitsSizeofTyp; }
and attribute =
Attr of string * Cil_types.attrparam list
| AttrAnnot of string
and attributes = Cil_types.attribute list
and attrparam =
AInt of Integer.t
| AStr of string
| ACons of string * Cil_types.attrparam list
| ASizeOf of Cil_types.typ
| ASizeOfE of Cil_types.attrparam
| AAlignOf of Cil_types.typ
| AAlignOfE of Cil_types.attrparam
| AUnOp of Cil_types.unop * Cil_types.attrparam
| ABinOp of Cil_types.binop * Cil_types.attrparam * Cil_types.attrparam
| ADot of Cil_types.attrparam * string
| AStar of Cil_types.attrparam
| AAddrOf of Cil_types.attrparam
| AIndex of Cil_types.attrparam * Cil_types.attrparam
| AQuestion of Cil_types.attrparam * Cil_types.attrparam *
Cil_types.attrparam
and compinfo = {
mutable cstruct : bool;
corig_name : string;
mutable cname : string;
mutable ckey : int;
mutable cfields : Cil_types.fieldinfo list;
mutable cattr : Cil_types.attributes;
mutable cdefined : bool;
mutable creferenced : bool;
}
and fieldinfo = {
mutable fcomp : Cil_types.compinfo;
forig_name : string;
mutable fname : string;
mutable ftype : Cil_types.typ;
mutable fbitfield : int option;
mutable fattr : Cil_types.attributes;
mutable floc : Cil_types.location;
mutable faddrof : bool;
mutable fsize_in_bits : int option;
mutable foffset_in_bits : int option;
mutable fpadding_in_bits : int option;
}
and enuminfo = {
eorig_name : string;
mutable ename : string;
mutable eitems : Cil_types.enumitem list;
mutable eattr : Cil_types.attributes;
mutable ereferenced : bool;
mutable ekind : Cil_types.ikind;
}
and enumitem = {
eiorig_name : string;
mutable einame : string;
mutable eival : Cil_types.exp;
mutable eihost : Cil_types.enuminfo;
eiloc : Cil_types.location;
}
and typeinfo = {
torig_name : string;
mutable tname : string;
mutable ttype : Cil_types.typ;
mutable treferenced : bool;
}
and varinfo = {
mutable vname : string;
vorig_name : string;
mutable vtype : Cil_types.typ;
mutable vattr : Cil_types.attributes;
mutable vstorage : Cil_types.storage;
mutable vglob : bool;
mutable vdefined : bool;
mutable vformal : bool;
mutable vinline : bool;
mutable vdecl : Cil_types.location;
mutable vid : int;
mutable vaddrof : bool;
mutable vreferenced : bool;
vgenerated : bool;
mutable vdescr : string option;
mutable vdescrpure : bool;
mutable vghost : bool;
vlogic : bool;
mutable vlogic_var_assoc : Cil_types.logic_var option;
}
and storage = NoStorage | Static | Register | Extern
and exp = {
eid : int;
enode : Cil_types.exp_node;
eloc : Cil_types.location;
}
and exp_node =
Const of Cil_types.constant
| Lval of Cil_types.lval
| SizeOf of Cil_types.typ
| SizeOfE of Cil_types.exp
| SizeOfStr of string
| AlignOf of Cil_types.typ
| AlignOfE of Cil_types.exp
| UnOp of Cil_types.unop * Cil_types.exp * Cil_types.typ
| BinOp of Cil_types.binop * Cil_types.exp * Cil_types.exp *
Cil_types.typ
| CastE of Cil_types.typ * Cil_types.exp
| AddrOf of Cil_types.lval
| StartOf of Cil_types.lval
| Info of Cil_types.exp * Cil_types.exp_info
and exp_info = { exp_type : Cil_types.logic_type; exp_name : string list; }
and constant =
CInt64 of Integer.t * Cil_types.ikind * string option
| CStr of string
| CWStr of int64 list
| CChr of char
| CReal of float * Cil_types.fkind * string option
| CEnum of Cil_types.enumitem
and unop = Neg | BNot | LNot
and binop =
PlusA
| PlusPI
| IndexPI
| MinusA
| MinusPI
| MinusPP
| Mult
| Div
| Mod
| Shiftlt
| Shiftrt
| Lt
| Gt
| Le
| Ge
| Eq
| Ne
| BAnd
| BXor
| BOr
| LAnd
| LOr
and lval = Cil_types.lhost * Cil_types.offset
and lhost = Var of Cil_types.varinfo | Mem of Cil_types.exp
and offset =
NoOffset
| Field of Cil_types.fieldinfo * Cil_types.offset
| Index of Cil_types.exp * Cil_types.offset
and init =
SingleInit of Cil_types.exp
| CompoundInit of Cil_types.typ *
(Cil_types.offset * Cil_types.init) list
and initinfo = { mutable init : Cil_types.init option; }
and fundec = {
mutable svar : Cil_types.varinfo;
mutable sformals : Cil_types.varinfo list;
mutable slocals : Cil_types.varinfo list;
mutable smaxid : int;
mutable sbody : Cil_types.block;
mutable smaxstmtid : int option;
mutable sallstmts : Cil_types.stmt list;
mutable sspec : Cil_types.funspec;
}
and block = {
mutable battrs : Cil_types.attributes;
mutable blocals : Cil_types.varinfo list;
mutable bstmts : Cil_types.stmt list;
}
and stmt = {
mutable labels : Cil_types.label list;
mutable skind : Cil_types.stmtkind;
mutable sid : int;
mutable succs : Cil_types.stmt list;
mutable preds : Cil_types.stmt list;
mutable ghost : bool;
}
and label =
Label of string * Cil_types.location * bool
| Case of Cil_types.exp * Cil_types.location
| Default of Cil_types.location
and stmtkind =
Instr of Cil_types.instr
| Return of Cil_types.exp option * Cil_types.location
| Goto of Cil_types.stmt Pervasives.ref * Cil_types.location
| Break of Cil_types.location
| Continue of Cil_types.location
| If of Cil_types.exp * Cil_types.block * Cil_types.block *
Cil_types.location
| Switch of Cil_types.exp * Cil_types.block * Cil_types.stmt list *
Cil_types.location
| Loop of Cil_types.code_annotation list * Cil_types.block *
Cil_types.location * Cil_types.stmt option * Cil_types.stmt option
| Block of Cil_types.block
| UnspecifiedSequence of
(Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
Cil_types.lval list * Cil_types.stmt Pervasives.ref list)
list
| TryFinally of Cil_types.block * Cil_types.block * Cil_types.location
| TryExcept of Cil_types.block * (Cil_types.instr list * Cil_types.exp) *
Cil_types.block * Cil_types.location
and instr =
Set of Cil_types.lval * Cil_types.exp * Cil_types.location
| Call of Cil_types.lval option * Cil_types.exp * Cil_types.exp list *
Cil_types.location
| Asm of Cil_types.attributes * string list *
(string option * string * Cil_types.lval) list *
(string option * string * Cil_types.exp) list * string list *
Cil_types.stmt Pervasives.ref list * Cil_types.location
| Skip of Cil_types.location
| Code_annot of Cil_types.code_annotation * Cil_types.location
and location = Lexing.position * Lexing.position
and logic_constant =
Integer of Integer.t * string option
| LStr of string
| LWStr of int64 list
| LChr of char
| LReal of Cil_types.logic_real
| LEnum of Cil_types.enumitem
and logic_real = {
r_literal : string;
r_nearest : float;
r_upper : float;
r_lower : float;
}
and logic_type =
Ctype of Cil_types.typ
| Ltype of Cil_types.logic_type_info * Cil_types.logic_type list
| Lvar of string
| Linteger
| Lreal
| Larrow of Cil_types.logic_type list * Cil_types.logic_type
and identified_term = { it_id : int; it_content : Cil_types.term; }
and logic_label =
StmtLabel of Cil_types.stmt Pervasives.ref
| LogicLabel of (Cil_types.stmt option * string)
and term = {
term_node : Cil_types.term_node;
term_loc : Lexing.position * Lexing.position;
term_type : Cil_types.logic_type;
term_name : string list;
}
and term_node =
TConst of Cil_types.logic_constant
| TLval of Cil_types.term_lval
| TSizeOf of Cil_types.typ
| TSizeOfE of Cil_types.term
| TSizeOfStr of string
| TAlignOf of Cil_types.typ
| TAlignOfE of Cil_types.term
| TUnOp of Cil_types.unop * Cil_types.term
| TBinOp of Cil_types.binop * Cil_types.term * Cil_types.term
| TCastE of Cil_types.typ * Cil_types.term
| TAddrOf of Cil_types.term_lval
| TStartOf of Cil_types.term_lval
| Tapp of Cil_types.logic_info *
(Cil_types.logic_label * Cil_types.logic_label) list *
Cil_types.term list
| Tlambda of Cil_types.quantifiers * Cil_types.term
| TDataCons of Cil_types.logic_ctor_info * Cil_types.term list
| Tif of Cil_types.term * Cil_types.term * Cil_types.term
| Tat of Cil_types.term * Cil_types.logic_label
| Tbase_addr of Cil_types.logic_label * Cil_types.term
| Toffset of Cil_types.logic_label * Cil_types.term
| Tblock_length of Cil_types.logic_label * Cil_types.term
| Tnull
| TLogic_coerce of Cil_types.logic_type * Cil_types.term
| TCoerce of Cil_types.term * Cil_types.typ
| TCoerceE of Cil_types.term * Cil_types.term
| TUpdate of Cil_types.term * Cil_types.term_offset * Cil_types.term
| Ttypeof of Cil_types.term
| Ttype of Cil_types.typ
| Tempty_set
| Tunion of Cil_types.term list
| Tinter of Cil_types.term list
| Tcomprehension of Cil_types.term * Cil_types.quantifiers *
Cil_types.predicate Cil_types.named option
| Trange of Cil_types.term option * Cil_types.term option
| Tlet of Cil_types.logic_info * Cil_types.term
and term_lval = Cil_types.term_lhost * Cil_types.term_offset
and term_lhost =
TVar of Cil_types.logic_var
| TResult of Cil_types.typ
| TMem of Cil_types.term
and model_info = {
mi_name : string;
mi_field_type : Cil_types.logic_type;
mi_base_type : Cil_types.typ;
mi_decl : Cil_types.location;
}
and term_offset =
TNoOffset
| TField of Cil_types.fieldinfo * Cil_types.term_offset
| TModel of Cil_types.model_info * Cil_types.term_offset
| TIndex of Cil_types.term * Cil_types.term_offset
and logic_info = {
mutable l_var_info : Cil_types.logic_var;
mutable l_labels : Cil_types.logic_label list;
mutable l_tparams : string list;
mutable l_type : Cil_types.logic_type option;
mutable l_profile : Cil_types.logic_var list;
mutable l_body : Cil_types.logic_body;
}
and builtin_logic_info = {
mutable bl_name : string;
mutable bl_labels : Cil_types.logic_label list;
mutable bl_params : string list;
mutable bl_type : Cil_types.logic_type option;
mutable bl_profile : (string * Cil_types.logic_type) list;
}
and logic_body =
LBnone
| LBreads of Cil_types.identified_term list
| LBterm of Cil_types.term
| LBpred of Cil_types.predicate Cil_types.named
| LBinductive of
(string * Cil_types.logic_label list * string list *
Cil_types.predicate Cil_types.named)
list
and logic_type_info = {
lt_name : string;
lt_params : string list;
mutable lt_def : Cil_types.logic_type_def option;
}
and logic_type_def =
LTsum of Cil_types.logic_ctor_info list
| LTsyn of Cil_types.logic_type
and logic_var_kind = LVGlobal | LVC | LVFormal | LVQuant | LVLocal
and logic_var = {
mutable lv_name : string;
mutable lv_id : int;
mutable lv_type : Cil_types.logic_type;
mutable lv_kind : Cil_types.logic_var_kind;
mutable lv_origin : Cil_types.varinfo option;
}
and logic_ctor_info = {
ctor_name : string;
ctor_type : Cil_types.logic_type_info;
ctor_params : Cil_types.logic_type list;
}
and quantifiers = Cil_types.logic_var list
and relation = Rlt | Rgt | Rle | Rge | Req | Rneq
and predicate =
Pfalse
| Ptrue
| Papp of Cil_types.logic_info *
(Cil_types.logic_label * Cil_types.logic_label) list *
Cil_types.term list
| Pseparated of Cil_types.term list
| Prel of Cil_types.relation * Cil_types.term * Cil_types.term
| Pand of Cil_types.predicate Cil_types.named *
Cil_types.predicate Cil_types.named
| Por of Cil_types.predicate Cil_types.named *
Cil_types.predicate Cil_types.named
| Pxor of Cil_types.predicate Cil_types.named *
Cil_types.predicate Cil_types.named
| Pimplies of Cil_types.predicate Cil_types.named *
Cil_types.predicate Cil_types.named
| Piff of Cil_types.predicate Cil_types.named *
Cil_types.predicate Cil_types.named
| Pnot of Cil_types.predicate Cil_types.named
| Pif of Cil_types.term * Cil_types.predicate Cil_types.named *
Cil_types.predicate Cil_types.named
| Plet of Cil_types.logic_info * Cil_types.predicate Cil_types.named
| Pforall of Cil_types.quantifiers * Cil_types.predicate Cil_types.named
| Pexists of Cil_types.quantifiers * Cil_types.predicate Cil_types.named
| Pat of Cil_types.predicate Cil_types.named * Cil_types.logic_label
| Pvalid_read of Cil_types.logic_label * Cil_types.term
| Pvalid of Cil_types.logic_label * Cil_types.term
| Pinitialized of Cil_types.logic_label * Cil_types.term
| Pallocable of Cil_types.logic_label * Cil_types.term
| Pfreeable of Cil_types.logic_label * Cil_types.term
| Pfresh of Cil_types.logic_label * Cil_types.logic_label *
Cil_types.term * Cil_types.term
| Psubtype of Cil_types.term * Cil_types.term
and identified_predicate = {
mutable ip_name : string list;
ip_loc : Cil_types.location;
ip_id : int;
ip_content : Cil_types.predicate;
}
and 'term variant = 'term * string option
and 'locs allocation = FreeAlloc of 'locs list * 'locs list | FreeAllocAny
and 'locs deps = From of 'locs list | FromAny
and 'locs from = 'locs * 'locs Cil_types.deps
and 'locs assigns = WritesAny | Writes of 'locs Cil_types.from list
and 'a named = {
name : string list;
loc : Cil_types.location;
content : 'a;
}
and ('term, 'pred, 'locs) spec = {
mutable spec_behavior : ('pred, 'locs) Cil_types.behavior list;
mutable spec_variant : 'term Cil_types.variant option;
mutable spec_terminates : 'pred option;
mutable spec_complete_behaviors : string list list;
mutable spec_disjoint_behaviors : string list list;
}
and ('pred, 'locs) behavior = {
mutable b_name : string;
mutable b_requires : 'pred list;
mutable b_assumes : 'pred list;
mutable b_post_cond : (Cil_types.termination_kind * 'pred) list;
mutable b_assigns : 'locs Cil_types.assigns;
mutable b_allocation : 'locs Cil_types.allocation;
mutable b_extended : (string * int * 'pred list) list;
}
and termination_kind = Normal | Exits | Breaks | Continues | Returns
and 'term loop_pragma =
Unroll_specs of 'term list
| Widen_hints of 'term list
| Widen_variables of 'term list
and 'term slice_pragma = SPexpr of 'term | SPctrl | SPstmt
and 'term impact_pragma = IPexpr of 'term | IPstmt
and 'term pragma =
Loop_pragma of 'term Cil_types.loop_pragma
| Slice_pragma of 'term Cil_types.slice_pragma
| Impact_pragma of 'term Cil_types.impact_pragma
and ('term, 'pred, 'spec_pred, 'locs) code_annot =
AAssert of string list * 'pred
| AStmtSpec of string list * ('term, 'spec_pred, 'locs) Cil_types.spec
| AInvariant of string list * bool * 'pred
| AVariant of 'term Cil_types.variant
| AAssigns of string list * 'locs Cil_types.assigns
| AAllocation of string list * 'locs Cil_types.allocation
| APragma of 'term Cil_types.pragma
and funspec =
(Cil_types.term, Cil_types.identified_predicate,
Cil_types.identified_term)
Cil_types.spec
and code_annotation = {
annot_id : int;
annot_content :
(Cil_types.term, Cil_types.predicate Cil_types.named,
Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.code_annot;
}
and funbehavior =
(Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.behavior
and global_annotation =
Dfun_or_pred of Cil_types.logic_info * Cil_types.location
| Dvolatile of Cil_types.identified_term list *
Cil_types.varinfo option * Cil_types.varinfo option *
Cil_types.location
| Daxiomatic of string * Cil_types.global_annotation list *
Cil_types.location
| Dtype of Cil_types.logic_type_info * Cil_types.location
| Dlemma of string * bool * Cil_types.logic_label list * string list *
Cil_types.predicate Cil_types.named * Cil_types.location
| Dinvariant of Cil_types.logic_info * Cil_types.location
| Dtype_annot of Cil_types.logic_info * Cil_types.location
| Dmodel_annot of Cil_types.model_info * Cil_types.location
| Dcustom_annot of Cil_types.custom_tree * string * Cil_types.location
and custom_tree = CustomDummy
type kinstr = Kstmt of Cil_types.stmt | Kglobal
type cil_function =
Definition of (Cil_types.fundec * Cil_types.location)
| Declaration of
(Cil_types.funspec * Cil_types.varinfo *
Cil_types.varinfo list option * Cil_types.location)
type kernel_function = {
mutable fundec : Cil_types.cil_function;
mutable return_stmt : Cil_types.stmt option;
mutable spec : Cil_types.funspec;
}
type localisation =
VGlobal
| VLocal of Cil_types.kernel_function
| VFormal of Cil_types.kernel_function
type mach = {
version_major : int;
version_minor : int;
version : string;
underscore_name : bool;
sizeof_short : int;
sizeof_int : int;
sizeof_long : int;
sizeof_longlong : int;
sizeof_ptr : int;
sizeof_float : int;
sizeof_double : int;
sizeof_longdouble : int;
sizeof_void : int;
sizeof_fun : int;
size_t : string;
wchar_t : string;
ptrdiff_t : string;
alignof_short : int;
alignof_int : int;
alignof_long : int;
alignof_longlong : int;
alignof_ptr : int;
alignof_float : int;
alignof_double : int;
alignof_longdouble : int;
alignof_str : int;
alignof_fun : int;
char_is_unsigned : bool;
const_string_literals : bool;
little_endian : bool;
alignof_aligned : int;
has__builtin_va_list : bool;
__thread_is_keyword : bool;
}
end