sig
type file = {
mutable fileName : Filepath.Normalized.t;
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.varinfo * Cil_types.location
| GFunDecl 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;
vtemp : bool;
mutable vdescr : string option;
mutable vdescrpure : bool;
mutable vghost : bool;
vsource : 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 constructor_kind = Plain_func | Constructor
and local_init =
AssignInit of Cil_types.init
| ConsInit of Cil_types.varinfo * Cil_types.exp list *
Cil_types.constructor_kind
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 bscoping : bool;
mutable blocals : Cil_types.varinfo list;
mutable bstatics : 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;
mutable sattr : Cil_types.attributes;
}
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
| Throw of (Cil_types.exp * Cil_types.typ) option * Cil_types.location
| TryCatch of Cil_types.block *
(Cil_types.catch_binder * Cil_types.block) list * Cil_types.location
| 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 catch_binder =
Catch_exn of Cil_types.varinfo *
(Cil_types.varinfo * Cil_types.block) list
| Catch_all
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
| Local_init of Cil_types.varinfo * Cil_types.local_init *
Cil_types.location
| Asm of Cil_types.attributes * string list *
Cil_types.extended_asm option * Cil_types.location
| Skip of Cil_types.location
| Code_annot of Cil_types.code_annotation * Cil_types.location
and extended_asm = {
asm_outputs : (string option * string * Cil_types.lval) list;
asm_inputs : (string option * string * Cil_types.exp) list;
asm_clobbers : string list;
asm_gotos : Cil_types.stmt Pervasives.ref list;
}
and location = Filepath.position * Filepath.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
| FormalLabel of string
| BuiltinLabel of Cil_types.logic_builtin_label
and logic_builtin_label =
Here
| Old
| Pre
| Post
| LoopEntry
| LoopCurrent
| Init
and term = {
term_node : Cil_types.term_node;
term_loc : Filepath.position * Filepath.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 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
| 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 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;
mutable mi_attr : Cil_types.attributes;
}
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
| LBinductive of
(string * Cil_types.logic_label list * string list *
Cil_types.predicate)
list
and logic_type_info = {
mutable lt_name : string;
lt_params : string list;
mutable lt_def : Cil_types.logic_type_def option;
mutable lt_attr : Cil_types.attributes;
}
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;
mutable lv_attr : Cil_types.attributes;
}
and logic_ctor_info = {
mutable 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_node =
Pfalse
| Ptrue
| Papp of Cil_types.logic_info * 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.predicate
| Por of Cil_types.predicate * Cil_types.predicate
| Pxor of Cil_types.predicate * Cil_types.predicate
| Pimplies of Cil_types.predicate * Cil_types.predicate
| Piff of Cil_types.predicate * Cil_types.predicate
| Pnot of Cil_types.predicate
| Pif of Cil_types.term * Cil_types.predicate * Cil_types.predicate
| Plet of Cil_types.logic_info * Cil_types.predicate
| Pforall of Cil_types.quantifiers * Cil_types.predicate
| Pexists of Cil_types.quantifiers * Cil_types.predicate
| Pat of Cil_types.predicate * Cil_types.logic_label
| Pvalid_read of Cil_types.logic_label * Cil_types.term
| Pvalid of Cil_types.logic_label * Cil_types.term
| Pvalid_function of Cil_types.term
| Pinitialized of Cil_types.logic_label * Cil_types.term
| Pdangling 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
and identified_predicate = {
ip_id : int;
ip_content : Cil_types.predicate;
}
and predicate = {
pred_name : string list;
pred_loc : Cil_types.location;
pred_content : Cil_types.predicate_node;
}
and variant = Cil_types.term * string option
and allocation =
FreeAlloc of Cil_types.identified_term list *
Cil_types.identified_term list
| FreeAllocAny
and deps = From of Cil_types.identified_term list | FromAny
and from = Cil_types.identified_term * Cil_types.deps
and assigns = WritesAny | Writes of Cil_types.from list
and spec = {
mutable spec_behavior : Cil_types.behavior list;
mutable spec_variant : Cil_types.variant option;
mutable spec_terminates : Cil_types.identified_predicate option;
mutable spec_complete_behaviors : string list list;
mutable spec_disjoint_behaviors : string list list;
}
and acsl_extension = {
ext_id : int;
ext_name : string;
ext_loc : Cil_types.location;
ext_has_status : bool;
ext_kind : Cil_types.acsl_extension_kind;
}
and acsl_extension_kind =
Ext_id of int
| Ext_terms of Cil_types.term list
| Ext_preds of Cil_types.predicate list
and ext_category =
Ext_contract
| Ext_global
| Ext_code_annot of Cil_types.ext_code_annot_context
and ext_code_annot_context =
Ext_here
| Ext_next_stmt
| Ext_next_loop
| Ext_next_both
and behavior = {
mutable b_name : string;
mutable b_requires : Cil_types.identified_predicate list;
mutable b_assumes : Cil_types.identified_predicate list;
mutable b_post_cond :
(Cil_types.termination_kind * Cil_types.identified_predicate) list;
mutable b_assigns : Cil_types.assigns;
mutable b_allocation : Cil_types.allocation;
mutable b_extended : Cil_types.acsl_extension list;
}
and termination_kind = Normal | Exits | Breaks | Continues | Returns
and loop_pragma =
Unroll_specs of Cil_types.term list
| Widen_hints of Cil_types.term list
| Widen_variables of Cil_types.term list
and slice_pragma = SPexpr of Cil_types.term | SPctrl | SPstmt
and impact_pragma = IPexpr of Cil_types.term | IPstmt
and pragma =
Loop_pragma of Cil_types.loop_pragma
| Slice_pragma of Cil_types.slice_pragma
| Impact_pragma of Cil_types.impact_pragma
and assertion_kind = Assert | Check
and code_annotation_node =
AAssert of string list * Cil_types.assertion_kind * Cil_types.predicate
| AStmtSpec of string list * Cil_types.spec
| AInvariant of string list * bool * Cil_types.predicate
| AVariant of Cil_types.variant
| AAssigns of string list * Cil_types.assigns
| AAllocation of string list * Cil_types.allocation
| APragma of Cil_types.pragma
| AExtended of string list * bool * Cil_types.acsl_extension
and funspec = Cil_types.spec
and code_annotation = {
annot_id : int;
annot_content : Cil_types.code_annotation_node;
}
and funbehavior = 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.attributes * Cil_types.location
| Daxiomatic of string * Cil_types.global_annotation list *
Cil_types.attributes * 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.attributes * 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
| Dextended of Cil_types.acsl_extension * Cil_types.attributes *
Cil_types.location
| Dcustom_annot of Cil_types.custom_tree * string *
Cil_types.attributes * 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 spec : Cil_types.funspec;
}
type localisation =
VGlobal
| VLocal of Cil_types.kernel_function
| VFormal of Cil_types.kernel_function
type syntactic_scope =
Program
| Translation_unit of Filepath.Normalized.t
| Block_scope of Cil_types.stmt
type mach = {
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;
underscore_name : bool;
const_string_literals : bool;
little_endian : bool;
alignof_aligned : int;
has__builtin_va_list : bool;
__thread_is_keyword : bool;
compiler : string;
cpp_arch_flags : string list;
version : string;
}
end